haskell中的类型级多态性

Question

我正在通过Richard Bird和Ross Paterson 的文章De Bruijn表示法作为嵌套数据类型.在一个点上,定义了一个术语的折叠操作:

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

然后作者说:

从理论上讲,我们可以采用m = id身份类型构造函数等方式获取foldT v a l = gfoldT v a l id.(...)但是,haskell中的类型构造函数多态性是有限的,因为类型构造函数变量只能实例化为数据类型构造函数.

他们进一步指出,由于这个原因,我们需要像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,但同构.

目前,我认为安全强制不足以强制使用Identity Int类型直接使用的类型Int.因此,Identity必须手动移除包装器以获得更简单折叠的类型.