Re: [Haskell-cafe] Is let special?
Max Bolingbroke schrieb: 2010/11/2 Günther Schmidt gue.schm...@web.de: 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is let special?
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. -- ryan On Thu, Nov 4, 2010 at 2:46 PM, Henning Thielemann schlepp...@henning-thielemann.de wrote: Max Bolingbroke schrieb: 2010/11/2 Günther Schmidt gue.schm...@web.de: 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is let special?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is let special?
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.
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.
If you are interested in the details, I'd suggest you to read the
original paper [damas1982principal].
Best regards,
Petr
@conference{damas1982principal,
title={{Principal type-schemes for functional programs}},
author={Damas, L. and Milner, R.},
booktitle={Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles
of programming languages},
pages={207--212},
year={1982},
organization={ACM},
url =
{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.122.3604rep=rep1type=pdf}
}
On Tue, Nov 02, 2010 at 02:34:29AM +0100, Günther Schmidt wrote:
Hi all,
is there something special about let? I don't mean only its use in
haskell, but in the general context of programming languages.
I've been given a few hints over time when I asked question
concerning DSLs but regretfully didn't follow them up.
Günther
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is let special?
2010/11/3 Petr Pudlak d...@pudlak.name: 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/index.htm ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is let special?
2010/11/3 Petr Pudlak d...@pudlak.name:
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
And just to be clear, this is specific to the H-M system. The function
f is typeable--but not inferable--in GHC-Haskell-with-extensions,
i.e. the definition:
{-# LANGUAGE Rank2Types #-}
f = ((\x - x x) :: forall a. (forall b. b - b) - a - a) (\y - y)
...is valid and will have the correct type for f. The more
restricted system provided by H-M is interesting largely because
everything typeable in it is also inferable.
- C.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is let special?
2010/11/2 Günther Schmidt gue.schm...@web.de: 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. Cheers, Max ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is let special?
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). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is let special?
Sorry, that was a mental note to myself :) / Emil 2010-11-02 12:41, Emil Axelsson skrev: 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). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Is let special?
Hi all, is there something special about let? I don't mean only its use in haskell, but in the general context of programming languages. I've been given a few hints over time when I asked question concerning DSLs but regretfully didn't follow them up. Günther ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is let special?
2010/11/2 Günther Schmidt gue.schm...@web.de: Hi all, is there something special about let? I don't mean only its use in haskell, but in the general context of programming languages. It means whatever the language specification/definition/implementation says it means. It's usually used for some kind of name binding however (there might be some language theory definition of let, but I wouldn't know). -- Ivan Lazar Miljenovic ivan.miljeno...@gmail.com IvanMiljenovic.wordpress.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Is let special?
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
