"case" of an empty type should have no branches
Felipe Almeida Lessa
felipe.lessa at gmail.com
Sun Oct 9 14:45:13 CEST 2011
On Sun, Oct 9, 2011 at 8:26 AM, Roman Beslik <beroal at ukr.net> wrote:
> Why the following code does not work?
>> data Empty
>> quodlibet :: Empty -> a
>> quodlibet x = case x of
> "parse error (possibly incorrect indentation)"
Works for me:
data Empty
quodlibet :: Empty -> a
quodlibet x = case x of _ -> undefined
> This works in Coq, for instance. Demand for empty types is not big, but they
> are useful for generating finite types:
>> Empty ≅ {}
>> Maybe Empty ≅ {0}
>> Maybe (Maybe Empty) ≅ {0, 1}
>> Maybe (Maybe (Maybe Empty)) ≅ {0, 1, 2}
> etc. Number of 'Maybe's = number of elements. I can replace @Maybe Empty@
> with @()@, but this adds some complexity.
I'd prefer to define something like
data Finite = Zero | Plus Finite
Cheers, =)
--
Felipe.
More information about the Glasgow-haskell-users
mailing list