Properties of Data Structures



So far: Refinements for properties of basic values like Int

e.g. {v:Int | lo <= v && v < hi}

Properties of Data Structures



So far: Refinements for properties of basic values like Int

e.g. {v:Int | lo <= v && v < hi}


Next: How to describe properties of data structures

Example: List average



Suppose we have a built-in div operator:

div :: Int -> {d:Int| d /= 0} -> Int


Input refinement specifies Pre-condition

Denominator d is non-zero

Example: List average


Lets use div to write an average function

{-@ average :: [Int] -> Int @-} average xs = let total = reduce (+) 0 xs n = length xs in div total n length :: [a] -> Int length [] = 0 length (_:t) = 1 + length t

Exercise: Why is there an error?

Properties of Structures


How to describe the size of a list?

Properties of Structures


How to describe the size of a list?


Allow Uninterpreted Functions Inside Refinements

Properties of Structures


Allow Uninterpreted Functions Inside Refinements

{-@ measure length @-}

Which lets us define a type alias

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

Exercise: Go back and fix average so it checks?

Properties of Structures


Measures Yield Refined Constructors

            []  :: {v:[a] | length v = 0}
            (:) :: a -> t:[a] -> {v:[a] | length v = 1 + length t}

Properties of Structures


Measures Yield Refined Constructors

            []  :: {v:[a] | length v = 0}
            (:) :: a -> t:[a] -> {v:[a] | length v = 1 + length t}

Where length is uninterpreted in refinement Logic

Properties of Structures


Measures Yield Refined Constructors

            []  :: {v:[a] | length v = 0}
            (:) :: a -> t:[a] -> {v:[a] | length v = 1 + length t}

Where length is uninterpreted in refinement Logic


Now plain refinement typing "just works" for properties of structures!

Example: map over Lists

A datatype for homework scores, function to compute their average:

data Hw = Hw { getName :: String -- ^ Student's Name , getScore :: Int -- ^ Student's Score } hwAverage :: [Hw] -> Int hwAverage hws = average (map getScore hws) map :: (a -> b) -> [a] -> [b] map f [] = [] map f (x:xs) = f x : map f xs

Exercise: What's the problem here? Can you fix it?

Recap: Properties of Structures


Measures specify properties as functions over Structures

                 {-@ measure length @-}
                 length       :: [a] -> Nat
                 length []    = 0
                 length (_:t) = 1 + length t

Recap: Properties of Structures


Measures specify properties as functions over Structures

                 {-@ measure length @-}
                 length       :: [a] -> Nat
                 length []    = 0
                 length (_:t) = 1 + length t

Refined Constructor Types

            []  :: {v:[a] | length v = 0}
            (:) :: a -> t:[a] -> {v:[a] | length v = 1 + length t}

Recap: Properties of Structures


Refined Constructor Types

            []  :: {v:[a] | length v = 0}
            (:) :: a -> t:[a] -> {v:[a] | length v = 1 + length t}

Generalize Properties

During construction i.e. applying type of [] and (:)


Recap: Properties of Structures


Refined Constructor Types

            []  :: {v:[a] | length v = 0}
            (:) :: a -> t:[a] -> {v:[a] | length v = 1 + length t}

Generalize Properties

During construction i.e. applying type of [] and (:)


Instantiate Properties

During pattern-matching i.e. unapplying type of [] and (:)

Multiple Measures are Conjoined



We wrote multiple measures for lists

                 length :: [a] -> Nat
                 elems  :: [a] -> Set a

Multiple Measures are Conjoined

We wrote multiple measures for lists

                 length :: [a] -> Nat
                 elems  :: [a] -> Set a

Their data constructor refinements are conjoined

        []  :: {v:[a] | length v = 0 && elems v = empty}
        (:) :: x:a -> xs:[a] -> {v:[a] |  length v = 1 + length xs
                                       && elems v  = addElem x  xs }

Allows programmer to easily extend properties