Hi Connor,
A puzzle for you (and for me too). I just tried to translate an old Epigram favourite (which predates Epigram by some time) into GADT-speak. It went wrong. I had a feeling it might. I wonder how to fix it: I imagine it's possible to fix it, but that some cunning may be necessary. Here it is:
Type-level Nat
data Z = Z data S x = S x
Finite sets: Fin Z is empty, Fin (S n) has one more element than Fin n
data Fin :: * -> * where Fz :: Fin (S n) Fs :: Fin n -> Fin (S n)
To me, this looks more like ordinal numbers than like general finite sets: For each type-level natural number n, the set Fin n contains all object-level natural numbers k < n, where k = Fs^k Fz .
The "thinning" function: thin i is the order-preserving embedding from Fin n to Fin (S n) which never returns i.
thin :: Fin (S n) -> Fin n -> Fin (S n) thin Fz i = Fs i thin (Fs i) Fz = Fz thin (Fs i) (Fs j) = Fs (thin i j)
So ``thin Fz i'' is defined for i = undefined :: Fin Z. If you don't want this kind of effect, you might consider to keep the empty type away from your calculations:
{-# OPTIONS -fglasgow-exts #-} data Z = Z data S x = S x
data Fin :: * -> * where Fz :: Fin (S n) Fs :: Fin (S n) -> Fin (S (S n))
thin :: Fin (S (S n)) -> Fin (S n) -> Fin (S (S n)) thin Fz i = Fs i thin (Fs i) Fz = Fz thin (Fs i) (Fs j) = Fs (thin i j)
This gets me one line farther into thicken. But what is possible now: Add a lifting (or embedding) function:
lift :: forall n . Fin n -> Fin (S n) lift Fz = Fz lift (Fs i) = Fs (lift i)
thicken0 :: forall n . Fin n -> Fin n -> Maybe (Fin n) thicken0 Fz Fz = Nothing thicken0 Fz (Fs j) = Just (lift j) thicken0 (Fs i) Fz = Just Fz thicken0 (Fs i) (Fs j) = case (thicken0 i j) of Nothing -> Nothing Just k -> Just (Fs k)
I think that one ley to your trouble is the fact that there is, as far as I can see, no direct way to define a predicate determining whether an Fin (S n) element is the largest of its type:
isMax :: forall n . Fin (S n) -> Bool isMax = undefined
This would need a type case on Fz :: Fin (S Z) --- I'd dig through Oleg's posts about type equality checking. If you can make this possible, cou can also define
unlift :: forall n . Fin (S n) -> Maybe (Fin n) unlift = undefined
and get your original thicken from that. Wolfram