[Haskell] Re: How to define tail function for Even/Odd GADT lists?
monnier at iro.umontreal.ca
Mon May 5 04:14:24 EDT 2008
> However, we were not able to write a function that returns the tail.
>> tailList :: Flip b c => List a b -> List a c
>> tailList (Cons _ xs) = xs
The problem here is that the caller will probably not know which "Flip
b c". OTOH the Cons of type "List a b" already contains a "Flip b c"
proof, so you really don't need to receive it.
Of course, in order to be able to write "List a c" you still need to
introduce a "c" variable somewhere. This should be done as follows:
tailList: List a b -> (Flip b c => List a c)
More information about the Haskell