Re: case of an empty type should have no branches
* John Meacham j...@repetae.net [2011-10-10 19:56:59-0700]
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.
In GHC, you need pseq for that. To quote the docs [1],
Note that we use pseq rather than seq. The two are almost equivalent,
but differ in their runtime behaviour in a subtle way: seq can
evaluate its arguments in either order, but pseq is required to
evaluate its first argument before its second, which makes it more
suitable for controlling the evaluation order in conjunction with par.
[1]: http://www.haskell.org/ghc/docs/latest/html/users_guide/lang-parallel.html
So, if, for some reason, the second argument of seq will be evaluated
first, you'll get an undefined error message.
On Sun, Oct 9, 2011 at 4:26 AM, Roman Beslik ber...@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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
--
Roman I. Cheplyaka :: http://ro-che.info/
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: case of an empty type should have no branches
On 2011-10-09 07:26, Roman Beslik wrote: Why the following code does not work? data Empty quodlibet :: Empty - a quodlibet x = case x of parse error (possibly incorrect indentation) It's a potential extension to ghc. See http://hackage.haskell.org/trac/ghc/ticket/2431 ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: case of an empty type should have no branches
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 ber...@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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
case of an empty type should have no branches
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@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: case of an empty type should have no branches
On Sun, Oct 9, 2011 at 8:26 AM, Roman Beslik ber...@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.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: case of an empty type should have no branches
On 09.10.11 15:45, Felipe Almeida Lessa wrote: On Sun, Oct 9, 2011 at 8:26 AM, Roman Beslikber...@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 is a solution. Thanks. I'd prefer to define something like data Finite = Zero | Plus Finite You just defined the set of natural numbers which is infinite. ;) ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
