February 2006 - Haskell-prime

RE: Bang patterns, ~ patterns, and lazy let
by Simon Peyton-Jones 08 Feb '06

08 Feb '06

| What have you got in mind? ANY tupling of bindings may change the SCC | structure, and hence the results of type inference--I'm taking that as | read. But that still leaves the question of whether the dynamic | semantics of the program is changed. Let's assume for the time being | that all bindings carry a type signature--then the SCC structure is | irrelevant, isn't it? Or am I missing something here? I'm under the | impression that the *dynamic* semantics of | | p1 = e1 | p2 = e2 | | *would* be the same as (p1,p2) = (e1,e2) under my strict matching | proposal. I don't see how the SCC structure can affect that. Well I put the example that you sent me on the Wiki, right at the bottom. Did I get it wrong? let { (y:ys) = xs; (z:zs) = ys } in body means case xs of (y:ys) -> case ys of (z:zs) -> body whereas let (y:ys, z:zs) = (xs,ys) in body means case (fix (\~(y:ys, z:zs). (xs,ys))) of (y:ys, z:zs) -> body which isn't the same. Simon

2 1

RE: Bang patterns, ~ patterns, and lazy let
by Simon Peyton-Jones 08 Feb '06

08 Feb '06

I've updated the Wiki to add your strict proposal, but rather briefly. If you want to add stuff, send it to me and I'll add it. Meanwhile: | And as a consequence, it is no longer possible to transform a pair of | bindings into a binding of a pair. In Haskell 98, | | p1 = e1 | p2 = e2 | | is always equivalent to | | (~p1, ~p2) = (e1,e2) In your strict proposal, I'm sure you hope that the above pair would be equivalent to (p1,p2) = (e1,e2) which would be even nicer. But sadly I don't think it is, because that'd change the strongly connected component structure. Somehow that smells wrong. Simon

2 1

RE: Bang patterns, ~ patterns, and lazy let
by Simon Peyton-Jones 08 Feb '06

08 Feb '06

| The trouble with those parts is that NOWHERE do they discuss how to | translate a let or where containing more than one binding. If they're | not to be translated via tupling, then how are they to be translated? Sorry I wasn't clear. Given let { p1 = e1; ... ; pn = en } in e0 (P1) For each pattern pi that is of form !qi = ei, transform it to xi@qi = ei and replace e0 by (xi `seq` e0) (P2) Now no pattern has a ! at the top. Now apply the existing rules in 3.12 of the Haskell report. So step (P1) above adds some seqs, and after that it's all just standard Haskell 98. My summary so far: 1) Bang patterns by themselves are quite decent, well-behaved patterns. 2) Rule (P1) is simple to describe. But the ! in a pattern binding is treated as part of the *binding* rather than part of the *pattern* which is wart-y. 3) There is a good argument to be made that pattern bindings should be strict by default. That is let (x,y) = e in b would evaluate e strictly. However that is *not* the same as saying that 'let' is strict. let x = e in b remains a lazy binding of x (because, as usual, a variable pattern matches without evaluation). 4) John argues that it would be bad to adopt bang patterns without also adopting (3). I don't agree. But I'm still attracted by (3). I will add some of this to the Wiki. Please do not treat it as "my" page --- any committee member can edit it. Simon

2 1

RE: Re[2]: Restricted Data Types
by Simon Peyton-Jones 08 Feb '06

08 Feb '06

| data Eq a => Set a = Set (List a) | | that is a sort of extension i will be glad to see. in my Streams | library, it's a typical beast and i forced to move all these contexts | to the instances/functions definitions: Another reasonable alternative is data Set a = Eq a => Set (List a) Operationally, a dictionary for (Eq a) is stored in the Set constructor along with the List a. Haskell (and GHC) doesn't allow this at the moment, but it would make perfect sense to do so, I think. The type of Set remains Set :: forall a. Eq a => List a -> Set a The type of member would become member :: a -> Set a -> Bool (with no Eq constraint). The typing rule for 'case' on a constructor with a context, like Set, would be to make the Eq dictionary available in the right-hand side of the case alternative: case e of { Set xs -> ....Eq a available in here... } I am not sure whether it would address all of the cases in John's paper, but it'd address some of them. It would be a significantly less radical step than Restricted Data Types I think. In particular, with GADTs imagine: data T where C :: forall a b. (Eq a, Num b) => a -> a -> b -> T b All Haskell compilers that support existentials will capture the (Eq a) dictionary, and make it available to the rhs of the case alternative. It would be weird not to capture the (Num b) dictionary in the same way. In short, a sensible design for GADTs will pretty much have to embrace this. GHC's implementation is trailing this a bit, I'm afraid, as GADT users will know. Making GADTs and type classes play nicely, particularly with a typed intermediate language, is interesting. Simon

3 2

RE: Bang patterns, ~ patterns, and lazy let
by John Hughes 08 Feb '06

08 Feb '06

> > From: Simon Peyton-Jones To: John Hughes ; haskell-prime(a)haskell.org Sent: Tuesday, February 07, 2006 11:37 PM Subject: RE: Bang patterns, ~ patterns, and lazy let Applying the rules on the wiki, the first step is to translate the first expression into a tuple binding, omitting the implicit ~: Not so! I changed it a few days ago after talking to Ben, to a simpler form that works nicely for recursive bindings too. Darn I forgot to change the rules at the bottom. Anyway, read the section “Let and where bindings”. Sorry about the rules at the end. Simon The trouble with those parts is that NOWHERE do they discuss how to translate a let or where containing more than one binding. If they're not to be translated via tupling, then how are they to be translated? The only relevant thing I could find was in the "modifications to the report" section at the bottom, which just tells you to omit implicit ~ when applying the tuplling rules in the report. So I don't understand how the semantics of multiple bindings is supposed to be defined (and I admit my proposal isn't so nice either). But more and more complex translations make me very nervous! I have a feeling there could be a nice direct semantics, though, including both ! and ~ in a natural way. Let's see now. Let environments be (unlifted) functions from identifiers to values, mapping unbound identifiers to _|_ for simplicity. The semantics of patterns is given by P[[pat]] :: Value -> Maybe Env The result is Just env if matching succeeds, Nothing if matching fails, and _|_ if matching loops. Two important clauses: P[[! pat]] v = _|_ if v=_|_ P[[pat]]v otherwise P[[~ pat]] v = Just _|_ if P[[pat]]v <= Nothing P[[pat]]v otherwise In definitions, pattern matching failure is the same as looping, so we define P'[[pat]]v = _|_ if P[[pat]]v = Nothing P[[pat]]v otherwise We do need to distinguish, though, between _|_ (match failure or looping), and Just _|_ (success, binding all variables to _|_). The semantics of a definition in an environment is D[[pat = exp]]env = P'[[pat]] (E[[exp]]env) (*) where E is the semantics of expressions. Note that this takes care of both ! and ~ on the top level of a pattern. Multiple definitions are interpreted by D[[d1 ; d2]]env = D[[d1]]env (+) D[[d2]]env where (+) is defined by _|_ (+) _ = _|_ Just env (+) _|_ = _|_ Just env (+) Just env' = Just (env |_| env') Note that (+) is associative and commutative. Let's introduce an explicit marker for recursive declarations: D[[rec defs]]env = fix menv'. D[[defs]](env |_| fromJust menv') Notice: This ignores the possibility of local variables shadowing variables from outer scopes. *Within defs* it makes no difference whether menv' is _|_ (matching fails or loops), or Just _|_ (succeeds with variables bound to _|_) If defs are not actually recursive, then D[[rec defs]]env = D[[defs]]env. Now let expressions are defined by E[[let defs in exp]]env = E[[exp]](env |_| D[[rec defs]]env) (this also ignores the possibility of local definitions shadowing variables from an outer scope). Too late at night to do it now, but I have the feeling that it should not be hard now to prove that E[[let defs1 in let defs2 in exp]]env = E[[let defs1; defs2 in exp]]env under suitable assumptions on free variable occurrences. That implies, together with commutativity and associativity of (+), that the division of declaration groups into strongly connected components does not affect semantics. I like this way of giving semantics--at least I know what it means! But it does demand, really, that matching in declarations is strict by default. Otherwise I suppose, if one doesn't care about compositionality, one could replace definition (*) above by D[[!pat = exp]]env = P'[[pat]](E[[exp]]env) D[[pat = exp]]env = P'[[~pat]](E[[exp]]env), otherwise But this really sucks big-time, doesn't it? John

1 0

Restricted Data Types
by Jim Apple 08 Feb '06

08 Feb '06

Have we considered Restricted Data Types? http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps Or even absracting over contexts, as described in section 7.5 (p. 14/15) of the above? Jim

5 8

RE: Bang patterns, ~ patterns, and lazy let
by Simon Peyton-Jones 07 Feb '06

07 Feb '06

Applying the rules on the wiki, the first step is to translate the first expression into a tuple binding, omitting the implicit ~: Not so! I changed it a few days ago after talking to Ben, to a simpler form that works nicely for recursive bindings too. Darn - I forgot to change the rules at the bottom. Anyway, read the section "Let and where bindings". Sorry about the rules at the end. Simon

1 0

Re: Bang patterns, ~ patterns, and lazy let
by John Hughes 07 Feb '06

07 Feb '06

>From: Ben Rudiak-Gould <Benjamin.Rudiak-Gould(a)cl.cam.ac.uk> >Subject: Re: Bang patterns, ~ patterns, and lazy let > >It's also not that case that !x has the same >meaning in both proposals, e.g. > > let { !x = y ; !y = const 'a' x } in x > >means 'a' in the current proposal but _|_ in yours. > > Aargh, you're right, it does mean _|_ in mine! That's not very nice. But wait, I'm not sure about let { !x = const undefined y ; !y = const 'a' x } in y desugars in the current proposal to let { x = const undefined y ; y = const 'a' x } in x `seq` y `seq` y which is _|_, but absent implicit ~, let { x = const undefined y ; y = const 'a' x } in y had better (and does) mean 'a'. Applying the rules on the wiki, the first step is to translate the first expression into a tuple binding, omitting the implicit ~: let (x,y) = (const undefined y, const 'a' x) in y This desugars to let (x,y) = fix (\ ~(x,y)->(const undefined y, const 'a' x)) in y which evaluates to 'a'. In other words, despite the ! on x, the current proposal is not strict in x. Maybe the intention was that !s on the lhs of let bindings should be transferred to the corresponding patterns when a tuple pattern is introduced? Let's try it: then the example desugars by pattern tupling to let (!x, !y) = (const undefined y, const 'a' x) in y Now we can introduce fix: let (!x, !y) = fix (\ ~(!x, !y) -> (const undefined y, const 'a' x)) in y and finally case: case fix (\~(!x,!y) -> (const undefined y, const 'a' x)) of ~(!x, !y) -> y and this is consistent with what you said above. But if I return to your first example, and do the same thing, I get let !x = y; !y = const 'a' x in x desugars by tupling to let (!x, !y) = (y, const 'a' x) in x which desugars by fix and case introduction to case fix (\ ~(!x, !y) -> (y, const 'a' x)) of ~(!x, !y) -> x The first approximation to the fixed point is _|_, so the second is (_|_, 'a'). Now, when ~(!x,!y) is matched against (_|_,'a') then *both* variables are bound to _|_ --- the effect of the ~ is just to delay matching (!x,!y) until one of the variables is used, but as soon as y, say, *is* used, then the match is performed and, of course, it loops. Thus (_|_, 'a') is the fixed point. For the same reason, x and y are both bound to _|_ in the body of the case, and so the entire expression evaluates to _|_, not 'a' as you claimed. Bottom line: I can't find a way to interpret the translation rules in the Haskell report, modified as the Wiki page suggests, to produce the results you expect in both cases. But maybe the fault is in the translation rules in the Haskell report. It was always rather tricky to explain a group of recursive bindings in Haskell in terms of a single tuple binding, because Haskell tuples are lifted. I see that you have a more direct understanding of what ! is supposed to mean. Is it possible, I wonder, to give a direct denotational semantics to a declaration group--say mapping environments to environments--in which there is only one case for ! (its natural semantics in patterns)? Such a semantics should have the property that let x1 = e1; x2 = e2 in e0 === let x1 = e1 in let x2 = e2 in e0 provided x1 does not occur in e2. Finding a simple and compositional denotational semantics with these properties, and proving the law above, would be a good way to show that ! patterns do NOT introduce semantic warts---and would probably also suggest that the semantics-by-translation used in the report is fundamentally flawed. We did construct denotational semantics of fragments of Haskell as part of the original design, and it had quite an impact on the result--I recommend it as a way of debugging ideas! John

1 0

Re: Restricted Data Types
by John Hughes 07 Feb '06

07 Feb '06

John Hughes wrote: >> That means that the Monad class is not allowed to declare >> >> return :: a -> m a >> >> because there's no guarantee that the type m a would be well-formed. The >> type declared for return has to become >> >> return :: wft (m a) => a -> m a > > I'm confused. It seems like the type (a -> m a) can't be permitted in any context, because it would make the type system unsound. If so, there's no reason to require the constraint (wft (m a)) to be explicit in the type signature, since you can infer its existence from the body of the type (or the fields of a datatype declaration). Correct, a -> m a can't be permitted anywhere. You're suggesting that wft (m a) be implicit therefore. The trouble is that ALL such contraints can't be implicit... there's an example in the paper showing a case where a constraint is needed on the type of a function to make its BODY well typed, but that constraint can't be inferred from the type alone. With your suggestion then, the programmer would need to write some, but not all, of the wft constraints. My suggestion was, in that case, that it's simpler and more consistent to write all. It's a design decision which could be made either way, of course, but writing all of them is my preference. Okay, simplify, simplify. How about the following: For every datatype in the program, imagine that there's a class declaration with the same name .... singleton :: a -> Set a becomes (internally) singleton :: (Set a) => a -> Set a and fmapM :: (Functor f, Monad m) => (a -> m b) -> f a -> m (f b) becomes fmapM :: (Functor f, Monad m, m b, f a, m (f b), f b) => (a -> m b) -> f a -> m (f b) ... Now you do type inference as normal, dealing with constraints of the form (tvar type+) pretty much like any other constraint. Does that correctly handle every case? I think this is the same as what I suggest, except that where I write wft (Set a), you write Set a and overload Set as both a type and a class. Again, that's a possible design decision one could take, but doesn't really simplify anything except perhaps the notation. John

1 0

RE: Restricted data types
by Simon Peyton-Jones 07 Feb '06

07 Feb '06

| >> Have we considered Restricted Data Types? | >> | >> http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps | > | | Finally, I wrote my paper before fundeps came on the scene. Some of the contortions I went through | in my simulation of RDTs could be avoided with the help of fundeps. A key point in the RDT paper, I think, was the ability to *abstract over a type class*. Now that is something one could consider adding to Haskell, as the SYB3 paper argues. (See my home page.) Suppose that one could abstract over a type class. How would the RDT paper change? I'm not sure. Simon

2 1