appa.tex

\chapter{Subtyping algorithm}
\label{appendix:subtyping}

\begin{singlespace}
\begin{multicols}{2}
\begin{lstlisting}[language=julia]
abstract Ty

type TypeName
  super::Ty
  TypeName() = new()
end

type TagT <: Ty
  name::TypeName
  params
  vararg::Bool
end

type UnionT <: Ty
  a; b
end

type Var
  lb; ub
end

type UnionAllT <: Ty
  var::Var
  T
end
\end{lstlisting}
\end{multicols}

\vspace{-3ex}
\begin{lstlisting}[language=julia]
## Any, Bottom, and Tuple
const AnyT = TagT(TypeName(),(),false); AnyT.name.super = AnyT
type BottomTy <: Ty; end; const BottomT = BottomTy()
const TupleName = TypeName(); TupleName.super = AnyT

super(t::TagT) =
  t.name===TupleName ? AnyT : inst(t.name.super, t.params...)

## type application
inst(t::TagT) = t
inst(t::UnionAllT, param) = subst(t.T, Dict(t.var => param))
inst(t::UnionAllT, param, rest...) = inst(inst(t,param), rest...)

subst(t,          env) = t
subst(t::TagT,    env) =
  t===AnyT ? t : TagT(t.name, map(x->subst(x,env), t.params),
                      t.vararg)
subst(t::UnionT,  env) = UnionT(subst(t.a,env), subst(t.b,env))
subst(t::Var,     env) = get(env, t, t)
function subst(t::UnionAllT, env)
  newVar = Var(subst(t.var.lb,env), subst(t.var.ub,env))
  UnionAllT(newVar, subst(t.T, merge(env, Dict(t.var=>newVar))))
end

rename(t::UnionAllT) = let v = Var(t.var.lb, t.var.ub)
  UnionAllT(v, inst(t,v))
end

type Bounds
  lb; ub       # current lower and upper bounds of a Var
  right::Bool  # this Var is on the right-hand side of A <: B
end

type UnionState
  depth::Int           # number of nested union decision points
  more::Bool           # new union found; need to grow stack
  stack::Vector{Bool}  # stack of decisions
  UnionState() = new(1,0,Bool[])
end

type Env
  vars::Dict{Var,Bounds}
  Lunions::UnionState
  Runions::UnionState
  Env() = new(Dict{Var,Bounds}(), UnionState(), UnionState())
end

issub(x, y)              = forall_exists_issub(x, y, Env(), false)
issub(x, y, env)         = (x === y)
issub(x::Ty, y::Ty, env) = (x === y) || x === BottomT

function forall_exists_issub(x, y, env, anyunions::Bool)
  for forall in false:anyunions
    if !isempty(env.Lunions.stack)
      env.Lunions.stack[end] = forall
    end

    !exists_issub(x, y, env, false) && return false

    if env.Lunions.more
      push!(env.Lunions.stack, false)
      sub = forall_exists_issub(x, y, env, true)
      pop!(env.Lunions.stack)
      !sub && return false
    end end
  return true
end

function exists_issub(x, y, env, anyunions::Bool)
  for exists in false:anyunions
    if !isempty(env.Runions.stack)
      env.Runions.stack[end] = exists
    end
    env.Lunions.depth = env.Runions.depth = 1
    env.Lunions.more = env.Runions.more = false

    found = issub(x, y, env)

    if env.Lunions.more
      return true  # return up to forall_exists_issub
    end
    if env.Runions.more
      push!(env.Runions.stack, false)
      found = exists_issub(x, y, env, true)
      pop!(env.Runions.stack)
    end
    found && return true
  end
  return false
end

function issub_union(t, u::UnionT, env, R)
  state = R ? env.Runions : env.Lunions
  if state.depth > length(state.stack)
    state.more = true
    return true
  end
  ui = state.stack[state.depth]; state.depth += 1
  choice = getfield(u, 1+ui)
  return R ? issub(t, choice, env) : issub(choice, t, env)
end

issub(a::UnionT, b::UnionT, env) = issub_union(a, b, env, true)
issub(a::UnionT, b::Ty, env)     = issub_union(b, a, env, false)
issub(a::Ty, b::UnionT, env)     = issub_union(a, b, env, true)
# take apart unions before handling vars
issub(a::UnionT, b::Var, env)    = issub_union(b, a, env, false)
issub(a::Var, b::UnionT, env)    = issub_union(a, b, env, true)

function issub(a::TagT, b::TagT, env)
  a === b && return true
  b === AnyT && return true
  a === AnyT && return false
  if a.name !== b.name
    return issub(super(a), b, env)
  end
  if a.name === TupleName
    va, vb = a.vararg, b.vararg
    la, lb = length(a.params), length(b.params)
    ai = bi = 1
    while ai <= la
      bi > lb && return false
      !issub(a.params[ai], b.params[bi], env) && return false
      ai += 1
      if bi < lb || !vb
        bi += 1
      end end
    return (la==lb && va==vb) || (vb && (la >= (va ? lb : lb-1)))
  end
  for i = 1:length(a.params)
    ai, bi = a.params[i], b.params[i]
    (issub(ai, bi, env) && issub(bi, ai, env)) || return false
  end
  return true
end

function join(a,b,env)
  (a===BottomT || b===AnyT || a === b) && return b
  (b===BottomT || a===AnyT) && return a
  UnionT(a,b)
end

issub(a::Ty, b::Var, env) = var_gt(b, a, env)
issub(a::Var, b::Ty, env) = var_lt(a, b, env)
function issub(a::Var, b::Var, env)
  a === b && return true
  aa = env.vars[a]; bb = env.vars[b]
  if aa.right
    bb.right && return issub(bb.ub, bb.lb, env)
    return var_lt(a, b, env)
  else
    if !bb.right   # check ~$\forall$~a,b . a<:b
      return issub(aa.ub, b, env) || issub(a, bb.lb, env)
    end
    return var_gt(b, a, env)
  end
end

function var_lt(b::Var, a::Union(Ty,Var), env)
  bb = env.vars[b]
  !bb.right && return issub(bb.ub, a, env)  # check ~$\forall$~b . b<:a
  !issub(bb.lb, a, env) && return false
  # for contravariance we would need to compute a meet here, but
  # because of invariance bb.ub ~$\sqcap$~ a == a here always.
  bb.ub = a  # meet(bb.ub, a)
  return true
end

function var_gt(b::Var, a::Union(Ty,Var), env)
  bb = env.vars[b]
  !bb.right && return issub(a, bb.lb, env)  # check ~$\forall$~b . b>:a
  !issub(a, bb.ub, env) && return false
  bb.lb = join(bb.lb, a, env)
  return true
end

function issub_uall(t::Ty, u::UnionAllT, env, R)
  haskey(env.vars, u.var) && (u = rename(u))
  env.vars[u.var] = Bounds(u.var.lb, u.var.ub, R)
  ans = R ? issub(t, u.T, env) : issub(u.T, t, env)
  delete!(env.vars, u.var)
  return ans
end

issub(a::UnionAllT, b::UnionAllT, env) = issub_uall(a,b,env,true)
issub(a::UnionT, b::UnionAllT, env)    = issub_uall(a,b,env,true)
issub(a::UnionAllT, b::UnionT, env)    = issub_uall(b,a,env,false)
issub(a::Ty, b::UnionAllT, env)        = issub_uall(a,b,env,true)
issub(a::UnionAllT, b::Ty, env)        = issub_uall(b,a,env,false)

\end{lstlisting}
\end{singlespace}