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)
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
% ---------- Now why would we not allow something like this: (case over a string for simplicity, although it is not supported)
fun: Int => Int => Int -> Int; fun x y z = x + y + z;
default = new-attribute (String -> Int); attribute fun default (lambda var-name -> case var-name | "x" -> 1 | "y" -> 0);
three = fun 2;% <=> (fun 1 0 2);
if a `default` is not provided for the function the compiler will fall back to the previous example.
Afficher les réponses par date
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
inc x y = x + y; five = inc (x := 3) 2;)
In fact in our case. for this to work the type annotation needs to be
inc: (x : Int) => Int -> Int;
Currently, yes. But we should also make it work if the type is
(x : Int) -> Int -> Int;
And, it should (once implemented) also work if there is no type annotation at all, because the inferred type would be
(x : Int) -> (y : Int) -> Int
Is this want we want ? The information seems quite redundant.
Not sure which redundancy you're referring to.
BTW, as you may have seen, I fixed conv_p (to some extent, at least), so now we actually do *check* the types, which caught various type errors in our code. I fixed some of them, but could you take a look at the remaining ones?
Stefan
Yes, I noticed. I think I solved most of the issues in my next commit.
I have an issue with attributes. It seems the context is not allowed to change when adding attributes. (Test "Implicit Arguments"). Nevertheless, the test about attributes is working. I am still investigating on the issue.
Yes, I noticed. I think I solved most of the issues in my next commit. I have an issue with attributes. It seems the context is not allowed to change when adding attributes. (Test "Implicit Arguments").
Don't know what you mean by "context is not allowed to change". Maybe it's related to my comment:
(* FIXME: We need to have something in lexp to represent this * add-attribute operation! *)
Nevertheless, the test about attributes is working. I am still investigating on the issue.
One thing that occurred to me is that maybe this attribute business is not needed. More specifically, instead of
greater-than = new-attribute (Int -> Bool); [...] attribute w greater-than (lambda (y : Int) -> True);"
being special declarations, we should just macro-expand them to
attribute_greater-than_table : lexp-table (Int -> Bool); attribute_greater-than_table = lexp-table-empty; [...] attribute_greater-than_table = lexp-table-add attribute_greater-than_table w (lambda (y : Int) -> True)
For that we need to implement the `lexp-table` data type, which would be an associative table indexed by lexps. And the main difference would be that the lookup would be done based on the *value* of `w` rather than based on the identity of the variable itself (and similarly, the `greater-than` would be treated as a *string* rather than referring to a particular variable).
Another thing I've been thinking about has to do with naming conventions:
- we need a special name-space for builtin thingies. E.g. when we print a "Sort (...)" usually it can be printed as "Type" or "Type1" but these vars may be hidden. We currently print them as "<Type>" or some such, but it's not an "official" syntax. I think we need an official syntax (one that works when reading a program) that stands for "builtin". It could be "##..." or "<...>" (i.e. a special naming convention) or "(## ...)" or the "(built-in ...)" we currently use. The important thing is that it should also be usable to represent the Sort(...) and SortLevel(...) lexps. And it should be sufficiently concise to be tolerable in printed output. I'm leaning towards "##" so we'd write "##Type ##0", "##Type (##S ##0)", "##+", "##TypeLevel", ... OTOH, since I plan on using "." for module-field names, we could use a ".." prefix and write things like "..Type ..0".
- For explicitly written metavariables (i.e. wholes that will be filled via type-inference), I was thinking of using the "?" prefix. So you could write:
foo : ?; bar : ?; foo = ...; bar = ...;
to declare that foo and bar are mutually-exclusive without specifying their type. And those metavars would be automatically generalized (as usual in Hindley-Milner type inference), so you could write:
identity : ?a -> ?a;
instead of
identity : (a : Type) ≡> a -> a; or identity : (a : ?) ≡> a -> a;
But admittedly, for such type declarations we could also accept
identity : a -> a;
if "a" is not in the context (yet).
Stefan
- we need a special name-space for builtin thingies. E.g. when we print a "Sort (...)" usually it can be printed as "Type" or "Type1" but these vars may be hidden. We currently print them as "<Type>" or some such, but it's not an "official" syntax. I think we need an official syntax (one that works when reading a program) that stands for "builtin". It could be "##..." or "<...>" (i.e. a special naming convention) or "(## ...)" or the "(built-in ...)" we currently use. The important thing is that it should also be usable to represent the Sort(...) and SortLevel(...) lexps. And it should be sufficiently concise to be tolerable in printed output. I'm leaning towards "##" so we'd write "##Type ##0", "##Type (##S ##0)", "##+", "##TypeLevel", ... OTOH, since I plan on using "." for module-field names, we could use a ".." prefix and write things like "..Type ..0".
Plus j'y pense plus ça me plait: "inductive-cons" devient "##cons", "inductive_" devient "##inductive" ou "##datatype". Et ce ne sont pas des variables, donc ça ne peut pas être redéfini.
Stefan
Here are my thoughts on our attribute business.
*Currently:* How attributes are working is: they are virtually macros that disappear once elaboration is done. attributes are saved inside the elaboration environment in an associative table that associate a variable and an attribute to a lexp (attribute's value).
As I understand it, the current issue is when an attribute is added:
attribute Int default default-int;
It modifies the environment without creating new declarations. Which is not allowed because it would endanger type checking soundness.
(Side note, if a dummy declaration is returned by `attribute`, the assert is still triggered. if the assert is removed, a DB index problem arise when attributes are used. The triggered assert is not in the Pmcall (where `attribute` is processed) but in the Pexpr branch).
*The proposed solution:*
make `attribute w greater-than (lambda (y : Int) -> True);`expand to
attribute_greater-than_table : lexp-table (Int -> Bool); attribute_greater-than_table = lexp-table-empty; attribute_greater-than_table = lexp-table-add attribute_greater-than_table w (lambda (y : Int) ->
True)
We have a lexp-table for each kind of attribute we want to create (Attribute: Int -> Bool, Attribute: Int, etc...). `attribute_greater-than_table` is a regular variable which will only be used under the hood.
`get-attribute w attr` => lexp-table-lookup w attribute_attr_table
Everything has to be done during the elaboration phase because we need to be able to inspect the lexp-table to retrieve the default attribute when processing implicit arguments.
I don't think lexp-table is needed at runtime since all the lookup should have been done already.
(Side note, if a dummy declaration is returned by `attribute`, the assert is still triggered.
Yes, it would really need to return a new kind of declaration, so we'd need to change the definition of `Let` in `lexp` for that.
Everything has to be done during the elaboration phase because we need to be able to inspect the lexp-table to retrieve the default attribute when processing implicit arguments.
That's right.
I don't think lexp-table is needed at runtime since all the lookup should have been done already.
Agreed. But we'll leave that to some hypothetical future optimizer.
Stefan