0. Introduction This is a complete rewrite of my implicit-parameter proposal, with a lot more motivating text and examples, as well as discussions of the tradeoffs involved in making various changes to the existing system. It incorporates various changes which came up in the discussion which followed my original post, as well as some which haven't been posted before. This document is pretty dry, which is deliberate; I'm trying to write a research paper this time instead of flippantly tossing out an idea. If you're not interested in the theory you can skip to section 3, where I lay out my specific suggestions for changes to the existing implementations. 1. The new framework I will develop the idea of implicit parameters using a different approach from that of the original paper by Lewis et al. (hereafter "LSML"). In my approach implicit parameters will be treated directly as implicitly- propagated function parameters, and not via an analogy with LISP's dynamic environment. I think that this new approach, by more closely modeling the way implicit parameters really work, suggests reasonable solutions to a variety of problems which are difficult to analyze within the LSML framework. It also raises some new questions which, though they apply to LSML also, may not have been noticed before. 1.1. Explicit labeled parameters Implicit named parameters differ from ordinary parameters in two ways: they are implicit (i.e. automatically propagated through function calls in some way), and they have names instead of ordinal positions. I will introduce these two properties into the language separately. First we consider explicit (or "ordinary") labeled parameters. I'll start with some examples to illustrate their expected behavior, as well as the new syntactic forms that I'll be using for them in this document: cons {head = h} {tail = t} = h : t \ cons {tail = t} {head = h} = h : t > all equivalent defs. cons {head = h, tail = t} = h : t / cons {head = 'h'} {tail = "ello"} ==> "hello" cons {tail = "ello"} ==> partially-applied function cons 'h' "ello" ==> error cons {tail = "ello"} {head = 'h'} ==> "hello" cons {tail = "ello", head = 'h'} ==> "hello" cons :: (head :: a, tail :: [a]) => [a] cons {head = 'h'} :: (tail :: String) => String elem :: (predicate :: a -> b -> Bool) => a -> [b] -> Bool elem item list {predicate = p} = ... \ elem item {predicate = p} list = ... > all equivalent elem {predicate = p} item list = ... / In function definitions, labeled parameters have two identifiers associated with them: the one on the left of the {...=...} form is the external (interface) name, or label, which appears in the type and is used by other functions to refer to the formal parameter, while the one on the right is the internal (implementation) name, which is used within the function to refer to the actual argument. Ordinary positional parameters have only the internal name. Since these two kinds of identifiers never appear in the same context, they may be placed in different namespaces. In particular, we may without ambiguity introduce a "punning" notation for function definitions, such as cons :: (head :: a, tail :: [a]) => [a] cons {head, tail} = head : tail However, aside from being potentially confusing, punning causes notational difficulties because it interferes with alpha-conversion (internal names must sometimes be renamed, but labels must never be renamed). I will not use punning in this document. Note that internal bindings have lexical extent, while labels have global extent. 1.2. Implicit parameters When we write a declaration such as mysort list = sortBy ?comparator list the explicit parameter "list" is mentioned twice, once at its abstraction or binding point and once at its reference or usage point. However, the implicit parameter introduced by "?comparator" is mentioned only once, at the reference point. We expect the corresponding abstraction to be propagated automatically toward the root of the expression tree, where "list" is already explicitly mentioned. Then, at call time, the actual argument should be propagated down again, along the same path, to the point of use. Secondly, when we write something like myWeirdSort list = sortBy ?comparator list ++ reverse (sortBy ?comparator list) we expect the two ?comparator forms to denote a single implicit argument. That is, the implicit abstractions should be merged by name as they're propagated up. This is not the only possible behavior; one can envision an implicit-parameter system in which equally-named labels are kept separate, as in section 2.1. Probably such a system wouldn't be useful; at any rate I won't consider it here. 1.3. Auto-lifted labels With this motivation, I introduce a special kind of label which I'll call "auto-lifted". Auto-lifted labels are like ordinary labels except that, when used in lambda abstractions, they behave as described above, propagating upward in the function and merging by name. I will distinguish auto-lifted labels with a prefix @. (I can't use ? because auto-lifted labels are not quite the same as implicit parameters -- see below.) For example, when we have an application node [F][X] in which [F] has auto-lifted parameters @p and @q and [X] has auto-lifted parameters @q and @r, we effectively convert the application node to this: \{@p=a,@q=b,@r=c} -> ([F] {@p=a,@q=b} ([X] {@q=b,@r=c})) At other node types, the implicit parameter abstractions behave as you might expect: they propagate out of the body of a let (but see section 2.8), and they rise out of the scrutinee and alternatives of a case statement (merging by name). The net effect of all this is that the abstraction barrier of each auto-lifted parameter expands to encompass more and more of the expression, until it reaches either the top level of the function or an explicit binding. In the former case it will "infect" and propagate upward through any other function which uses this one. When the node is a labeled application of an auto-lifted parameter, we have to be careful not to lift that parameter from the LHS, since it's bound at this node and shouldn't be lifted any further. Rank-2 contexts have to be treated specially too (see section 2.9). It's worth noting that it's only really necessary to lift the parameters on the RHS of the application. Haskell already has a sort of implicit parameter mechanism for left-hand sides: when we write code like sum = foldl (+) 0 the unmentioned third parameter of foldl automatically becomes a parameter of sum. The same happens to labeled parameters, auto-lifting and otherwise. Ashley Yakeley pointed out that instead of assuming this special behavior at application nodes, we can just allow functions to be specialized in another way, from a -> b to (@x :: c) => a -> ((@x :: c) -> b). I won't use this formulation because it doesn't extend as naturally to linear implicit parameters (section 2.10). 1.4. The ?x notation In terms of auto-lifted labels, the familiar implicit parameters ?x behave as follows: * As an expression, ?x is equivalent to \{@x=t} -> t (that is, the identity function with an auto-lifting labeled parameter). * On the left of the equal sign in {...=...} notation, and in type signatures, ?x is equivalent to @x. It's interesting that in this framework ?x appears to be overloaded: it denotes a label in one context and a function in another. Also interesting is that the function is a closed lambda form which makes no reference to its environment. So "?x" is very different from "x". 2. Extensions, problems, solutions, unresolved questions 2.1. Duplicate labels It is possible for a function's interface to include two or more explicit parameters with the same label, as in f {arg = x} {arg = y} z = x+y+z or more subtly f {arg = x} = g ... g {arg = y} z = y+z Theoretically the definition and use of such functions seems to be unproblematic: indeed, permitting them actually simplifies the denotational semantics. There are some practical problems with this idea, however. I'll expand on this section if there's interest in adding explicit labeled parameters to Haskell. The question of duplicate names does not arise in the case of implicit parameters, because of their merge-by-name behavior. 2.2. Custom applications Haskell provides a convenient infix operator ($!) for strict application. Unfortunately, there seems to be no way to extend an operator of this kind to labeled application; the best you can do is define a new operator for each label, which is almost certainly a waste of time. This is really a special case of the general issue that functions with labeled arguments can't be passed to higher-order functions expecting positional arguments. I see no hope of a solution to this; it's just the way things work. 2.3. Defaults for labeled parameters There appears to be a straightforward and unambiguous mechanism, patterned after the existing type-class system, for providing default values for named parameters which are used automatically when no explicit value is provided. Unfortunately, the defaulting mechanism does not seem to extend to implicit parameters. Again, I will expand on this section is there's interest in adding explicit labeled parameters to Haskell. 2.4. Namespace issues By their nature, labels have global extent; however, this still leaves a choice of how their names should be scoped -- in particular, whether label names should be considered a part of the module namespace, or should belong to a global flat namespace. The disadvantages of module scoping are more typing (of the keyboard variety), the annoyance of conflicts when importing unqualified names, and perhaps additional complexity in the implementation; the advantage is the prevention of inadvertent label "capture" across modules. This becomes an issue if we implement the most straightforward defaulting mechanism for named parameters. It is also worrisome in the presence of implicit parameters, where identical labels are merged by the system and so it's very important to know what the system considers to be identical. I think it is wise to place label names in module scope for this reason alone, despite the occasional nuisance this may cause. 2.5. Record syntax There is a close analogy between labeled parameters and the labeled-field syntax of Haskell 98. Given the declaration data C = F { f1,f2 :: Int, f3 :: Bool } it is natural to give the constructor F the type F :: (f1 :: Int, f2 :: Int, f3 :: Bool) => C Unfortunately this change is not backward compatible, because Haskell 98 requires F to have the type Int -> Int -> Bool -> C. Furthermore, extending this analogy to the field-update syntax appears to be tricky (though not, I think, impossible -- the existing behavior can probably be duplicated through an argument defaulting mechanism). I hope that these issues will be considered for Haskell 2; the fact that the field syntax already exists in Haskell is a good reason to consider adding explicit labeled parameters. 2.6. The f {?x = ...} question How should the compiler treat the expression f {?x = ...} when f's type does not include an implicit parameter by that name? Two behaviors seem reasonable: it could reject the expression, or it could accept it and treat it as equivalent to f. The argument for accepting the expression is: + If this application node is to be valid, the left hand side must have a labeled parameter @x. But adding an ignored implicit parameter to f is a legitimate specialization; indeed, we must allow the type checker to create specializations of this sort, for otherwise it could not infer a type for perfectly reasonable functions such as fromJust' Nothing = ?default fromJust' (Just x) = x So the natural behavior of the type checker is to specialize f to satisfy the constraint imposed by the application node. When the application is performed the argument will be ignored, and the net result is as if we'd just typed "f". The argument for rejecting it is: - Expressions of the kind under consideration are never useful, since they are always exactly equivalent to their LHS alone. On the other hand, they will appear as the result of a common error: mistakenly believing that an expression has an implicit parameter which in fact it doesn't. The big advantage of static typing is early detection of bugs; here we have an expression type which is never useful in a correct program and commonly occurs as a bug. We should reject it. I find the latter argument to be more compelling than the former. Therefore I propose that we reject these expressions. 2.7. Parallel bindings in labeled-application notation Consider the following two attempts at a fibonacci-number-producing function: fib1 :: Integer -> Integer -> [Integer] fib1 a b = a : fib1 b (a+b) fib2 :: (?a :: Integer, ?b :: Integer) => [Integer] fib2 = ?a : fib2 {?a = ?b} {?b = ?a + ?b} fib1 works, but fib2 doesn't: if passed 1 and 1 as arguments it will produce [1,2,4,8,...]. What went wrong here is that the recursive call to fib2 contains two nested application nodes; the implicit @b parameter on the RHS of the inner one is lifted out, and becomes a target of the outer application. The effect is that the rebindings of ?a and ?b happen sequentially, from right to left, instead of in parallel. We can "solve" this by treating the f {..., ...} notation as a single parallel application node, instead of a shorthand for f {...} {...}. Then fib2 will work if we write it as fib2 = ?a : fib2 {?a = ?b, ?b = ?a + ?b} This semantics is trivial to implement, since it's already how the let/with binding form works, and it's compatible with everything else, because except where implicit parameters are involved it doesn't matter whether the applications happen sequentially or in parallel. However, I'm not really happy with it; intuitively I feel that {...} {...} should behave the same as {..., ...}. The let form is actually clearer here. This is frustrating because otherwise there seems to be a clear-cut case for preferring the labeled application syntax over the let syntax. 2.8. The meaning of let Excluding recursive definitions and considering denotational semantics only, there seem to be two ways of interpreting a statement like let x = [E] in [F] -- it could be the same as [F] with [E] directly substituted in place of x, or it could be the same as (\x -> [F]) [E]. In the absence of implicit parameters these two interpretations seem to be semantically equivalent. (Except that one may type-check while the other does not -- but here, as elsewhere in this document, I don't consider that to be a semantic difference.) But they are not equivalent when [E] has an implicit parameter. (\x -> [F]) [E] is an application node, so [E]'s implicit parameter is lifted out, and the path down to the usage point goes directly to [E] without involving [F] at all. But if we substitute for x inside of [F], the path to [E] goes through [F], and the implicit parameter may be rebound along that path. I think this ambiguity is at the root of a lot of the confusing behavior of implicit parameters. LSML doesn't seem to note this distinction explicitly, although the authors do say that let ?x = u in (let y = v in t) is equivalent to let y = v in (let ?x = u in t) and not to let y = (let ?x = u in v) in (let ?x = u in t), adding that under the latter equivalence, "implicit parameters would simply be static variables" (LSML section 3.1). Actually this appears to be exactly the substitution versus abs/app distinction. Implicit parameters could work either way, I think. In general, expressions will have different types, not just different behaviors, under the two interpretations. For example, let x = ?z in (let ?z = "" in (x ++ ?z)) has principal type String if the outer let is interpreted as a substitution, and (?z :: String) => String if it's interpreted as an abs/app. I don't think that the principal types ever differ in the case of type-class constraints. The type-inference rules of LSML are based on substitution semantics, but the implementation in Hugs and GHC uses abs/app semantics in a single case: when a pattern binding is reduced to a monotype because of the monomorphism restriction. This behavior appears to be accidental (due to the way the implementation shares code with the type-class mechanism). I think it's very important that it be changed. More about this in section 2.12. This typing issue seems to force us to choose between substitution and abs/app semantics for let statements. I propose that we choose substitution semantics and use it consistently. 2.9. Implicitly parameterized parameters Ordinarily when a function with implicit parameters is used on the RHS of an application node, the implicit parameters are lifted out as described above. But what if we really want to pass the whole function as an argument, implicit parameters and all? The function on the LHS would need to have a type with a "rank-2 implicit argument": ((?arg :: t) => val) -> ... There's no way for types like this to be inferred automatically, but they could be provided via explicit type signatures. Unfortunately, it turns out that by introducing types like this, we make a program's behavior dependent on its typing. For example: f1 :: (Num a, Num b) => a -> ((?x :: b) => b) -> (a,b) f1 a b = (a,b) {@x = 2} f2 :: (Num a, Num b) => ((?x :: a) => a) -> b -> (a,b) f2 a b = (a,b) {@x = 2} f1 ?x ?x {@x = 1} ==> (1,2) f2 ?x ?x {@x = 1} ==> (2,1) I would prefer to avoid this problem by banning these types. However, there are two good arguments for allowing them: + They're useful. + They're already implemented, and used in at least one large project (HScheme). I think that these arguments trump the opposition. It's sad to lose the type-independence of the semantics, but the silver lining is that the compiler will never infer these types, so one can avoid this particular can of worms in one's project by never writing such types explicitly. 2.10. Linear implicit parameters Linear implicit parameters (as described in the GHC manual) fit neatly into the framework of auto-lifting parameters -- they are like ordinary auto-lifting parameters except that a call to "split" is inserted whenever the value is propagated down to both sides of the application node. The GHC manual mentions two problems which are specific to linear implicit parameters. I propose a solution to one of them (let substitution is invalid) in section 2.12. I don't know if the other one (behavior of a certain function depends on presence or absence of a type signature) can be solved; however, from the point of view of this framework, the behavior with the type signature is clearly correct, and the behavior without incorrect. Therefore I propose that the latter behavior be changed to agree with the former, *if that's possible*. It seems as though the following would work (here and elsewhere): first infer the function's type by the existing algorithm, and then perform auto-lifting in a subsequent pass with that type as the basis. 2.11. Discarding ?x notation The new implicit parameter framework exposes some wartiness in the ?x notation; @x seems to have a simpler semantics. A possible solution to some of the peculiar behavior of implicit parameters is to eliminate the ?x notation and use @x instead. This effectively makes implicit parameters more explicit by separating binding and use. This is not as dumb an idea as it sounds, because the most useful property of implicit parameters is that they auto-propagate through functions that don't mention them at all -- and that behavior would remain unchanged. Just writing "\{@x=t}->t" instead of ?x everywhere isn't going to solve anything; some additional discipline would need to be imposed. One possibility which looks promising is to require that @x parameters appear only in function bindings. I haven't explored very far in this direction. 2.12. The monomorphism restriction The stated purpose of the monomorphism restriction is to "prevent unexpected loss of sharing". This goal has to be weighed against two constraints: the mechanism to preserve sharing should not alter program semantics, and it should cause program rejection as rarely as possible. The present monomorphism restriction for type-class constraints meets these criteria pretty well. It always preserves sharing, it always preserves program semantics, and it doesn't usually reject programs unless it's really impossible to make the other two properties hold. The present monomorphism restriction for implicit parameters does not preserve program semantics. For example, the expression "let ?x = 1 in let y = ?x in let ?x = 2 in y" has the value 2 with the monomorphism restriction turned off, and the value 1 with it turned on. I feel very strongly that this should change -- the monomorphism restriction should never alter semantics, and all else should be secondary to this. I have several reasons for this belief, but the primary one is the following: + If the monomorphism restriction ever alters semantics, then it is not a restriction at all, but an interpretation. I don't think anyone wants a monomorphism interpretation -- it's intrusive enough as a restriction. What is a sensible replacement for the current rule? It's not hard to see that the only way to preserve sharing is to reduce the binding to a monotype at the binding point, and the only way to preserve semantics while doing this is to set the implicit parameter to the *correct* value -- that is, the value it would have had anyway. In general, this isn't possible. For example, in let f = ... in (f {?x = 1} + f {?x = 2}) we can't possible apply the correct value because there's more than one of them. In other cases, it's tricky to find the value -- as in let f = ... in (f {?x = [some complex expression]}) where the complex expression is not in scope at f's binding point and would have to be "pulled out" somehow. In an effort to avoid these kinds of problems, I propose the following compromise rule. I assume a bound identifier "f" with an implicit parameter "?x". 1. If ?x is never mentioned anywhere in the body of the let or in f's recursive binding group, *AND* f is nowhere passed as an implicitly-parameterized argument (see section 2.9), then f is reduced to a monotype in the same way it's done presently. (Under this restriction, this always preserves semantics.) 2. If every use of f is on the left-hand side of an application node, *OR* there's just one use of f total, then f is generalized (i.e. the monomorphism restriction is not applied). The motivation for the first condition is that by using f in a function application, the programmer is indicating explicitly that f is a function, just as would be indicated by supplying an explicit type signature. 3. Otherwise, the program is rejected. I think this rule would be reached only rarely. I think that this rule is easy to implement, and works well; it preserves semantics and sharing, and allows the programmer a useful additional "escape hatch" in a common case. What about linear implicit parameters? I claim that linear implicit parameters should not be subject to the monomorphism restriction at all. Reason: the purpose of the monomorphism restriction is to prevent unexpected loss of sharing, but with linear implicit parameters loss of sharing is the whole point! The programmer wouldn't be using them unless he wanted each use to be distinct. Since we are treating let statements as having substitution semantics, each substituted LIP should be different. The easiest way to ensure this is to generalize all let bindings which use them. 2.13. Let syntax version labeled-application syntax I think that there's a strong case for abandoning the let-binding syntax for implicit parameters in favor of labeled-application syntax. Among the reasons: + The identifiers foo and ?foo have very different characteristics: the former is a newly-introduced name for a locally-scoped binding, while the latter refers to a global label which lives in a separate namespace, and probably follows module scoping rules. Their coexistence in the let syntax is uneasy. + There is a close analogy between implicit-parameter labels and Haskell 98 field labels, suggesting that the same syntax be used for both. It also extends naturally to explicit labeled parameters, if we add those. + Let-bindings of implicit parameters are non-recursive. This is a wart when the let syntax is used, but is the natural state of affairs in labeled-application notation. + The behavior of expressions like "let ?x = 3 in ?x + ?x", which happens to yield the same result as "let x = 3 in x + x" despite its very different underlying semantics, is a conceptual trap which encourages the writing of plausible but incorrect code. + The expression "let ?x = 1 in let z = ?x in let ?x = 2 in z" is difficult to understand precisely because the usual semantics of let statements conflicts with the semantics of implicit variables. The equivalent expression using the labeled-apply notation is "(let z = ?x in z {?x = 2}) {?x = 1}". This seems to be much easier to understand. + In the expression "(let ... in ...) {?x = ...}", the binding of ?x does not scope over the binding portion of the let statement -- just as in an ordinary function application, but unlike the behavior of ordinary let in the expression "let x = ... in (let ... in ...)", where the binding of x does scope over the binding portion of the nested let. + The let syntax suggests that it should be legal to bind implicit parameters which are never used; the application syntax suggests it should be illegal. I think it should be illegal (see section 2.6). + "let ?x" bindings are monomorphic, like function arguments but unlike "let x" bindings. + Labeled-apply syntax encourages binding implicit parameters close to the call point, which is less bug-prone because you know exactly where your value is going. Let syntax encourages binding at a higher level. The reasons for favoring let syntax are: - "let ?b = ?a + ?b in (let ?a = ?b in fib)" behaves as it looks like it should behave, while the equivalent "fib {?a = ?b} {?b = ?a + ?b}" doesn't. - The difference between "let ?a = ... in (let ?b = ... in ...)" and "let { ?a = ... ; ?b = ... } in ..." is clearer than the corresponding difference in the labeled-application syntax. It's frustrating that there isn't an unambiguous winner here, but I do think that labeled-application syntax has the advantage. 2.14. Implicit parameters in recursive binding groups See the section on linear implicit parameters (2.10). I may expand on this later. 3. Summary of suggested changes 3.1. Changes which are easy to implement and seem to be clear wins * Reject expressions of the form "let ?x = [E] in [F]" when [F] does not depend on ?x (that is, when [F]'s principal type does not include an implicit parameter ?x). See section 2.6. * Never implicitly reduce implicit-parameter contexts by "pulling values from the environment", except as prescribed by the monomorphism restriction rule. For example, the following should be illegal: let ?x = 1 in let z :: Integer z = ?x in ... See section 2.8. * Remove the monomorphism restriction for linear implicit parameters, and change the current MR rule for ordinary implicit parameters to something which preserves semantics. See section 2.12. * Introduce the {?x = ...} syntax for implicit-parameter application. (Should this be in section 3.3?) 3.2. Changes which may be harder to implement, but seem to be clear wins * Implement my proposed MR rule. See section 2.12. * Place implicit parameters in the module namespace. See section 2.4. * Make recursive functions with linear implicit parameters behave as though explicitly typed. See section 2.10. 3.3. Other changes which we should consider * Implement explicit named parameters, possibly with a defaulting system. * Deprecate the let ?x syntax. See section 2.13. -- Ben