如何定义多变量箭头？

Question

这个问题和this earlier one有点关系：

我正在尝试定义几个半依赖类型，它们允许您跟踪函数的“单调性”（如Monotonicity Types 论文中所述），因此程序员不必手动执行此操作（当非单调操作被传递给需要的东西时，在编译时失败）。

更一般地说：我想跟踪函数的一些“限定符”

基于answers to this earlier question，我已经能够定义一个“索引类别”和“索引箭头”，其中h = f >>> g 中h 的限定词取决于f 和g 的限定词。

只要您只使用单参数函数，这很有效。但是，（和普通箭头也有这个问题），当你尝试创建一个带有多个参数的箭头时，你有以下选项。 （以(+) :: Int -> Int -> Int 为例）：

1. 普通arr (+)。这个结果类型将是Arrow x => x Int (Int -> Int)，因为这个函数是柯里化的。这意味着只有第一个参数被提升到箭头上下文中，因为箭头“返回一个参数更少的函数”。换句话说：箭头上下文不用于其余参数，所以这不是我们想要的。
2. arr (uncurry (+))。结果类型为Arrow x => x (Int, Int) Int。现在这两个参数都成为箭头的一部分，但我们失去了例如部分应用它。我也不清楚如何以与数量无关的方式进行 uncurrying：如果我们想要三个、四个、五个...参数函数怎么办？

我知道可以定义一个“递归类型类”来创建一个多变量函数，例如 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 user guide on TypeApplications)

---

现在，例如，如果你有一个箭头(:->)，你可以写这个把它变成一个箭头：

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

对于uncurry_，有一个额外的小技巧，可以将n-argument 函数转换为n-tuple 上的函数，而不是(n+1)-tuples 被一个你会天真地理解的单元所覆盖。两个实例现在都按函数类型进行索引，实际测试的是结果类型是否为函数。

-- 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