9 Oct
2011
9 Oct
'11
8:45 a.m.
On Sun, Oct 9, 2011 at 8:26 AM, Roman Beslik
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.