[Haskell-cafe] Re: GADTs: the plot thickens?

[apfelmus at quantentunnel.de]

> Its partial inverse, "thickening" has the spec
> 
> thicken i i = Nothing
> thicken i (thin i j) = Just j
> 
>> thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n)
>> thicken Fz      Fz      = Nothing
>> thicken Fz      (Fs j)  = Just j
>> thicken (Fs i)  Fz      = Just Fz
>> thicken (Fs i)  (Fs j)  = fmap Fs (thicken i j) 

> [...]

> 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)

Isn't the problem simply that in the former 'thicken', the compiler can
not guarantee that the case

   thicken (Fs i)  Fz      = Just Fz

does never show up when we have 'thicken :: Fin (S Z) -> ...'? I mean
the subtle point about Fin is that 'Fz' is the "only" inhabitant of 'Fin
(S Z)'. At least, this is what Epigram can deduce. But due to _|_, every
constructor that is declared may appear in the form of

   Fs _|_

That's why only the latter 'thicken' can be correct.


Regards,
apfelmus