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

**URL:** <https://discourse.julialang.org/t/unification-or-pattern-matching-for-matching-unionall-types-against-each-other/32217>\
**Category:** Internals & Design\
**Tags:** type, parametric-types\
**Created:** [December 13, 2019, 12:51am UTC](https://discourse.julialang.org/t/unification-or-pattern-matching-for-matching-unionall-types-against-each-other/32217 "2019-12-13T00:51:27Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![goretkin](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/goretkin/32/167_2.png) [@goretkin](https://discourse.julialang.org/u/goretkin)\
**Post date:** [December 13, 2019, 12:51am UTC](https://discourse.julialang.org/t/unification-or-pattern-matching-for-matching-unionall-types-against-each-other/32217/1 "2019-12-13T00:51:27Z")

</div>

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.

```julia
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.:

```julia
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](https://stackoverflow.com/questions/4442314/differences-between-pattern-matching-and-unification) and [Unification (computer science) - Wikipedia](https://en.wikipedia.org/wiki/Unification_(computer_science))

---

<div class="post-metadata">

**Author:** ![jameson](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/jameson/32/23_2.png) [@jameson](https://discourse.julialang.org/u/jameson)\
**Post date:** [December 16, 2019, 4:33pm UTC](https://discourse.julialang.org/t/unification-or-pattern-matching-for-matching-unionall-types-against-each-other/32217/2 "2019-12-16T16:33:34Z")

</div>

> `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.

---

<div class="post-metadata">

**Author:** ![goretkin](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/goretkin/32/167_2.png) [@goretkin](https://discourse.julialang.org/u/goretkin)\
**Post date:** [December 16, 2019, 5:26pm UTC](https://discourse.julialang.org/t/unification-or-pattern-matching-for-matching-unionall-types-against-each-other/32217/3 "2019-12-16T17:26:50Z")

</div>

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

```julia
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.

---

<div class="post-metadata">

**Author:** ![goretkin](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/goretkin/32/167_2.png) [@goretkin](https://discourse.julialang.org/u/goretkin)\
**Post date:** [December 16, 2019, 6:47pm UTC](https://discourse.julialang.org/t/unification-or-pattern-matching-for-matching-unionall-types-against-each-other/32217/4 "2019-12-16T18:47:45Z")

</div>

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:

```julia
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})

```

---

<div class="post-metadata">

**Author:** ![jameson](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/jameson/32/23_2.png) [@jameson](https://discourse.julialang.org/u/jameson)\
**Post date:** [December 16, 2019, 7:02pm UTC](https://discourse.julialang.org/t/unification-or-pattern-matching-for-matching-unionall-types-against-each-other/32217/5 "2019-12-16T19:02:39Z")

</div>

The env is computed for the argument on the right

---

<div class="post-metadata">

**Author:** ![goretkin](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/goretkin/32/167_2.png) [@goretkin](https://discourse.julialang.org/u/goretkin)\
**Post date:** [December 16, 2019, 7:15pm UTC](https://discourse.julialang.org/t/unification-or-pattern-matching-for-matching-unionall-types-against-each-other/32217/6 "2019-12-16T19:15:55Z")

</div>

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

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

```

---

<div class="post-metadata">

**Author:** ![jameson](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/jameson/32/23_2.png) [@jameson](https://discourse.julialang.org/u/jameson)\
**Post date:** [December 16, 2019, 7:25pm UTC](https://discourse.julialang.org/t/unification-or-pattern-matching-for-matching-unionall-types-against-each-other/32217/7 "2019-12-16T19:25:50Z")

</div>

`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`).

---

<div class="post-metadata">

**Author:** ![goretkin](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/goretkin/32/167_2.png) [@goretkin](https://discourse.julialang.org/u/goretkin)\
**Post date:** [December 16, 2019, 8:08pm UTC](https://discourse.julialang.org/t/unification-or-pattern-matching-for-matching-unionall-types-against-each-other/32217/8 "2019-12-16T20:08:46Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![jameson](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/jameson/32/23_2.png) [@jameson](https://discourse.julialang.org/u/jameson)\
**Post date:** [December 16, 2019, 8:23pm UTC](https://discourse.julialang.org/t/unification-or-pattern-matching-for-matching-unionall-types-against-each-other/32217/9 "2019-12-16T20:23:43Z")

</div>

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

```

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