haskell中的非法多态或限定类型

haskell不支持非指示性类型,特别是不允许 forall 出现在任何类型构造函数下(除了 -> )

例如, Maybe (forall a. a), [forall a. a->a], ((forall a. a), Bool) 是被禁止的。

使用A newtype 包装如果你想要的话。

newtype T = T (forall a. a->a)
foo :: [T] -- OK
foo = [T id]

出于好奇,你想用这种类型做什么?它看起来像一个连接的组合子的类型 quote 这样 [X] quote == [[X]] (有时被称为 unit )换句话说,它在堆栈顶部获取一个值,并将其包装在一个函数中,应用该函数时,将该值推送到堆栈。

这里有一个过去用于这种功能的表示。这个 Tupled 类型族将类型列表转换为嵌套元组以表示堆栈。

-- Tupled '[t1, t2, ..., tn] s == (t1, (t2, (... (tn, s))))
type family Tupled ts t where
  Tupled '[] t' = t'
  Tupled (t ': ts) t' = (t, Tupled ts t')

使用 newtype 包装器我们可以使一个函数(具有特定的输入和输出数量)在堆栈的其余部分具有多态性。

newtype as :-> bs = Fun (forall s. Tupled as s -> Tupled bs s)

这是标准的隐藏方式 非指示性多态性 ,即,使用 forall -类型构造函数(而不是函数箭头)下的量化类型 (->) ,就像你想写的那样 (forall r. (r -> (a, r)), s) . Haskell不直接支持这个,但是如果您使用 新类型 包装器,编译器知道何时引入和消除 福尔 .

打开这个 新类型 并将其应用于堆栈类型,我们可以将包装函数应用于堆栈。

apply :: forall z as bs. (as :-> bs) -> Tupled as z -> Tupled bs z
apply (Fun f) as = f @z as

这个 引用 Combinator在函数中包装堆栈的顶部元素:

quote :: forall a s. (a, s) -> ([] :-> '[a], s)
quote (a, s) = (Fun $ \s' -> (a, s'), s)

unquote 将堆栈上的函数应用于堆栈的其余部分。

unquote
  :: forall z as bs s
  .  (Tupled as z ~ s)
  => (as :-> bs, s)
  -> Tupled bs z
unquote (f, s) = apply @z f s

(注意等式约束 Tupled as z ~ s ,这意味着输入堆栈类型 s 必须以一系列类型开头 as ,剩下的就叫做 z 艾尔.

add 是加法运算符 (+) 提升到堆栈;它只是添加堆栈的前两个元素。

add :: forall a. (Num a) => '[a, a] :-> '[a]
add = Fun $ \ (x, (y, s)) -> (x + y, s)

现在,引用和取消引用一个元素,它将保持不变:

unquote (quote ("hello", ()) == ("hello", ())

加法函数可以直接应用

apply add (1, (2, ())) == (3, ())

或者放在堆栈上然后应用。

unquote (add, (1, (2, ()))) == (3, ())

这需要以下扩展:

• DataKinds 允许类型级别的类型列表

• RankNTypes 和 ScopedTypeVariables 允许显式 福尔 并将类型变量带入作用域,以便我们可以使用 TypeApplications ,因为我们需要 AllowAmbiguousTypes 将指定“堆栈”类型推迟到调用站点,如 apply @z f as

• TypeFamilies 启用 元组 类型族

• TypeOperators 给这个漂亮的象征性名字 :-> 包装函数类型