"case" of an empty type should have no branches

[John Meacham]

What are you trying to acomplish? A case doesn't necessarily force
evaluation in haskell depending on the binding pattern. for instance

case x of _ -> undefined will parse, but the function is still lazy in
x. it is exactly equivalant to

quodlibet x = undefined

If you want to actually enforce that quodlibet _|_ evaluates to _|_
then you want quodlibet x = x `seq` undefined. Though, that too is
technically equivalent in a theoretical sense, but may have practical
benefits when it comes to error messages depending on what you are
trying to acomplish.

  John

On Sun, Oct 9, 2011 at 4:26 AM, Roman Beslik <beroal at ukr.net> wrote:
> 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.
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>