I want to make sure I got his right before implementing it. It is my understanding that we would like to support something like:
inc: Int => Int -> Int; inc x y = x + y;
five = inc (y := 2) (x := 3); % <=> (inc 3 2)
Pretty much, except that "inc 3 2" is an error (`inc` can only take a single non-implicit argument). It should be `inc (x := 3) 2` or `inc (_ := 3) 2`.
Now , as you see `x` is an implicit argument. The user can provide a value that will populate that argument with a default value if not provided.
default = new-attribute (Int); attribute Int default 1;
four = inc 3; % <=> inc 1 3 inc2 = inc (x := 2); % partial application five = inc2 3; % <=> inc 2 3
IIUC by "can provide" you mean "in the future". Then, yes, pretty much, except that new attribute can't have type Int since we ant to be able to use it for other arg types than Int. Instead it'll be a macro, so something like:
default = new-attribute (LexpContext -> LexpType -> Sexp); attribute Int default (lambda lxpctx goal -> integer_ 1);
Now why would we not allow something like this: (case over a string for simplicity, although it is not supported)
[...]
fun x y z = x + y + z;
[...]
attribute fun default (lambda var-name ->
We could, indeed. We could get "similar" results with
type Option t | None | Some t attribute Option default (lambda lxpctx goal -> symbol_ "None")
fun: Option Int => Option Int => Int -> Int; fun (_ := x) (_ := y) z = let x = case x | None => 1 | Some x => x; y = case y | None => 1 | Some y => y in x + y + z;
Or even
type Opt t (v : t) | Val t unVal v = case v | Val v => v
attribute Opt default (lambda lxpctx goal -> ...return second arg `goal`...)
fun: Opt Int 1 => Opt Int 0 => Int -> Int; fun (_ := x) (_ := y) z = unVal x + unVal y + z;
The main downside is that you have to write
fun (x := Val 5) 7
[ Note that it wouldn't be hard to make it so Typer optimizes "Val" and "unVal" away, so there is no associated runtime cost. ]
Maybe the "default" macro could *also* be invoked for explicit-implicit arguments (i.e. the explicit-implicit arg wouldn't directly provide the arg, but would instead provide a "hint" to the default macro):
default = new-attribute (LexpContext -> LexpType -> Option Sexp -> Sexp); attribute Opt default (lambda lxpctx goal arg -> case arg | Some s -> node_ (symbol_ "Val") s | None -> ...return second arg `goal`...)
But, to tell you the truth I'm not sure how far I want to go down that road, and I'd like to minimize the hardcoded functionality in the core language. The ability to programatically compute the default value of "missing" implicit arguments is important, of course, so we do want that ability.
Oh, while I'm here: the type of macros should look like
(List Sexp -> ME Sexp)
where "ME" is the "macro expansion monad". Then we can provide primitives like `getGoal : ME Lexp` to get the target type of the expression we're building or `lookupSym : String -> ME (Option Lexp)` to lookup the type of a variable.
Of course, there's also the thorny issue of mixing Lexp and Sexp: a macro should also be able to return a Lexp, and should be able to convert a Sexp into a Lexp (i.e. to call lparse). Ideally, we'd also have some way to convert a Lexp to a Sexp (in a reversible way), but it's probably going to be difficult to do that...
Stefan