haskell - Haskell 中的类型级多态性

Question

我正在研究论文 De bruijn notation as a nested datatype理查德·伯德和罗斯·帕特森。在某一时刻，定义了一项对一项的折叠操作:

infixl 9 :@

data Expr a =
      Var a
    | (Expr a) :@ (Expr a)
    | Lam (Expr (Maybe a)

foldT ::
    (forall a. a -> n a) ->
    (forall a. n a -> n a -> n a) ->
    (forall a. n (Maybe a) -> n a) ->
    Expr b -> n b
foldT v _ _ (Var x) = v x
foldT v a l (fun :@ arg) = a (foldT v a l fun) (foldT v a l arg)
foldT v a l (Lam body) = l (foldT v a l body)

...以及进一步的通用版本，允许操作自由变量的值:

gfoldT ::
    (forall a. m a -> n a) ->
    (forall a. n a -> n a -> n a) ->
    (forall a. n (Maybe a) -> n a) ->
    (forall a. (Maybe (m a)) ->  m (Maybe a)) ->    
    Expr (m b) -> n b                               
gfoldT v _ _ _ (Var x) = v x
gfoldT v a l t (fun :@ arg) = a (gfoldT v a l t fun) (gfoldT v a l t arg)
gfoldT v a l t (Lam body) = l (gfoldT v a l t (mapT t body))

然后作者声明:

In theory, we can take m = id, the identity type constructor, and so obtain foldT v a l = gfoldT v a l id . (...) However, type constructor polymorphism in haskell is limited, in that type constructor variables may only be instantiated to datatype constructors.

并且他们进一步声明，出于这个原因，我们需要一次性的专用函数，例如 foldT以上。

我想知道究竟是什么 type constructor polymorphism意味着在那种情况下(类似于完整的 System F ？)，如果类似于 foldT v a l = gfoldT v a l id可以通过新添加的类型级编程功能来实现，例如 DataKinds , PolyKinds或 TypeFamilies .

Answer 1

我认为这句话是指缺乏类型级 lambda 抽象。具体来说，以下在 Haskell 中是非法的。

data T m a = T (m a)

foo :: T (\t -> t) Int
foo = T 5

人们可能会尝试使用类型同义词或类型系列来规避这个问题，但没有成功。不允许出现以下情况:

type F t = t
foo :: T F Int
foo = T 5

这也不是:

type family F a
type instance F a = a
foo :: T F Int
foo = T 5

在 Haskell 中，类型方程 m Int ~ Int无解: m必须是数据类型构造函数。事实上，除其他外，编译器依赖于 m在统一期间是单射的，这很容易被任意类型级别的函数破坏。

但是可以使用 m ~ Identity并获得 Identity Int与 Int 不同，但同构。

目前，我相信 safe coercions不够强大，无法使用 Identity Int 强制类型进入直接使用的类似类型 Int .因此 Identity必须手动移除包装器以获得更简单的折叠类型。