Type-level Polymorphism in haskell

Viewed 153

I'm working through the paper De bruijn notation as a nested datatype by Richard Bird and Ross Paterson. At one one point a fold operation over a term gets defined:

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)

... and further a generalized version that allows manipulations of the values of free vars:

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

Then the authors state that:

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.

and further they state, that for this reason we need one-off specialized functions like foldT above.

I was wondering what exactly type constructor polymorphism means in that context (something like full System F?) and if something like foldT v a l = gfoldT v a l id can be achieved by means of the newly added type level programming features like DataKinds, PolyKinds or TypeFamilies.

1 Answers
Related