Data Types



















Example: Lists


Lets define our own List data type:


data List a = Emp -- Nil | (:::) a (List a) -- Cons













Specifying the Length of a List


Measure

Haskell function with a single equation per constructor


{-@ measure length @-} length :: List a -> Int length Emp = 0 length (_ ::: xs) = 1 + length xs













Specifying the Length of a List


Measure

Strengthens type of data constructor


data List a where

  Emp   :: {v:List a | length v = 0}

  (:::) :: x:a -> xs:List a
        -> {v:List a | length v = 1 + length xs}













Using Measures
















Exercise: Partial Functions


Fear head and tail no more!

{-@ head :: List a -> a @-} head (x ::: _) = x head _ = impossible "head" {-@ tail :: List a -> List a @-} tail (_ ::: xs) = xs tail _ = impossible "tail"



Q: Write types for head and tail that verify impossible.













Naming Non-Empty Lists


A convenient type alias


{-@ type ListNE a = {v:List a| 0 < length v} @-}

























Back to average


{-@ avg :: List Int -> Int @-} avg xs = safeDiv total n where total = sum xs n = length xs -- returns a Nat


Q: Write type for avg that verifies safe division.













Multiple Measures
















SMT Solvers Reason About Sets


Hence, we can write Set-valued measures


Using the Data.Set API for convenience


import qualified Data.Set as S













Specifying A Lists Elements


{-@ measure elems @-} elems :: (Ord a) => List a -> S.Set a elems Emp = S.empty elems (x:::xs) = addElem x xs {-@ inline addElem @-} addElem :: (Ord a) => a -> List a -> S.Set a addElem x xs = S.union (S.singleton x) (elems xs)


inline lets us reuse Haskell terms in refinements.













Multiple Measures


Measure

Strengthens type of data constructor


data List a where

  Emp   :: {v:List a | length v == 0 
                     && elems v == S.empty}


  (:::) :: x:a -> xs:List a
        -> {v:List a | length v == 1 + length xs
                     && elems v == addElem v xs  }













Example : Inserting Elements


{-@ insert :: x:a -> xs:List a -> {v : List a | length v == length xs + 1 && elems v == addElem x xs } @-} insert x Emp = x ::: Emp insert x (y ::: ys) | x <= y = x ::: y ::: ys | otherwise = y ::: insert x ys



Can we specify sortedness?













Refining Data Types



    Make illegal states unrepresentable













Example: Sorted Lists


Lets define a type for ordered lists


data OList a = OEmp | (:<:) { oHd :: a , oTl :: OList a }













Ordered Lists


Lets refine the type to enforce order


{-@ data OList a = OEmp | (:<:) { oHd :: a , oTl :: OList {v:a | oHd <= v}} @-}


Head oHd is smaller than every value v in tail oTl













Ordered Lists


Illegal values unrepresentable


okList :: OList Int okList = 1 :<: 2 :<: 3 :<: OEmp badList :: OList Int badList = 1 :<: 3 :<: 2 :<: OEmp













Exercise: Insertion Sort


Q: Oops. There's a problem! Can you fix it?


{-@ sortO :: xs:List a -> OList a @-} sortO Emp = OEmp sortO (x:::xs) = insertO x (sortO xs) {-@ insertO :: x:a -> xs:_ -> OList a @-} insertO x (y :<: ys) | x <= y = y :<: x :<: ys | otherwise = y :<: insertO x ys insertO x _ = x :<: OEmp














Measures vs. Indexed Types


Unlike indexed types, measures ...


  • Decouple properties from data type

  • Reuse same data type with different invariants













Refinements vs. Full Dependent Types


  • Limited to decidable logics but ...

  • Offer massive amounts of automation


Compare with insertionSort in:













Unfinished Business


Problem: How to reason about elems and lenght of an OList?


Solution: Make OList an instance of List using Abstract Refinements!
















Recap



  1. Refinements: Types + Predicates
  2. Subtyping: SMT Implication
  3. Measures: Specify Properties of Data


Next: Abstract Refinements