Maybe you are right on this, and I just misunderstood let-guards.

But with a non-recursive let, I would get a scope error instead of non-termination if I write

  let Just x | x > 0 = e ...

which I definitely prefer.

So, consider this aspect dropped from my proposal of non-recursive lets.

On 10.07.2013 09:44, Dan Doel wrote:
On Wed, Jul 10, 2013 at 3:08 AM, Andreas Abel <[email protected]
<mailto:[email protected]>> wrote:

    Another instance (cut-down) are let-guards like

       let Just x | x > 0 = e in x

    The "x > 0" is understood as an assertion here, documenting an
    invariant.  However, Haskell reads this as

       let Just x = case () of { () | x > 0 -> e } in x

    leading to non-termination.  A non-recursive version

       let' Just x | x > 0 = e in x

    could be interpreted as

       case e of { Just x | x > 0 -> x }

    instead, which is meaningful (in contrast to the current
    interpretation).


I still don't understand how this is supposed to work. It is a
completely different interpretation of guarded definitions that can only
apply to certain special cases.

Specifically, you have a let with one definition with one guard. This
lets you permute the pieces into a case, because there is one of
everything. But, if we instead have two guards, then we have two
possible bodies of the definition, and only one body of the let. But,
the case has only one discriminee (which comes from the definition
body), and two branches (which are supposed to come from the let body).
We have the wrong number of pieces to shuffle everything around.

The only general desugaring is the one in the report, but keeping the
non-recursive let. This means that the x in the guard refers to an outer
scope. But it is still equivalent to:

     let' Just x = case x > 0 of True -> e in x

     let' x = case (case x > 0 of True -> e) of ~(Just y) -> y in x

not:

     case e of Just x | x > 0 -> x

     case e of Just x -> case x > 0 of True -> x


--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

[email protected]
http://www2.tcs.ifi.lmu.de/~abel/

_______________________________________________
Haskell-prime mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-prime

Reply via email to