"case" of an empty type should have no branches

Roman Beslik beroal at ukr.net
Sun Oct 9 13:26:29 CEST 2011


Hi.

Why the following code does not work?
 > data Empty
 > quodlibet :: Empty -> a
 > quodlibet x = case x of
"parse error (possibly incorrect indentation)"

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.



More information about the Glasgow-haskell-users mailing list