Bonus Slides: Verifying range

range :: lo:_ -> hi:{lo <= hi} -> [{v:_ | lo <= v && v < hi}] 
range lo hi
  | lo < hi   = let tail = range (lo + 1) hi  ----------- (1)
                in  lo : tail -------------------- (2l,2t,2r)
  | otherwise = [] -------------------------------------- (3)  

Polymorphic Type and Instance for "Cons"

    (:) :: a -> [a] -> [a]
    (:) :: {v:Int|K(v)} -> [{v:Int|K(v)}] -> [{v:Int|K(v)}]

where a replaced with unknown {v:Int|K(v)}

Subtyping Constraints

range :: lo:_ -> hi:{lo <= hi} -> [{v:_ | lo <= v && v < hi}] 
range lo hi
  | lo < hi   = let tail = range (lo + 1) hi  ----------- (1)
                in  lo : tail -------------------- (2l,2t,2r)
  | otherwise = [] -------------------------------------- (3)  

Yields the Subtyping Constraints

lo < hi |- {v:Int|v = lo+1}     <: {v:Int|v <= hi}    -- (1)
lo < hi |- {v:Int|v = lo}       <: {v:Int|K(v)}       -- (2l)
lo < hi |- [{v:Int|lo+1<=v<hi}] <: [{v:Int|K(v)}]     -- (2t)
lo < hi |- [{v:Int|K(v)}]       <: [{v:Int|lo<=v<hi}] -- (2r)
lo >=hi |- [{v:Int|false}]      <: [{v:Int|lo<=v<hi}] -- (3)

Horn Constraints

range :: lo:_ -> hi:{lo <= hi} -> [{v:_ | lo <= v && v < hi}] 
range lo hi
  | lo < hi   = let tail = range (lo + 1) hi  ----------- (1)
                in  lo : tail -------------------- (2l,2t,2r)
  | otherwise = [] -------------------------------------- (3)  

List Subtyping reduces to element-wise Subtyping

lo < hi => (v = lo+1)   => (v <= hi)                  -- (1)
lo < hi => (v = lo)     => K(v)                       -- (2l)
lo < hi => (lo+1<=v<hi) => K(v)                       -- (2t)
lo < hi => K(v)         => (lo <= v < hi)             -- (2r)
lo >=hi => false        => (lo <= v < hi)             -- (3)

Solution: K(v) := lo <= v < hi