如何定义多变量箭头？

Question

这个问题与之前的问题有些相关

： 我正在尝试定义几个半依赖类型，它们允许您跟踪函数的“单调性”（如

单调性类型

论文中所述），以便程序员不必手动执行此操作（并且当非单调操作传递给需要单调操作的操作时，会在编译时失败）。 更一般地说：我想跟踪函数的一些“限定符”

基于

对这个早期问题的回答

，我已经能够定义“索引类别”和“索引箭头”，其中h中

h = f >>> g

的限定符取决于

f

和

g

的限定符.只要您只使用单参数函数，这种方法就很有效。但是，（普通箭头也有这个问题），当您尝试创建具有多个参数的箭头时，您有以下选项。 （以

(+) :: Int -> Int -> Int

为例）：

普通

arr (+)
1. 。由于该函数是柯里化的，因此结果类型将是

   Arrow x => x Int (Int -> Int)

   。这意味着只有第一个参数被提升到箭头上下文中，因为箭头“返回一个少一个参数的函数”。换句话说：箭头上下文不用于其余参数，因此这不是我们想要的。
arr (uncurry (+))
2. 。结果类型将是

   Arrow x => x (Int, Int) Int

   。现在这两个参数都成为了箭头的一部分，但是我们失去了例如部分应用它。我也不清楚如何以与参数无关的方式进行取消柯里化：如果我们想要三个、四个、五个......参数函数怎么办？
我知道可以定义一个“递归类型类”来创建一个多元函数，例如 Rosettacode

here

上描述的例子。我试图定义一个更通用的函数包装类型，可能会以这种方式工作，但到目前为止我还没有成功。我不知道如何在 a -> b 的类型类实例中正确辨别

b

是最终结果还是另一个函数

(b' -> c)

，以及如何提取和使用

b'

的限定符（如果结果是）第二种情况。这可能吗？我在这里错过了什么吗？或者我完全走错了路，有没有另一种方法可以将

n-argument

函数提升为箭头，而不管 n 的值如何？

Answer 1

arrowfy

将函数

a -> b -> ...

转换为箭头

a `r` b `r` ...

（其中

r :: Type -> Type -> Type

是箭头类型），以及定义函数

uncurry_

将函数转换为具有单个元组参数的函数

(a, (b, ...)) -> z

（然后可以使用以下命令将其提升到任意箭头

arr :: (u -> v) -> r u v

）。

{-# LANGUAGE
    AllowAmbiguousTypes,
    FlexibleContexts,
    FlexibleInstances,
    MultiParamTypeClasses,
    UndecidableInstances,
    TypeApplications
  #-}

import Control.Category hiding ((.), id)
import Control.Arrow
import Data.Kind (Type)

两种方法都使用具有重叠实例的多参数类型类。一个函数实例，只要初始类型是函数类型，就会选择该实例；一个基本情况实例，只要它不是函数类型，就会选择该实例。

-- Turn (a -> (b -> (c -> ...))) into (a `r` (b `r` (c `r` ...)))
class Arrowfy (r :: Type -> Type -> Type) x y where
  arrowfy :: x -> y

instance {-# OVERLAPPING #-} (Arrow r, Arrowfy r b z, y ~ r a z) => Arrowfy r (a -> b) y where
  arrowfy f = arr (arrowfy @r @b @z . f)

instance (x ~ y) => Arrowfy r x y where
  arrowfy = id

关于 

arrowfy @r @b @z

语法的旁注这是 TypeApplications 语法，自 GHC 8.0 起可用。

arrowfy的类型是：

arrowfy :: forall r x y. Arrowfy r x y => x -> y

问题在于 r 是不明确的：在表达式中，上下文只能确定 x 和 y，而这并不一定限制 r。
@r 注释允许我们显式地专门化 arrowfy。
请注意，arrowfy 的类型参数必须以固定顺序出现：

arrowfy :: forall r x y. ...

arrowfy @r1 @b @z             -- r = r1, x = b, y = z

（

GHC 用户指南

TypeApplications

）

现在，例如，如果您有一个箭头

---

(:->)

，您可以编写以下代码将其变成箭头：

test :: Int :-> (Int :-> Int)
test = arrowfy (+)

对于 

uncurry_

，有一个额外的小技巧，可以将 n 参数函数转换为 n 元组上的函数，而不是您天真地得到的由单位限制的 (n+1) 元组。现在两个实例都按函数类型索引，实际测试的是结果类型是否是函数。

-- Turn (a -> (b -> (c -> ... (... -> z) ...))) into ((a, (b, (c, ...))) -> z)
class Uncurry x y z where
  uncurry_ :: x -> y -> z

instance {-# OVERLAPPING #-} (Uncurry (b -> c) yb z, y ~ (a, yb)) => Uncurry (a -> b -> c) y z where
  uncurry_ f (a, yb) = uncurry_ (f a) yb

instance (a ~ y, b ~ z) => Uncurry (a -> b) y z where
  uncurry_ = id

一些例子：

testUncurry :: (Int, Int) -> Int
testUncurry = uncurry_ (+)

-- combined with arr
testUncurry2 :: (Int, (Int, (Int, Int))) :-> Int
testUncurry2 = arr (uncurry_ (\a b c d -> a + b + c + d))

完整要点：

https://gist.github.com/Lysxia/c754f2fd6a514d66559b92469e373352