Unification or pattern matching for matching `UnionAll` types against each other

Internals & Design
,
1

There’s some type-system functionality which I believe exists in Julia, that I’d like to try to access. I don’t know of a better way to explain it than jumping straight to a code example.

connection(x, y) = false
connection(x::Ptr{Ptr{S}}, y::Ptr{T}) where {T, S <: T} = true

connection(Ptr{Ptr{Int64}}(), Ptr{Int64}())
connection(Ptr{Ptr{Int64}}(), Ptr{Integer}())


a_predicate(x) = connection(x(), Ptr{Integer}())

if false
# mock use of desired function
method = only(methodswith(Ptr, connection))   # pick out the method that returns `true`
unification_args = Tuple{T, Ptr{Integer}} where T
# fill in T, so that `method` applies to `unification_args`
result = unify(method, unification_args)
unification_output = result.T
end

unification_output = (Ptr{Ptr{T}} where T <: Integer)

# another way to compute the same result as `a_predicate`
the_same_predicate(x) = x <: unification_output

for T in [Ptr{Ptr{Int}}, Ptr{Int}, Ptr{Ptr{Float64}}]
    @assert a_predicate(T) == the_same_predicate(T)
end

I’m looking for something with the same functionality as what is implied by the code: a function unify that takes 1. a method and 2. a partially-specified type of arguments to a method, and returns a fully-specified type of arguments such that the method would apply, OR failure.

Failure in this case would arise for example in a call like
unify(method, Tuple{Vector{T}, Ptr{Integer}} where T), since there’s no assignment to T that makes method applicable.

And then really, I would like to not necessarily use method directly, but use method.sig (minus the first element, which is just the function type itself), e.g.:

match(
    Tuple{Ptr{Ptr{S}},Ptr{T}} where S<:T where T, # ...against this
    Tuple{U, Ptr{Integer}} where U  # match this....
).result == (:U = Ptr{Ptr{A}} where A <:Integer)

# or

match(
    Tuple{Ptr{Ptr{S}},Ptr{T}} where S<:T where T, # ...against this
    Tuple{Ptr{U{Int}}, Ptr{Integer}} where U # match this....
).result == (:U = Ptr) # not sure if this is right

This is an area with terminology I’m not very comfortable with, but I’m trying to use terms that appear to be consistent with e.g. Differences between pattern matching and unification? - Stack Overflow and Unification (computer science) - Wikipedia

2

Ptr{U{Int}} where U

This is not a well-formed specification. It appear to be trying to state the constraint of all types where the first parameter is Int. However, that would be exactly equivalent to all types, since (UnionAll(T, Any) where T){Int} === Any) for any value substitution of Any (that expression usually gets normalized and then disallowed if you try to eval it, but symbolically it’s valid)

Type-unification in Julia is normally computed with typeintersect(T, S). As I think you noticed, this function also knows how to compute the bounds on the type variables (since they may be made available as a local variable in the method body inside the call), although the internal function for computing them (jl_type_intersection_with_env) is not currently exported for general consumption.

3 Likes
3

Thanks for the reply! You mentioned jl_type_intersection_with_env, which I see is used in Julia via ccall.

I gave this a shot

intersection_env(@nospecialize(x), @nospecialize(y)) = ccall(:jl_type_intersection_with_env, Any, (Any,Any), x, y)
(intersection, env) = intersection_env(Ptr{T}  where T, Ptr{Int64})

gives: (Ptr{Int64}, svec()). I expected env to contain something about the bound on T.

4

Wel, of course there would not be any information about T, because Ptr == (Ptr{T} where T).

but I am still left expecting, after giving the following a shot:

intersection_env(@nospecialize(x), @nospecialize(y)) = ccall(:jl_type_intersection_with_env, Any, (Any,Any), x, y)

somefunc(x::Ptr{T}) where T = false
m = collect(methods(somefunc))[1]

Ptr_T = (Base.unwrap_unionall(m.sig).parameters)[2]

(intersection, env) = intersection_env(Ptr_T, Ptr{Int64})
5

The env is computed for the argument on the right

6

Ah, okay, thanks. But then I must not be understanding Ptr_T correctly, because this doesn’t work:

julia> (intersection, env) = intersection_env(Ptr{Int64}, Ptr_T)
svec(Ptr{Int64}, svec())
7

Ptr_T is a malformed Type (as objects typically are when you access their fields), so the results are undefined. Pass a valid Type there (like Ptr).

8

I think that I already tried that above. If you know the answer, can you tell me how I can get e.g. (:type_arg_1=Int64) out of (Ptr, Ptr{Int64})? You mentioned, “[type variables] may be made available as a local variable in a method body inside”. I would like to get those bounds, given some types and a method signature.

9 
julia> intersection_env(Ptr{Int64}, Ptr)
svec(Ptr{Int64}, svec(Int64))

So Int64 <: (Ptr.var) <: Int64

1 Like