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