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