As syntax, "let" goes back at least to ISWIM. As for there being something special, Milner's algorithm for type checking/inference in SML had to treat let specially.

Fundera på vad parentesen innebär. / Emil 2010-11-02 10:20, Max Bolingbroke skrev:

To recover this sharing, you either need some sort of observable sharing, or some common subexpression elimination (which risks introducing space leaks if your DSL has lazy semantics).

Max Bolingbroke schrieb:

2010/11/2 Günther Schmidt :

...

I've been given a few hints over time when I asked question concerning DSLs but regretfully didn't follow them up.

I think this is probably to do with observable sharing. The problem in DSLs is if you have:

fact :: Term -> Term fact = Factorial

instance Num Term where fromIntegral = Int (+) = Plus

e = let x = fact 2 :: Term in x + x :: Term

(Lets say the terms of our deeply embedded DSL are of type Term). If you pattern match on "e" you will get something like (Factorial (Int 2)) `Plus` (Factorial (Int 2)). This has lost the work sharing implicit in the original term, where the Factorial computation was shared.

To recover this sharing, you either need some sort of observable sharing, or some common subexpression elimination (which risks introducing space leaks if your DSL has lazy semantics). Quite a lot of papers have mentioned this issue: the one that springs to mind is Gill's "Type Safe Observable Sharing".

Actually, I often need some replacement for 'let' in EDSL's - a sharing 'let' on the level of the target language. So far I have solved such issues by Arrows (fact :: EDSLArrow Term Term). Others have solved it by searching and sharing common sub-expressions.

On Thu, 4 Nov 2010, Ryan Ingram wrote:

When you use arrows for your DSL, how do you avoid getting trapped by "arr"? It seems like it's hard to avoid people working arbitrary functions into your computation using it.

I use this for instance in synthesizer-llvm. Actually people can lift anything into the arrow, but in the end there is a run function that expects an arrow of type Arrow (Value a) (Value b) where (Value a) denotes a virtual LLVM register that holds a value with a type equivalent to the Haskell type 'a'. There are functions like (\a -> (a,a)) that can be lifted to the arrow and that make sense. But e.g. there is no (uncury (+)) for Value.

2010/11/3 Petr Pudlak :

However, from the typing point of view, it makes quite a difference. It is an integral part of the Hindley-Milner type inference algorithm, which is used by many functional languages. Consider the following two expressions:

...

f = (\x -> x x) (\y -> y) g = let x = \y -> y in x x

The function "f" is not typable in the Hindley-Milner type system, while "g" is is (and its type is "a -> a"). The reason is that in the first case (f), the typing system tries to assign a single type to "x", which is impossible (one would have to unify types "a" and "a -> b"). In the second case (g), the typing system assigns "x" a polymorphic type schema  forall a.a -> a which can be instantiated to both "a -> a" (the second "x") and "(b -> b) -> (b -> b)" (the first "x"), and then applied together. I'd say that "let ... in ..." is a core feature of the language that gives us parametric polymorphism.

Although this decision is not without problems. See the recent paper "Let should not be generalised" [1] -- ryan [1] Let should not be generalised, Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijvers; submitted to TLDI 2010. http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/ind...

On Wed, 2010-11-03 at 18:05 +0100, Petr Pudlak wrote:

Hi Günther,

from the semantical point of view, you can replace

...

let x = e' in e by (\x -> e) e' Both should evaluate to the same thing.

You also need (sometimes) fix function

let xs = 1:xs in xs

and

fix (\xs -> 1:xs)

Regards