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

Question

为什么 Haskell 在尝试解析此类型签名时抱怨？

f :: (a,s) -> (forall r.(r -> (a,r)),s)

Answer 1

Haskell 不支持谓词类型，特别是不允许 forall 出现在任何类型构造函数下（-> 除外）。

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

如果需要，请使用 newtype 包装器。

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

Answer 2

出于好奇，你想用这个类型做什么？它看起来像 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 不直接支持这一点，但是如果您使用 newtype 包装器，那么编译器会确切知道何时引入和消除 forall.

通过展开此 newtype 并将其应用于堆栈类型，我们可以将包装函数应用于堆栈。

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

quote 组合子将栈顶元素包装在一个函数中：

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 允许显式 foralls 并将类型变量引入作用域，以便我们可以使用 TypeApplications 引用它们，因为我们需要 AllowAmbiguousTypes 将指定“堆栈”类型推迟到调用站点，如 apply @z f as
TypeFamilies 启用 Tupled 类型系列
TypeOperators 为包装的函数类型提供漂亮的符号名称 :->

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

Illegal polymorphic or qualified type in Haskell

haskell

higher-rank-types