- Haskell - Haskell.org

Implicit Parameters
by Koen Claessen 05 Feb '02

05 Feb '02

Hi all, Now we are talking about implicit parameters, let us take up the following problem with them on the Haskell mailing list too. Suppose I have the following function definition: app :: (?ys :: [a]) => [a] -> [a] app xs = case ?ys of [] -> xs (y:ys') -> y : (app xs with ?ys = ys') This function appends its argument to its implicit argument, by recursively changing the implicit argument. For example: Hugs> app [1,2] with ?ys = [3,4] [3,4,1,2] So far so good! Now, since Haskell has type inference, we can leave out the type signature: -- app :: (?ys :: [a]) => [a] -> [a] app xs = case ?ys of [] -> xs (y:ys') -> y : (app xs with ?ys = ys') Let us check if it still works again: Hugs> app [1,2] with ?ys = [3,4] [3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,{Interrupted!} And, stunningly, it doesn't! Why doesn't this work? That is because type inference assumes that the body of `app' is monomorphic, i.e. has no context in its type. Therefore, the recursive call to app where ?ys is changed, had no effect at all. It works with the type signature there, because in order to implement type checking (note: not type inference) with polymorphic recursion demands to use the stated type in checking the body of the function. Mark Shields, Simon Peyton-Jones, and I, and also Jörgen Gustavsson have been discussing several modest solutions to this (we believe it is not needed to do full type inference that can deal with polymorphic recursion to solve this problem). My questiona are: Were the designers of the implicit parameters paper aware of this problem when they wrote the paper? If so, they probably did not think this was a big problem. Do people in general think this is a problem? /Koen. -- Koen Claessen http://www.cs.chalmers.se/~koen Chalmers University, Gothenburg, Sweden.

3 2

Re: RFC: Syntax for implicit parameter bindings
by John Hughes 05 Feb '02

05 Feb '02

[Resent with permission of author -=chak] I'm beginning to find implicit parameters *extremely* useful, so I think it's important to get this right. I have some code that will have to change, but not as much as I will have in a couple of years...! I find adding a keyword to implicit parameter declarations, as in let dynamic ?base = 10 in addBase 5 or let nonrec ?base = 10 in addBase 5 just plain ugly. The question mark already indicates that this is an implicit parameter binding, there is no need for another keyword to say the same thing. This would make sense to me if implicit parameter names were lexically the same as other identifiers -- but THAT would be a big mistake! Without wanting to stir up language wars, this idea reminds me of ML rather than Haskell. One of the great strengths of Haskell's syntax, in my opinion, is just that it is so concise. Let's keep it that way! I am against let ?base := 10 in addBase 5 also -- not because := is already a constructor, but because I have another proposal for how to use it! From time to time I argue for a "monomorphic binding" operator, a substitute for the monomorphism restriction, which has become even more necessary with the addition of implicit parameters. (See my "Global Variables in Haskell" paper for a discussion and example). I'd like to reserve := for monomorphic binding. That leaves plain let bindings -- and in that case, why not also where, case, do, and lambda? There was also a mention of extending the implicit parameter story to work as recursive bindings, but I don't know any details here. It would certainly strengthen the case for using plain `let'. Why not recursive bindings? Why not mix implicitly bound variables and explicitly bound ones in the same pattern? This is surely the most orthogonal and powerful mechanism. The question is whether such bindings always have a clear meaning. I claim they do. For each implicitly bound variable ?x, let's assume that x is a fresh variable. Let e be an expression in the scope of ?x. Then I claim that replacing each such e by e with ?x = x and replacing the binding occurrence of ?x by x gives a sensible meaning to the extended language. For example, let ?fac n = if n==0 then 1 else n*fac? (n-1) in e means let fac n = if n==0 then 1 else n*fac? (n-1) with fac? = fac in e with fac? = fac And (\?x -> e) means (\x -> e with ?x = x) The only funny thing is that, because of the way implicit parameters are passed, their types cannot be generalised. John

2 1

Reference types
by Simon Peyton-Jones 05 Feb '02

05 Feb '02

For some time now, GHC and Hugs have had the following families of types and operations: data IO a data IORef a newIORef :: a -> IO (IORef a) readIORef :: IORef a -> IO a writeIORef :: IORef a -> a -> IO () data ST s a data STRef s a newSTRef :: a -> ST s (STRef s a) readSTRef :: STRef s a -> ST s a writeSTRef :: STRef s a -> a -> ST s () The basic bind operations etc are overloaded for IO and ST, but to overload the Ref operations one needs to add class RefMonad r m | r -> m, m -> r where newRef :: a -> m (r a) readRef :: r a -> m a writeRef :: r a -> a -> m () instance RefMonad IORef IO where ... instance RefMonad (STRef s) (IO s) where ... A multi-paramter type class is needed. Notice particularly the bidirectional functional dependencies. This is the only convincing example I know with functional dependencies going both ways. Or at least it was. But in a recent conversation with Peter Thiemann I realised that this is all baloney. There's a much easier type structure: data Ref m a -- References in monad m, values of type a newIORef :: a -> IO (Ref IO a) readIORef :: Ref IO a -> IO a writeIORef :: Ref IO a -> a -> IO () newSTRef :: a -> ST s (Ref (ST s) a) readSTRef :: Ref (ST s) a -> ST s a writeSTRef :: Ref (ST s) a -> a -> ST s () class RefMonad m where newRef :: a -> m (Ref m a) readRef :: Ref m a -> m a writeRef :: Ref m a -> a -> m () instance RefMonad IO where ... instance RefMonad (ST s) where ... No functional dependencies. No multi-parameter classes. Pure Haskell 98. All of this works for mutable arrays too, of course. I'm sending this to the Haskell list for several reasons. 1. It's a good lesson in "don't use a sledgehammer just becaues it happens to be to hand". 2. I'd be interested to know of any other examples you have of *bi-directional* functional depenencies. The above simplification nukes my only convincing example. (Usually one set of type variables determines another, but not vice versa.) Unless there's some technical flaw, this simpler type structure will be in the new hierarchical Haskell library structure. Simon

4 3

RE: Another Implicit Parameter Infelicity
by Simon Peyton-Jones 05 Feb '02

05 Feb '02

GHC treats implicit parameters as a type scheme, not a type. As it happens, John Hughes's message to the list today discusses exactly this point. Simon | -----Original Message----- | From: Ashley Yakeley [mailto:ashley@semantic.org] | Sent: 04 February 2002 21:14 | To: Simon Peyton-Jones; Haskell List | Subject: RE: Another Implicit Parameter Infelicity | | | At 2002-02-04 02:01, Simon Peyton-Jones wrote: | | >Neither GHC nor Hugs allow a polymorphic type variable | >(the argument of Maybe) to be instantiated to a polymorphic type. | >Systems which do are called 'impredicative' (or is it the other way | >around?). Going impredicative has big negative implications | for type | >inference, and I have always steered well clear! | | That's not what's happening here with implicit parameters, is | it? No type | variable is being instantiated. | | I'm pretty sure this does not need impredicativeness: | | p :: forall a. Maybe ((?param :: a) => a) | p = return g; | | It's more or less equivalent to this: | | p :: forall a. Maybe (a -> a) | p = return g; | | ...and not to be confused with this: | | p :: Maybe (forall a. a -> a) | p = return g; | | Or am I misunderstanding something? | | -- | Ashley Yakeley, Seattle WA | |

1 0

Re: why is this legal
by Antony Courtney 05 Feb '02

05 Feb '02

David Feuer wrote: >>From: Hal Daume III <hdaume(a)ISI.EDU> >> > >>then, why are we allowed to rebind f in a let clause :) >> > > 1. There is no real reason not to allow this, Hmmm. I thought Hal gave a fairly real reason: f x = f' 0 x where f' acc [] = acc f acc (x:xs) = f' (x+acc) xs This example has a notoriously difficult to spot one character typo that causes the whole program to do something other than what the programmer intended at runtime. > so such a > rule would just limit the flexibility of the language and > annoy programmers. It would also make it somewhat harder > to write compilers, because they would have to check > uselessly for violations of an extra rule. > You know, this is exactly the kind of argument used by a Scheme programmer to tell us why static type systems are bad. :-) I hope you share my (subjective) view that such complaints are bogus if we are talking about static type systems. If so, and if you will forgive a terrible pun, why do you think it's ok for the compiler to catch type errors, but not typing errors? (*GROAN*....couldn't resist, sorry.) > 2. It increases the ability to move code around without > changing it. For example, suppose you have > [...] > There is another, possibly more significant reason, > however: sometimes it is very nice to be able to "shadow" > an external variable Yes, these are all valid uses, which is why I would favor having the compiler emit a warning in such circumstances. Interestingly, this is exactly what gcc does if you shadow a parameter with a local variable in a function in C: int f(int y) { int y = 20; return y + 10; } $ gcc -c shadow.c shadow.c: In function `f': shadow.c:4: warning: declaration of `y' shadows a parameter $ Many in the Haskell community disagree with me, but I find compiler warnings such as the above immensely helpful. They are a way for the compiler to say to the programmer, "Your program has a reasonable meaning, but you used some dangerous construct so that what you said might not have been what you meant." Of course, good compilers/tools will let you turn such warnings on and off selectively, and good programmers write programs that compile without warnings (since warnings usually indicate dubious constructs). While the examples you give are valid, I'm not convinced they are common enough that a warning would become a nuisance. -antony -- Antony Courtney Grad. Student, Dept. of Computer Science, Yale University antony(a)apocalypse.org http://www.apocalypse.org/pub/u/antony

4 4

Re: Implicit Parameters
by John Hughes 05 Feb '02

05 Feb '02

On Monday 04 February 2002 02:25 am, John Hughes wrote: > Not so fast! Proposing a "solution" means this is regarded as a "problem"! > But what is to say that the first behaviour is "right" in any general > sense? > > The important thing is that the language semantics is clear, and this is a > semantic question. The static semantics of Haskell *is* clear: recursive > calls are monomorphic unless a type signature is given; this is the basis > for understanding the behaviour above. I think part of the problem is that we've confused implicit parameterisation with polymorphism. Haskell has a two-level type system with monomorphic types at the bottom level, and polymorphic and qualified types at the second level. It turned out to be very straightforward to add implicit parameters to Haskell by treating them as a special kind of qualified type, and thus they also play according to the rules of polymorphic types - i.e. you `capture' implicit parameters exactly when you generalize a polymorphic definition. However, Koen's example suggests that maybe implicit parameters shouldn't necessarily play according to the rules of polymorphic types. Perhaps implciit parameters should be a special kind of monomorphic type instead. If this were the choice, then it's clear that they should be captured by recursive definitions. Yes, if one asks in isolation whether implicit parameters should belong at the type level or the type scheme level, then it might seem reasonable to make either choice. but bear in mind that the type/type scheme distinction is also tied in with type inference. Namely, inferred types cannot contain nested type schemes, only declared types may do so. (GHC's recent extension beyond rank 2 types doesn't change this basic fact). If implicit parameters were to be moved to the type level, then it should also be possible to infer types containing them in nested positions. For example, f x = (x with ?y = 1) + 1 should receive the inferred type f :: (Num a, Num b) => (?y :: a => b) -> b What happens to principality? Even if there are principal types, can type inference still be done fast (feels like inference in the presence of subtypes)? These are hard questions! I would be AGAINST moving implicit parameters to the type level, without solving the inference problem satisfactorily. That would give Haskell three sorts of types: inferrable types (no implicit parameters in nested positions) declarable monomorphic types (nested implicit parameters) type schemes (And now, of course, one may wonder what kind of monomorphism the M-R refers to...). Two sorts of types is, in my view, already enough. John

1 0

RFC: Syntax for implicit parameter bindings
by Manuel M. T. Chakravarty 04 Feb '02

04 Feb '02

Dear Haskell Folks, I am sure you are fully aware that the most painful decisions that a language designer has to make are those concerning the syntax of the language. Earth shattering disputes have been fought over the syntax of programming languages with equals only in arguments over the monomorphism restriction...and, well, maybe also n+k patterns. In a previously closed discussion concerning the syntax of implicit parameter bindings, it has been suggested to lay the facts open to your scrutinising eyes, in the hope that a wise decision will emerge. The Status Quo ~~~~~~~~~~~~~~ Given a function that requires an implicit parameter addBase :: (?base :: Int) Int => Int addBase x = x + ?base both GHC and Hugs currently support implicit parameter bindings using syntax based on the keyword `with', as in addBase 5 with ?base = 10 For the motivation behind implicit parameters and their semantics, please see Lewis et al's POPL paper <http://www.cse.ogi.edu/~jlewis/implicit.ps.gz>. The Problem ~~~~~~~~~~~ Both GHC and Hugs support implicit parameters only when a command line option is given that instructs them to enable language extensions that go beyond Haskell 98. However, as soon as this command line option, which activates all sorts of extensions, is given, `with' suddenly becomes a keyword and any Haskell code that uses `with' as a variable name fails to parse. Given that `with' is a quite short and rather common word, this problem is hard to neglect. In particular, the XML library HaXML and the libraries in the FFI Addendum use `with' for function names, which would be awkward to change. Now, given that implicit parameters are a - I believe - rarely used extension, can't we just change the keyword to something else and be done with it? We could, but implicit parameters are an eminently useful feature that may well be formalised into a Haskell 98 addendum, or even be included in a future revision of the language. So, it seems worthwhile to spent some thought on how to solve the problem properly. In addition to the keyword problem, `with' doesn't fit very well in with other Haskell binding constructs, which are in prefix form and extend as far to the right as possible (eg, `let', `case', and lambdas). This, for example, raises the questions what let x = e1 in e2 with ?y = e3 might mean. (The exception to prefix form is `where', but it scopes over groups of right-hand sides, not expressions.) Possible Solutions ~~~~~~~~~~~~~~~~~~ [Ugly & easy] The `with' keyword could be renamed to `iwith' or a prefix form could be called `ilet' or `dlet' (the last of which is actually accepted by Hugs as an alternative syntax). [Just use let] Alternatively, it seems reasonable to reuse the existing `let' syntax. So, our above example would read let ?base = 10 in addBase 5 The problem here is that let-bindings are recursive and introduce polymorphic bindings, which doesn't match well with the semantics for implicit parameters. This is aggravated by the ability to mix bindings of implicit parameters with standard variable and function bindings. These problems could be avoided by defining that a let binding either exclusively contains implicit parameter bindings or none at all. Moreover, all implicit parameter bindings are non-recursive and not subject to generalisation during type checking. This is a simple and workable solution, but some people feel that merely having a `?' on the lhs of bindings provides to little visual clue for a semantics that deviates quite strongly from standard `let' bindings. [Add a special identifier] To emphasis the difference in semantics, we may add a special identifier[1] after the let, such as let dynamic ?base = 10 in addBase 5 or let nonrec ?base = 10 in addBase 5 where `nonrec' would have the advantage that it might also be used for explicit value bindings where they are meant to be non-recursive (just like plain `let' in SML). The main disadvantage of this solution is that, in Haskell, some keywords (`let', `case', `where', and `do') trigger the layout rule and now `dynamic' or `nonrec' would have to trigger the layout rule, but *only* when appearing after a `let'. *urgh* [Use a special binding operator] An alternative way to emphasis the non-standard semantics for `let's containing bindings for implicit parameters would be to use a binding operator other than `='; for example, let ?base := 10 in addBase 5 Unfortunately, `:=' is currently a valid infix constructor symbol and making it into a reserved operator is probably as bad as making `with' into a reserved identifier. On the other hand, like the `nonrec' special identifier, the syntax could also be used for explicit value bindings. Are there other, better alternatives for the binding operator? There was also a mention of extending the implicit parameter story to work as recursive bindings, but I don't know any details here. It would certainly strengthen the case for using plain `let'. In Summary ~~~~~~~~~~ We want implicit parameters, but we also want to avoid turning common identifiers into keywords, thus, stealing them from library designers. It seems best to render bindings of implicit parameters as a variant of `let' bindings. The question is, which syntax do we choose for this. The arguments and examples in this message are a summary of mail messages and verbal discussion between Marcin Kowalczyk, John Launchbury, Jeff Lewis, Simon Marlow, Erik Meijer, Sven Panne, Simon Peyton Jones, Alastair Reid, and my humble self. Cheers, Manuel [1] A special identifier is *not* a keyword. It is special only in some contexts (in this case, after a `let'). Everywhere else, it can be used as a normal identifier.

4 3

Re: RFC: Syntax for implicit parameter bindings
by Ashley Yakeley 04 Feb '02

04 Feb '02

At 2002-02-04 01:45, Koen Claessen wrote: > | addBase{?base=7} 5 > >I like this! It is the least polluting syntax of all. Hmm... you have braces without following a keyword. I think in all other cases, braces follow a keyword (where, let, do, of). -- Ashley Yakeley, Seattle WA

2 1

New haskell.org policies
by John Peterson 04 Feb '02

04 Feb '02

Our switch to a new server for haskell.org is complete. We are making a few changes in the way this machine is administered - instead of handing out the root password we are now using sudo instead. Anyone who used needs root access and is not a sudoer can contact me and I'll fix things. Some changes on the web pages made last week might be missing - if anyone has a problem I can help restore things. Finally, we now have far more disk space on haskell.org. I would encourage anyone with Haskell-related projects to consider using haskell.org for distributions, mailing list, and anything else you need. Contact me if you need more information about getting an account. John Peterson

1 0

RE: Another Implicit Parameter Infelicity
by Ashley Yakeley 04 Feb '02

04 Feb '02

At 2002-02-04 02:01, Simon Peyton-Jones wrote: >Neither GHC nor Hugs allow a polymorphic type variable >(the argument of Maybe) to be instantiated to a polymorphic >type. Systems which do are called 'impredicative' (or is it the >other way around?). Going impredicative has big negative >implications for type inference, and I have always steered well clear! That's not what's happening here with implicit parameters, is it? No type variable is being instantiated. I'm pretty sure this does not need impredicativeness: p :: forall a. Maybe ((?param :: a) => a) p = return g; It's more or less equivalent to this: p :: forall a. Maybe (a -> a) p = return g; ...and not to be confused with this: p :: Maybe (forall a. a -> a) p = return g; Or am I misunderstanding something? -- Ashley Yakeley, Seattle WA

1 0