[Haskell-cafe] Type-indexed expressions with fixpoint
Brent Yorgey
byorgey at seas.upenn.edu
Mon Nov 9 18:09:21 EST 2009
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
More information about the Haskell-Cafe
mailing list