Implicit parameters, second draft

[Ben Rudiak-Gould]

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