Re: "case" of an empty type should have no branches
* John Meacham [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 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
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 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
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
On 09.10.11 15:45, Felipe Almeida Lessa wrote: On Sun, Oct 9, 2011 at 8:26 AM, 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)" 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
Re: "case" of an empty type should have no branches
On Sun, Oct 9, 2011 at 8:26 AM, 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)" 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
"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