Ad hoc polymorphism #703
Merged
Ad hoc polymorphism #703
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
We make the lazy constraint mechanism more powerful by having the solver attempt to expand a lazy constraint every time it learns something new about the type of its trigger expression, not just when the type becomes fully concretized. For example, a constraint that checks that a variable is of a container type can be expanded as soon as the top-level definition has been resolved (i.e., we know whether it is a set or a vector) even if the element type of the container is not yet known. This change is in preparation for the ad hoc polymorphism feature that will require expanding the first argument of a function call just enough to disambiguate amoing all functions with the same name.
mihaibudiu
approved these changes
Jul 15, 2020
doc/tutorial/tutorial.md
Outdated
| extern function log(module: module_t, level: log_level_t, msg: string): () | ||
| ``` | ||
|
|
||
| The compiler automatically infers these annotations for non-extern functions, so |
There was a problem hiding this comment.
This seems inconsistent, before you said that non-extern functions cannot have side-effects. So what annotations are inferred?
There was a problem hiding this comment.
non-extern functions can invoke extern functions with side effects. I will clarify.
| | otherwise = | ||
| (rname $ name f) <> "_" <> targ0 <> "_" <> pp (length $ funcArgs f) | ||
| where | ||
| arg0 = funcArgs f !! 0 |
There was a problem hiding this comment.
arg0 is only evaluated if this is a polymorphic function. Polymorphic functions must take at least one argument (enforced in Validate.hs)
| -- recursive functions, as reasoning about them seems tricky otherwise. | ||
| and exprArgs && (maybe False (exprIsInjective d (CtxFunc f) (S.fromList $ map (\a -> ArgVar f $ name a) funcArgs)) $ funcDef) | ||
| where f@Function{..} = getFunc d exprFunc | ||
| exprIsInjective' _ EApply{..} = and exprArgs |
There was a problem hiding this comment.
what happened to recursive functions?
There was a problem hiding this comment.
oops. I actually implemented support for them but forgot to use it here.
There was a problem hiding this comment.
no, we're good, that check just moved above.
| | otherwise = t | ||
| where t = funcType $ getFunc d f ts | ||
|
|
||
| exprNodeType' _ _ e@EApply{} = error $ "exprNodeType' called with unresolved functio name: " ++ show e |
| -- Attributes do not affect the semantics of the program and can therefore | ||
| -- be validated last. | ||
| progValidateAttributes d'' | ||
| return d'' | ||
|
|
||
| {- |
There was a problem hiding this comment.
are you still doing this someplace else?
There was a problem hiding this comment.
no, recursive functions are now allowed
| //var podsByNode = Aggregate((appliedToGroup), group2map((nodeName, podsOnNode))). | ||
|
|
||
| AppliedToGroupSpan(appliedToGroup, nodeName) :- | ||
| AppliedToGroupPod(appliedToGroup, _, nodeName). | ||
| // var span = Aggregate((appliedToGroup), group2set(nodeName)). | ||
| // var span = Aggregate((appliedToGroup), group`/2set(nodeName)). |
This commit implements RFC vmware#670. We already have support for argument polymorphism, e.g.: ``` function vec_length(v: Vec<'X>): usize ``` Here we introduce ad hoc polymorphism, that additionally allows defining functions with the same name for different types, e.g.,: ``` function size(v: Set<'X>): usize {...} function size(v: Map<'X>): usize {...} ``` The compier uses the number of arguments and the type of the _first_ argument to disambiguate the callee: ``` // (1) function size(v: Vec<'X>): usize {...} // OK: different number of arguments function size(v: Vec<'X>, foo: 'Y): usize {...} // OK: different type of the first argument. function size(v: Set<'X>): usize {...} // ERROR: conflicts with (1) function size(v: Vec<bool>): usize {...} ``` This improves DDlog code in a coupe of ways: - We no longer need to prefix function names with type or module names - Once we support object-oriented function call notation, it will be nicer to write `x.length()` vs `x.vec_length()` - We will be able to get rid of the horrible hack with string conversions functions where the function name is computed by addint `2string` to the type name, and just name all of them `to_string()`. Implementation details: - Within a module, we always report conflicts regardless of whether conflicting functions are invoked anywhere in the program. When conflicting declarations appear in different modules, we postpone the check until the user makes a function call that cannot be unambiguously resolved to one of the candidates, i.e., we won't complain even if the user imports both modules unqualified unless they try calling the function. - Rust does not allow functions with the same name unless they appear inside different modules or impl blocks. Both options don't work well for us. Instead the compiler mangles names of polymorphic functions by adding the type of the first argument and the number of arguments to the name. This is invisible to the user, except in extern functions, which must be named-mangled manually. This is ugly and fragile; hence the preferred solution is to make sure that extern function names are unique, and define aliases to them in DDlog. E.g, in std.dl we keep old function names like string_substr and add new functions, e.g., substr(string,...) that invoke them. This commit also adds support for recursive functions.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Implements #674
Details - in commit messages.
Also adds support for recursive functions along the way.
Not in this PR:
I will work on these next.