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}} @-}

Invariants In Constructors


Make illegal values unrepresentable!

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

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}> @-}

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

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]