Proposal: Non-recursive let

Proposal: add a non-recursive let to the Haskell language. In let' p = e in e' do { ... let' p = e ... } the variables of pattern p are then *not* in scope in e. Reasons for adding a non-recursive let: 1. recursive-let is the source for many non-termination bugs. An instance of such a bug is in the state monad of mtl-2.1 (forgive me, Edward, for quoting this again): http://hackage.haskell.org/packages/archive/mtl/2.1/doc/html/src/Control-Mon... state :: (s -> (a, s)) -> m a state f = do s <- get let ~(a, s) = f s put s return a here, a non-recursive let was meant, the s bound by the let was supposed to be a new state, shadowing the old state. However, since let is recursive, this actually causes a loop. 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). 2. Connected to 1., a non-recursive let allows for painless shadowing. For instance, the hack do ... x <- return $ f x exploiting non-recursiveness of the <- binding, would be unnecessary, instead we could write do ... let' x = f x NB: In a do-Block, we could drop the keyword let' and simply write do ... x = f x for a non-monadic binding, in accordance to x <- mf x, See also http://www.haskell.org/pipermail/beginners/2009-February/001075.html http://stackoverflow.com/questions/8398607/declaration-order-in-let-bindings... PS.: I can work out the details of grammar and semantics if this proposal finds followers. Cheers, Andreas -- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.abel@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/

On Wed, Jul 10, 2013 at 3:08 AM, Andreas Abel
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

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
mailto:andreas.abel@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@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/

Andreas Abel
Proposal: add a non-recursive let to the Haskell language. In
let' p = e in e' do { ... let' p = e ... }
the variables of pattern p are then *not* in scope in e.
Reasons for adding a non-recursive let:
1. recursive-let is the source for many non-termination bugs.
-1 from me. I don’t see that having non-recursive let available will have much impact on the bugs. It just changes forgetting to use different variable names because of recursion (which is currently uniform throughout the language) to forgetting to use non recursive let instead of let. -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk

On 10.07.2013 10:00, Jon Fairbairn wrote:
Andreas Abel
writes: Proposal: add a non-recursive let to the Haskell language. In
let' p = e in e' do { ... let' p = e ... }
the variables of pattern p are then *not* in scope in e.
Reasons for adding a non-recursive let:
1. recursive-let is the source for many non-termination bugs.
-1 from me. I don’t see that having non-recursive let available will have much impact on the bugs. It just changes forgetting to use different variable names because of recursion (which is currently uniform throughout the language) to forgetting to use non recursive let instead of let.
Sorry, but I cannot change history. Ideally, "let" was non-recursive, and we had a "let rec" to indicate recursion. I certainly am not going to propose to make "let" non-recursive. I am not buying your argument. I think it is easier to retrain the brain to use "let'" instead of "let" by default, because writing keywords is a background activity (like walking) and does not need the attention that thinking of the right variable needs. (My brain does confuse names, but not articles like "der" and "das".) Also, I want shadowing because then there are less variants of variables around that I can confuse. Shadowing is a way to clean out the name space, to dispose of things you do not need anymore. Cheers, Andresa -- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.abel@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/
participants (3)
-
Andreas Abel
-
Dan Doel
-
Jon Fairbairn