# Proposal: Non-recursive let

Dan Doel dan.doel at gmail.com
Wed Jul 10 09:44:49 CEST 2013

```On Wed, Jul 10, 2013 at 3:08 AM, Andreas Abel <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.
>
>   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
-------------- next part --------------
An HTML attachment was scrubbed...