Introducing Operator types #84
Conversation
Still need to work on resolve_overloading.
The arithmetic rules still need work
It was found earlier that the HeatXfer test was actually poorly typed and thus was removed from the tests. It only happened to work because of the order in which the rules were applied.
This needs tests added
I've changing our type checking behavior to return all errors. If there is any error, an exception will be thrown.
GeorgeR227
force-pushed
the
gr/impv_infer
branch
from
ce10d11 to
5fc4c85
Compare
This function now returns the type difference as Inf if the rule doesn't match the operator. Also added doc strings.
src/acset.jl
Outdated
| score_src = (rule.src_type == d[d[op1_id, :src], :type]) | ||
| score_tgt = (rule.tgt_type == d[d[op1_id, :tgt], :type]) | ||
| """ | ||
| check_operator(d::SummationDecapode, op_id, rule, edge_val; check_name::Bool = false, check_aliases::Bool = false, ignore_infers::Bool = false, ignore_usertypes::Bool = false) |
test/language.jl
Outdated
| infer_types!(op_not_in_rules) | ||
|
|
||
| @test op_not_in_rules == op_not_in_rules_res | ||
| @test op_not_in_rules !== op_not_in_rules_res |
There was a problem hiding this comment.
how can both of these tests pass?
There was a problem hiding this comment.
Line 858 is checking that the ACSets have the same entries, Line 859 is checking that the memory locations are not the same.
| name = [:h, :Γ, :n, :ḣ, :sum_1, Symbol("•2"), Symbol("•3"), Symbol("•4"), Symbol("•5"), Symbol("•6"), Symbol("•7"), Symbol("•8"), Symbol("•9"), Symbol("•10"), Symbol("1"), Symbol("•11"), Symbol("2"), Symbol("•_6_1"), Symbol("•_6_2")] | ||
| end | ||
| end | ||
|
|
There was a problem hiding this comment.
Do we not need to test this anymore?
There was a problem hiding this comment.
It was figured out that this Decapode was actually poorly typed and thus not a good test for ensuring the overloading/inferring was working correctly. Instead I've converted this into a type-checking test. It's been shifted around I but not deleted.
| struct Operator{T} | ||
| res_type::T | ||
| src_types::AbstractVector{T} | ||
| op_name::Symbol | ||
| aliases::AbstractVector{Symbol} | ||
|
|
||
| function Operator{T}(res_type::T, src_types::AbstractVector{T}, op_name, aliases = Symbol[]) where T | ||
| new(res_type, src_types, op_name, aliases) | ||
| end | ||
|
|
||
| function Operator{T}(res_type::T, src_type::T, op_name, aliases = Symbol[]) where T | ||
| new(res_type, T[src_type], op_name, aliases) | ||
| end | ||
|
|
||
| function Operator(res_type::Symbol, src_type::Union{Symbol, AbstractVector{Symbol}}, op_name, aliases = Symbol[]) | ||
| Operator{Symbol}(res_type, src_type, op_name, aliases) | ||
| end | ||
| end | ||
|
|
||
| function same_type_rules_op(op_name::Symbol, types::AbstractVector{Symbol}, arity::Int, g_aliases::AbstractVector{Symbol} = Symbol[], sp_aliases::AbstractVector = Symbol[]) | ||
| @assert isempty(sp_aliases) || length(types) == length(sp_aliases) | ||
| map(1:length(types)) do i | ||
| aliases = isempty(sp_aliases) ? g_aliases : vcat(g_aliases, sp_aliases[i]) | ||
| Operator{Symbol}(types[i], repeat([types[i]], arity), op_name, aliases) | ||
| end | ||
| end | ||
|
|
||
| function arithmetic_operators(op_name::Symbol, broadcasted::Bool, arity::Int = 2) | ||
| @match (broadcasted, arity) begin | ||
| (true, 2) => bin_broad_arith_ops(op_name) | ||
| _ => error("This type of arithmetic operator is not yet supported or may not be valid.") | ||
| end | ||
| end | ||
|
|
||
| function bin_broad_arith_ops(op_name) | ||
| all_ops = map(t -> Operator{Symbol}(t, [t, t], op_name), FORM_TYPES) | ||
| for type in vcat(USER_TYPES, NUMBER_TYPES) | ||
| append!(all_ops, map(t -> Operator{Symbol}(t, [t, type], op_name), FORM_TYPES)) | ||
| append!(all_ops, map(t -> Operator{Symbol}(t, [type, t], op_name), FORM_TYPES)) | ||
| end | ||
|
|
||
| all_ops | ||
| end |
There was a problem hiding this comment.
This looks like it is trying to emulate the style of having an abstract type for an "Operator", can this idiom be used explicitly.
|
@quffaro This PR checks types via a notion of a “score” which counts the number of mis-matched types between a function’s type signature vs. a collection of type signatures (“rules”). It seems to be converging on some variation of the “pattern matching” idiom. (If a pattern is fully matched, or no partial match is found (i.e. fall through), throw an error. Else when a partial match is found, throw an error.) And so I am concerned that we may be unwittingly getting into maintaining a bespoke type checker by way of reimplementing of a pattern matching system. I think that the explicit notion of “scoring” is a step in the right direction, but ultimately should be realized by making use of a fully-featured pattern matching capabilities offered by MLStyle or a similar package like Moshi. Can I get your thoughts on this? @quffaro |
Meant to check if the ruleset contains a situation where multiple rules may be applied in the same situation.
This PR is driven in part by two different desires. There is a past one, in issue #53, to generalize the inference/overloading rules since there was a lot of repetition. Then there is also the current one, in issue #81, to remove the users from adding in DEC operator annotations.
My idea is to begin the process of having DEC operators as simply being Symbols in the ACSet to being an Operator node which is richer in that it has typing and naming information attached to it. So for example we'll no longer have
:dfloating around but:dthat acts on:Form0and returns:Form1and has other aliases:d_0, etc.... This PR won't change the actual ACSet to use this since this will be massively breaking but it will be used heavily for our compilation code.This data organization moves our ACSet code closer to that of a theory, where operators are not just names but are expected to act on and return certain types. This structure also allows us to present generic names to the user while having functions that can take in the struct information and output a unique name for the operator.
There is some future-proofing included which expects the similar shift from Symbol types, like
:Form0, to our new Symbolic types. A goal I'd want to tackle but will leave out of scope for when our Symbolics code matures more is to merge these Operators with their Symbolic function representations.