Proposal: Non-recursive let
Andreas Abel
andreas.abel at ifi.lmu.de
Wed Jul 10 11:03:17 CEST 2013
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/
More information about the Haskell-prime
mailing list