Skip to content

Commit

Permalink
juliatypes.jl: WIP on diagonal dispatch
Browse files Browse the repository at this point in the history 
[ci skip]
  • Loading branch information
@JeffBezanson
JeffBezanson committed Jan 22, 2015
1 parent fc61385 commit 4e66eb0
Showing 1 changed file with 42 additions and 7 deletions.
49 changes: 42 additions & 7 deletions examples/juliatypes.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,8 @@ type Bounds
lb
ub
right::Bool
concrete::Bool
Bounds(l,u,r) = new(l,u,r,false)
end

type UnionState
Expand Down Expand Up @@ -266,7 +268,7 @@ end
function isconcrete(v::Var, env)
b = env.vars[v]
#return issub(b.ub, b.lb, env)
return isconcrete(b.ub, env) # ???
return b.concrete || isconcrete(b.ub, env) # ???
end

function isconcrete(t::UnionAllT, env)
Expand Down Expand Up @@ -302,14 +304,15 @@ function issub(a::TagT, b::TagT, env)
bp = b.params[bi]
end
if isa(bp,Var) && env.vars[bp].right
if !isconcrete(ap, env)
ap = Var(:_,BottomT,ap)
env.vars[ap] = Bounds(BottomT, ap.ub, false)
if !isconcrete(env.vars[bp].lb, env)
return false
end
env.vars[bp].concrete = true
if isa(ap, Var)
env.vars[ap].concrete = true

This comment has been minimized.

Sign in to view

Copy link
@jakebolewski

jakebolewski Jan 23, 2015

Member

It looks like the logic a.concrete = false is being used to mean two things at the same time, namely "a is not concrete" and "a is not yet proven to be concrete".

The logical conflation shows up here because as ap or bp is determined to be concrete, other typevars in the environment which have ap or bp as upper bounds are not set to concrete = true and thus the type environment is in an inconsistent state.

In the example

    @test issub((@UnionAll T @UnionAll S<:T tupletype(T,S)),
                (@UnionAll R tupletype(R,R)))

issub(Tuple{T,S},Tuple{R,R}) is called. In this method call T is determined to be concrete and S<:T is in the type environment but S is not set to concrete even though S is only used in a covariant context in the tuple type (T, S). The type environment that results after this line is executed is therefore inconsistent with the covariant usage of S.

This comment has been minimized.

Sign in to view

Copy link
@jakebolewski

jakebolewski Jan 23, 2015

Member

This algorithm for deducing concreteness doesn't work when a typevar is used in both invariant and covariant contexts, e.g. in a type like (Array{(T,T)}, (T, T)).

For typevar T in Array{(T,T)} the issue with subtyping and bottom <: T shows up.

This comment has been minimized.

Sign in to view

Copy link
@JeffBezanson

JeffBezanson Jan 23, 2015

Author Member

It might help to mark typevars as concrete in advance based on where they appear. Maybe even during type construction.
end
!(issub(ap,bp,env) && issub(bp,ap,env)) && return false
else
!issub(ap, bp, env) && return false
end
!issub(ap, bp, env) && return false
end
return (la==lb && va==vb) || (vb && (la >= (va ? lb : lb-1)))
end
Expand Down Expand Up @@ -353,6 +356,9 @@ function var_lt(b::Var, a::Union(Ty,Var), env)
bb = env.vars[b]
!bb.right && return issub(bb.ub, a, env) # check ∀b . b<:a
!issub(bb.lb, a, env) && return false
if bb.concrete
!issub(a, bb.ub, env) && return false
end
# for contravariance we would need to compute a meet here, but
# because of invariance bb.ub ⊓ a == a here always. however for this
# to work we need to compute issub(left,right) before issub(right,left),
Expand All @@ -365,6 +371,9 @@ function var_gt(b::Var, a::Union(Ty,Var), env)
bb = env.vars[b]
!bb.right && return issub(a, bb.lb, env) # check ∀b . b>:a
!issub(a, bb.ub, env) && return false
if bb.concrete
!issub(bb.lb, a, env) && return false
end
bb.lb = join(bb.lb, a, env)
return true
end
Expand Down Expand Up @@ -517,6 +526,32 @@ using Base.Test

issub_strict(x,y) = issub(x,y) && !issub(y,x)

function test_diagonal()
@test !issub(Ty((Integer,Integer)), @UnionAll T tupletype(T,T))
@test !issub(Ty((Integer,Int)), (@UnionAll T @UnionAll S<:T tupletype(T,S)))
@test !issub(Ty((Integer,Int)), (@UnionAll T @UnionAll T<:S<:T tupletype(T,S)))

@test issub((@UnionAll R tupletype(R,R)),
(@UnionAll T @UnionAll S tupletype(T,S)) )
@test issub((@UnionAll R tupletype(R,R)),
(@UnionAll T @UnionAll S<:T tupletype(T,S)) )
@test issub((@UnionAll R tupletype(R,R)),
(@UnionAll T @UnionAll T<:S<:T tupletype(T,S)) )
@test issub((@UnionAll R tupletype(R,R)),
(@UnionAll T @UnionAll S>:T tupletype(T,S)) )

@test !issub((@UnionAll T @UnionAll S tupletype(T,S)),
(@UnionAll R tupletype(R,R)))

@test issub((@UnionAll T @UnionAll S<:T tupletype(T,S)),

This comment has been minimized.

Sign in to view

Copy link
@jakebolewski

jakebolewski Jan 23, 2015

Member

@JeffBezanson, swapping T and S here (in the tuple) allows the test to pass.

This comment has been minimized.

Sign in to view

Copy link
@JeffBezanson

JeffBezanson Jan 23, 2015

Author Member

Switching <: to >: has the same effect.

This comment has been minimized.

Sign in to view

Copy link
@jakebolewski

jakebolewski Jan 23, 2015

Member

Why does the ordering of the TypeVar's in the tuple matter?

This comment has been minimized.

Sign in to view

Copy link
@JeffBezanson

JeffBezanson Jan 23, 2015

Author Member

Well, there must be some unwanted asymmetry in the algorithm somewhere.
(@UnionAll R tupletype(R,R)))

@test issub((@UnionAll T @UnionAll T<:S<:T tupletype(T,S)),
(@UnionAll R tupletype(R,R)))

end


# level 1: no varags, union, UnionAll
function test_1()
@test issub_strict(Int, Integer)
Expand Down

0 comments on commit 4e66eb0

Please sign in to comment.