[Haskell-cafe] GADTs: the plot thickens?

[Conor McBride]

Hi Bruno

This looks like the stuff!

> Lets also have naturals reflected at the value level:
>
> > data Nat :: * -> * where
> >    Zero :: Nat Z
> >    Succ :: Nat n -> Nat (S n)

Good plan. Of course, if you combine this method with Pablo's 
suggestion, you can make the class RepNat n whose method is

  repNat :: Nat n

and then wrap your explicit versions in implicit versions. Implicit 
information inferred from type information but passed at run time: it's 
something we need to get used to. I'm glad we only need three 
definitions of the natural numbers, none of which is

  data Nat = Zero | Succ Nat

> Now we modify thin to take an extra Nat n (not needed, but just to 
> show the duality with thickening):
>
> > thin :: Nat n -> Fin (S n) -> Fin n -> Fin (S n)
> > thin n         Fz      i       = Fs i
> > thin (Succ n)  (Fs i)  (Fz)    = Fz
> > thin (Succ n)  (Fs i)  (Fs j)  = Fs (thin n i j)
>
> The thing to note here is that only:
>
> > thin (Succ n)  (Fs i)  (Fz)    = Fz
>
> is well typed; if you had the case:
>
> > thin Zero  (Fs i)  (Fz)    = Fz
>
> you get:
>
> Conor.lhs:28:21:
>     Inaccessible case alternative: Can't match types `S n' and `Z'
>     In the pattern: Fz
>     In the definition of `thin': thin Zero (Fs i) (Fz) = Fz
> Failed, modules loaded: none.

That's a relief. Of course, in Epigram, you get that n is a successor 
for free, the moment you look at an element of Fin n.

> Now lets go for the thickening function:
>
> > thicken :: Nat n -> Fin (S n) -> Fin (S n) -> Maybe (Fin n)
> > thicken n                Fz      Fz      = Nothing
> > thicken n                Fz      (Fs j)  = Just j
> > thicken Zero             (Fs i)  Fz      = Nothing
> > thicken (Succ _)         (Fs i)  Fz      = Just Fz
> > thicken (Succ n)         (Fs i)  (Fs j)  = fmap Fs (thicken n i j)
>
> Note that this version of thicken is more precise than the version you 
> had -- your third case splits into two
> different cases now. The problem is that when you had:
>
> > thicken (Fs i) Fz = ...
>
> you need to account for two possibilities: the first possibility is 
> (Fz :: Fin (S Zero)), to which you want to return Nothing
> and (Fz :: Fin (S (S n))) for which you can safely return Just Fz.

I thought that might work. Your solution is quite close to the Epigram 
version of the program, but you haven't covered the Zero (Fs i) (Fs j) 
case, which is impossible anyway. I suggest the following minor 
modification, whose significance is purely documentary.

 > thicken :: Nat n -> Fin (S n) -> Fin (S n) -> Maybe (Fin n)
 > thicken n                Fz      Fz      = Nothing
 > thicken n                Fz      (Fs j)  = Just j
 > thicken Zero             (Fs i)  j      =  undefined {- i stinks -}
 > thicken (Succ _)         (Fs i)  Fz      = Just Fz
 > thicken (Succ n)         (Fs i)  (Fs j)  = fmap Fs (thicken n i j)

The Epigram version explicitly refutes i in the case where it inhabits 
Fin Z. I thought of this example because of the other thread about empty 
cases.

> Let me know if that helps.

It certainly delivers the necessary explanation. What has happened here? 
Somehow, we discovered that we had to shift some data from the static 
language to the dynamic language so that we could give the compiler 
enough information to see what was ok about the program we started with. 
There's something subtle here. If the compiler just magically swallowed 
my earlier program, I think we'd lose type safety,
because it allows us to manufacture a non-_|_ inhabitant of (Fin Z)

  fromJust (thicken (Fs undefined) Fz) = Fz :: Maybe (Fin Z)

So you really need a safety check there. Another way to do it, crudely 
but avoiding the run time numbers, is this

 > thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n)
 > thicken Fz      Fz      = Nothing
 > thicken Fz      (Fs j)  = Just j
 > thicken (Fs Fz)  Fz      = Just Fz
 > thicken (Fs Fz)  (Fs j)  = fmap Fs (thicken Fz j)
 > thicken (Fs (Fs i))  Fz      = Just Fz
 > thicken (Fs (Fs i))  (Fs j)  = fmap Fs (thicken (Fs i) j)

That's just another way to get the strictness you need. Although it's 
ugly. Perhaps it's possible to pack up the explanation "every element of 
a finite set is an element of a nonempty finite set" as some sort of 
view, although not the sort of view currently being proposed, I guess.

Exactly what information is needed in which phase and how totality or 
its absence affects what's possible are interesting and subtle 
questions. We live in interesting times.

All the best

Conor