[Haskell-cafe] Type-indexed expressions with fixpoint

[Brent Yorgey]

Hi all,

This email is literate Haskell.  I'm struggling to come up with the
right way to add a fixpoint constructor to an expression language
described by a type-indexed GADT (details below).  Any suggestions,
comments, or pointers welcome.

> {-# LANGUAGE KindSignatures, GADTs #-}

Consider the following type-indexed GADT, which encodes descriptions
of polymorphic regular types:

> data U  :: (* -> *) -> * where
>   Unit  :: U None
>   Var   :: U Id
>   (:+:) :: U f -> U g -> U (Sum f g)
>   (:*:) :: U f -> U g -> U (Prod f g)
>
> data None a = None
> data Id a = Id a
> data Sum f g a = Inl (f a) | Inr (g a)
> data Prod f g a = Prod (f a) (g a)

Given u :: U f, thanks to the type indexing, we can write the
following function to enumerate all the shapes of a given size
described by u:

> enumShapes :: Int -> U f -> [f ()]
> enumShapes 0 Unit = [None]
> enumShapes _ Unit = []
> enumShapes 1 Var  = [Id ()]
> enumShapes _ Var  = []
> enumShapes n (f :+: g) = map Inl (enumShapes n f) ++ map Inr (enumShapes n g)
> enumShapes n (f :*: g) = [ Prod x y | x <- enumShapes n f, y <- enumShapes n g ]

But of course this isn't very interesting without adding a least
fixpoint constructor.  That is, I'd like to have something like

  data U  :: (* -> *) -> * where
    Unit  :: U None
    Var   :: U Id
    (:+:) :: U f -> U g -> U (Sum f g)
    (:*:) :: U f -> U g -> U (Prod f g)
    Mu    :: ???

  enumShapes n (Mu ...) = ...

But I am quite at a loss as far as expressing the type of Mu.  If the
GADT wasn't type-indexed, I'd just use HOAS, i.e.  Mu :: (U -> U) ->
U; but since Haskell doesn't have type-level lambdas, I don't see how
to make that work.

Suggestions greatly appreciated!  Pointing out that I am looking at
this in the wrong way (if you think such is the case) would be highly
appreciated as well.

thanks,
-Brent