Design for implicit parameters

[timsueberkrueb]

Declaration site

foo(x: Q, y: R, implicit z: S, implicit w: T)

Usage site

foo(x, y)

foo(x, y, z := z)

foo(x := 1, y, z:=z)

Pros

• A argument list with both explicit and implicit parameters rather than multiple lists which don't fit the general language design
• Intuitive, doesn't need a lot of explanation for new users

Cons

• The implicit keyword is rather long

[timsueberkrueb]

Pseudo-EBNF:

Declaration site

<Telescope> ::= '(' ( <Param> ',' )* ')' | ε
<Param> ::= <ExplicitParam> | <ImplicitParam>
<ExplicitParam> ::= <Var>+ : <Exp>
<ImplicitParam> ::= 'implicit' <Var>+ : <Exp>

Usage site:

<Args> ::= '(' ( <Arg> ',' )* ')' | ε
<Arg> ::= <NamedArg> | <UnnamedArg>
<NamedArg> ::= <Var> `:=` <Exp>
<UnnamedArg> ::= <Exp>

Lowering semantics:

• For any explicit parameter at the declaration site, there must be either an unnamed argument or a named argument at the usage site.
• For any implicit parameter at the declaration site, there may be a named argument at the usage site
• All arguments must be specified in the declared order

[eternaleye]

So, implicits are something I have a lot of thoughts about; both in terms of their worst pitfalls and how to remedy them. IMO, the worst pitfall of any implicits implementation is when the search implementation can potentially "make the wrong choice" - e.g. if you have an implicit of Monoid Nat and it chooses multiplication rather than addition.

As far as I'm aware, the only reliable way to avoid this is to enforce that the search system must have at most one valid candidate it could find. However, there are many ways of achieving this - and fortunately, there's plenty of room for them to coexist:

• The type of the implicit is subsingleton, itself; this is the "strongest" option
• The type of the implicit is localized in some way, e.g. to its own defining module and the module of a chosen parameter. This allows an overlap check to be guaranteed to catch any overlapping instances. This is Rust's "orphan rule".
• The means of adding an implicit to the search set is in some way uniqueness-enforcing. With effect handlers, this is generally a system of scope-based shadowing, either lexical or dynamic.

Crucially, as long as no two methods that submit an implicit to be searched can submit an overlapping instance that will be found by the same search method (e.g. effect handlers may use a different search method than _), all of these can coexist cleanly.

EDIT: Note that simply erroring out if search is ambiguous is not sufficient; it leaves the codebase fragile to ecosystem changes and refactors. Ensuring that it cannot be ambiguous, "statically", is key.

[BinderDavid]

The name "implicit arguments" might be a bit misleading; we currently do not intend this to involve any kind of instance search. Instead, implicit arguments are replaced by meta-variables during the lowering phase which are then solved by the unification algorithm. We plan for the unification algorithm to support Miller's pattern fragment of higher-order unification which guarantees that it finds the most general unifier, i.e. a unique solution. I think this corresponds to your "subsingleton" option above.

I am definitely thinking about a more powerful instance search mechanism for the future, maybe something like the mechanism described in the cochis paper. But the scope of this proposal is more restricted. We mainly try to replace Cons(Bool, True, Nil(Bool))) by Cons(True, Nil) and f.ap(Nat,Bool,2) by f.ap(2) etc. :wink: