haskell - 如何定义多变量箭头？

Question

这个问题与this earlier one有一定关系。 :

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

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

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

只要您只使用单参数函数，这种方法就很有效。但是，(普通箭头也有这个问题)，当您尝试创建具有多个参数的箭头时，您有以下选项。 (以(+) :: Int -> Int -> Int为例):

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

我知道可以定义一个“递归类型类”来创建一个多元函数，例如 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 参数函数转换为 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