On 09/13/2010 12:23 PM, Michael Lazarev wrote:

2010/9/13 Henning Thielemann:

...

It means that variables bound by let, may be instantiated to different types later.

Can you give an example, please?

testOk = let f = id in (f 42, f True) --testNotOk :: Monad m => m (Int, Bool) --testNotOk = do f <- return id -- return (f 42, f True) Try uncommenting the 'testNotOk' definition.

On 09/13/2010 12:38 PM, Thomas Davie wrote:

On 13 Sep 2010, at 10:28, Gleb Alexeyev wrote:

...

On 09/13/2010 12:23 PM, Michael Lazarev wrote:

...

2010/9/13 Henning Thielemann:

...

It means that variables bound by let, may be instantiated to different types later.

Can you give an example, please?

testOk = let f = id in (f 42, f True)

--testNotOk :: Monad m => m (Int, Bool) --testNotOk = do f<- return id -- return (f 42, f True)

Try uncommenting the 'testNotOk' definition.

There's no "later" here at all.

Two seperate definitions in a Haskell program act as if they have always been defined, are defined, and always will be defined, they are not dealt with in sequence (except for pattern matching but that doesn't apply here).

Instead, what's going on here is scoping. The f in testOk is a different f to the one in testNotOkay, distinguished by their scope.

Finally, this is not how you use a let in a do expression, here's how you should do it:

testOk2 :: Monad m => m (Int, Bool) testOk2 = do let f = id return (f 42, f True)

I don't understand, I'm afraid. Michael Lazarev asked for example on the difference between let-bound and lambda-bound values. testNotOk definition mirrors the structure of the testOk definition, but testNotOk is, pardon my pun, not ok, because f is let-bound and, therefore, monomorphic, while f in the first definition is polymorphic. I never implied that definitions are processed in some sort of sequence, nor I stated that the two f's are somehow related.

Thanks

Tom Davie

On 09/13/2010 12:45 PM, Gleb Alexeyev wrote:

is, pardon my pun, not ok, because f is let-bound and, therefore, monomorphic

This line doesn't make sense, I was too hasty to hit the 'Send' button, I meant to write 'lambda-bound', of course, apologies for that.

On Sep 13, 12:22 pm, Michael Lazarev wrote:

Thanks for examples and pointers.

Since I came from Lisp, it never occurred to me that let and lambda are different constructs in Haskell.

You're not alone, I didn't believe my eyes when I first read about the difference (I learned Scheme, but the difference doesn't really matter here)

Prelude> :t (\f -> (f 42, f True))

<interactive>:1:10:     No instance for (Num Bool) [...] If I understand correctly, compiler first checks f 42, and deduces that f must be of type (Num a) => a -> b. Then it checks f True, and it does not satisfy the previously deduced type for f, because type of True is not in Num class.

That's a reasonable explanation - I don't know details about the order, and

:t (\f -> (f True, f 42)) gives the same mistake; I believe that type-checking is still in order (left-to-right or right-to-left, we can't say) but whether (Num t) and Bool is deduced first does not matter, because unifying them is commutative.

This works:

Prelude> :t (\f -> (f 42, f 41.9)) (\f -> (f 42, f 41.9)) :: (Fractional t1) => (t1 -> t) -> (t, t)

It just managed to deduce a type for f :: (Fractional t1) => (t1 -> t)

Yes, but that's not polymorphic in the sense people are using - ghc searched for a common type, and realized that there's a whole class of types where both 42 and 41.9 belong - Fractional.

And this, of course, works:

Prelude> let f = id in (f 42, f True) (42,True)

If I understand correctly again, it happens because f is a definition, which gets substituted to f 42 and to f True.

Almost true. In evaluating let a = b, b must be evaluated before binding it to a, and a value has a type. Actually, one can define the "substitution semantics" you describe, but interesting things happen then. Section 22.7 of Types and Programming Languages from Pierce discusses exactly this, in the context of ML* - I guess you can also Google for let-polymorphism. The real thing is that when you write "let f = id in", the type of a is deduced (internally "a -> a"), and then generalized (internally "forall a. a -> a"). The difference is that in the first case, GHC will try to discover what type "a" is by unifying it with the type of arguments of f - unification would produce type equations "a = Int, a = Bool" in the above example. The forall prevents that. Note that I wrote "internally", even if you can actually write both types (the second with an extension, IIRC) because in many cases when you write a top-level type-signature: f :: a -> a that is also implicitly generalized. * Note that in the end Pierce explains a problem with polymorphic references and its solution, but this does not applies to Haskell because of the lack of side effects (or you could say that unsafePerformIO does allow such things, and that's why it's not type- safe).

wren ng thornton wrote:

On 9/13/10 6:22 AM, Michael Lazarev wrote:

...

Thanks for examples and pointers.

Since I came from Lisp, it never occurred to me that let and lambda are different constructs in Haskell. I thought that let x = y in f is really (\x -> f) y It turns out that let is about declarations which are not the same as function applications above.

Right. This is a common mistake for people coming from Lisp, Scheme, and other untyped lambda calculi. In the untyped world it's fine to conflate let and lambda, because they only differ in how they're typed (and if you have no types...).

The difference is that, for let-bindings, once you've figured out a type of the variable being bound, then that type can be "generalized". The exact process of generalization has some subtle details to watch out for, but suffice it to say that certain type variables are allowed to become universally quantified. Which means that you're allowed to use x at different types within f, provided all those different types are consistent with the generalized type.

Whereas, lambda-bindings don't get generalized, and so they'll always be monomorphic (assuming Hindley--Milner inference without extensions like -XRankNTypes). This is necessary in order to catch numerous type errors,

Disclaimer: I am not a type system expert. Anyway, I thought the reason was that type inference for rank-n types (n>1) is undecidable. And therefore:

though Haskell lets you override this behavior by giving an explicitly polymorphic type signature if you have -XRankNTypes enabled.

...so that polymorphic types for arguments don't have to be inferred. I think it was in Milner's original paper where he tries to give some intuition why let and lambda are treated differently: even though we always have (\x -> e) y == let x = y in e which means that let can be translated to lambda, the converse is not true, since a lambda expression can appear in contexts other than (as the left hand side of) an application. Thus, let is syntactically more restrictive than lambda, which means we can be more liberal when typing it. In principle, the type-checker *could* be extended to infer polymorphic types for those lambda-bound variables where the lambda expression immediately gets applied to some other expression. In practice this would be of little use as these are exactly the situations where a let can (and should!) be used instead of a lambda. Cheers Ben

wren ng thornton wrote:

On 9/16/10 4:59 PM, Ben Franksen wrote:

...

even though we always have

(\x -> e) y == let x = y in e

which means that let can be translated to lambda, the converse is not true,

Not exactly. Note that when compilers do CPS conversion, everything is converted into let-binding and continuations (i.e., longjump/goto with value passing). It's just dual to the everything-is-lambda world, nothing special.

I meant "not possible" as in "by a source-to-source transformation in a simple core-ML-like language" (such as is used in most introductions to HM-style type inference). If you translate to a language with mutable state and/or built-in continuations then things are different, of course. Do you know a good online introduction to CPS conversion that explains the kind of duality you mentioned? Cheers Ben

wren ng thornton wrote:

On 9/17/10 4:04 PM, Ben Franksen wrote:

...

wren ng thornton wrote:

...

Note that when compilers do CPS conversion, everything is converted into let-binding and continuations (i.e., longjump/goto with value passing). It's just dual to the everything-is-lambda world, nothing special.

Do you know a good online introduction to CPS conversion that explains the kind of duality you mentioned?

Not off hand. These papers[1] give a pretty good explanation of CPS conversion and the other stages of compilation, from the perspective of proving compiler correctness. But they don't say much about the duality aspect of it. For the duality side of things, Andrzej Filinski's masters thesis[2] is an excellent read; though it doesn't say much about compilation IIRC.

Thanks, I'll take a look.

Basically the duality comes when decomposing a whole program. When we separate a term from its context, which part is in control? Control is just a perspective, so you could be outside the function looking in, or inside the function looking out. One person's push is another's pull. This is the same sort of thing as build/foldr vs unfoldr/destroy forms of list fusion: once we separate the F-algebra and F-coalgebra, which one should get the recursion?[3]

Ok, this gives me some vague intuition. Cheers Ben