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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
