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 obtainfoldT 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.