Invariants In Constructors


Many many possibilities ...

Invariants In Constructors


Lets specify ordered lists:

{-@ data OList a = Emp
                 | (:<) { hd :: a
                        , tl :: OList {v:a | hd <= v}}
  @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Invariants In Constructors


Make illegal values unrepresentable!

ok :: OList Int
ok = 1 :< 2 :< 3 :< Emp
bad :: OList Int
bad = 1 :< 3 :< 2 :< Emp
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Invariants In Constructors


Make illegal values unrepresentable!


But its tedious to have multiple list types ...

Abstracting Refinements


Parameterize types over refinements! [ESOP 13]

Abstracting Refinements


Parameterize types over refinements! [ESOP 13]


data [a]<p :: a -> a -> Prop> where
  = []
  | (:) { hd :: a
        , tl :: [{v:a | p hd v}]}

Abstracting Refinements


Instantiate refinements to get different invariants!


{-@ type Incrs a = [a]<{\x y -> x <= y}> @-}
{-@ type Decrs a = [a]<{\x y -> x >= y}> @-}
{-@ type Diffs a = [a]<{\x y -> x /= y}> @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Using Abstract Refinements


Inference FTW!


{-@ insertSort :: (Ord a) => [a] -> Incrs a @-}
insertSort xs = foldr insert [] xs
insert x []     = [x]
insert x (y:ys)
  | x < y       = x : y : ys
  | otherwise   = y : insert x ys
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Recap


Abstract Refinements

Parametric Polymorphism for Refinement Types

Recap


Abstract Refinements

Parametric Polymorphism for Refinement Types


Bounded Refinements

Bounded Quantification for Refinement Types

[IFCP 2015]

Bounded Refinements


The bound Inductive says relation step preserves inv

Inductive inv step = \y ys acc v ->
  inv ys acc ==> step y acc v ==> inv (y:ys) v

Bounded Refinements


The bound Inductive says relation step preserves inv

Inductive inv step = \y ys acc v ->
  inv ys acc ==> step y acc v ==> inv (y:ys) v

Key Idea

Bound is a Horn Clause over (Abstract) Refinements

Bounded Refinements


The type of foldr encodes induction over lists ...

foldr :: (Inductive inv step)
      => (x:a -> acc:b -> b<step x acc>)
      -> b<inv []>
      -> xs:[a]
      -> b<inv xs>

Bounded Refinements


... and lets us verify:

insertSort :: (Ord a)
           => xs:[a]
           -> {v:Incrs a | elts v == elts xs}

insertSort = foldr insert []

[continue]