Proposal: Non-recursive let

[Andreas Abel]

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 <andreas.abel at ifi.lmu.de
> <mailto:andreas.abel at ifi.lmu.de>> 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

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/