Structural Induction



How we express and prove properties on data types?


{-# LANGUAGE TupleSections #-} module StructuralInduction where import Prelude hiding (map, id, length, return) import Language.Haskell.Liquid.ProofCombinators

The list data type


A user defined list,

data L a = N | C a (L a) {-@ data L [length] @-}

with its anchored size function.

{-@ measure length @-} {-@ length :: L a -> Nat @-} length N = 0 length (C _ xs) = 1 + length xs

Definition of Structural Inductive Functions


{-@ reflect map @-} map :: (a -> b) -> L a -> L b map f N = N map f (C x xs) = f x `C` map f xs

Definition of Non Recursive Functions


Non-recursive functions reflect too!

{-@ reflect id @-} id :: a -> a id x = x {-@ reflect compose @-} compose :: (b -> c) -> (a -> b) -> a -> c compose f g x = f (g x)

Proving Map-Identity


Optimization property: to map identity do not transverse the list!

{-@ mapId :: xs:L a -> { map id xs == id xs } @-} mapId N = map id N ==. N ==. id N *** QED mapId (C x xs) = map id (C x xs) ==. id x `C` map id xs ==. x `C` map id xs ==. x `C` id xs ? mapId xs ==. x `C` xs ==. id (x `C` xs) *** QED

Proof by case splitting and recursive call.

Automation: Proving Map-Identity


Pretty Verbose Proof: Proof Automation!

{-@ LIQUID "--automatic-instances=liquidinstanceslocal" @-}
{-@ automatic-instances mapIdAuto @-} {-@ mapIdAuto :: xs:L a -> { map id xs == id xs } @-} mapIdAuto N = trivial mapIdAuto (C x xs) = mapIdAuto xs

Proof Generation:

  • Automatic Unfolding, but
  • Manual case splitting.

Proving Map-Fusion


Optimization property: transverse the list only once!

{-@ automatic-instances mapFusion @-} {-@ mapFusion :: f:(b -> c) -> g:(a -> b) -> xs:L a -> { map (compose f g) xs == (map f) (map g xs) } @-} mapFusion f g xs = undefined "Prove me!"

Exercise: Can you prove map-fusion?

Onto Monoid Laws


Reflect the monoid list operators


{-@ reflect append @-} append :: L a -> L a -> L a append N ys = ys append (C x xs) ys = x `C` append xs ys {-@ reflect empty @-} empty :: L a empty = N

Monoid Laws: Left Identity


Lets prove the left identity monoid law!

{-@ automatic-instances emptyLeft @-} {-@ emptyLeft :: x:L a -> { append empty x == x } @-} emptyLeft x = undefined "Prove me!"

Monoid Laws: Right Identity


Lets prove the right identity monoid law!

{-@ automatic-instances emptyRight @-} {-@ emptyRight :: x:L a -> { append x empty == x } @-} emptyRight _ = undefined "Prove me!"

Monoid Laws: Associativity


Lets prove the associativity monoid law!

{-@ automatic-instances appendAssoc @-} {-@ appendAssoc :: xs:L a -> ys:L a -> zs:L a -> {append xs (append ys zs) == append (append xs ys) zs } @-} appendAssoc _ _ _ = undefined "Prove me!"

Onto Monad Laws!


Define monad list operators

{-@ reflect return @-} return :: a -> L a return x = C x N {-@ reflect bind @-} bind :: L a -> (a -> L b) -> L b bind N _ = N bind (C x xs) f = append (f x) (bind xs f)

Monad Laws: Left Identity


Lets prove the left identity monad law!

{-@ automatic-instances leftIdentity @-} {-@ leftIdentity :: x:a -> f:(a -> L b) -> { bind (return x) f == f x } @-} leftIdentity x f = undefined "Prove me!"

Monad Laws: Right Identity


Lets prove the right identity monad law!

{-@ automatic-instances rightIdentity @-} {-@ rightIdentity :: x:L a -> { bind x return == x } @-} rightIdentity _ = undefined "Prove me!"

Monad Laws: Associativity


To prove associativity, lets assume a helper lemma!

  • Bind distribution
{-@ automatic-instances bindAppend @-} {-@ bindAppend :: xs:L a -> ys:L a -> f:(a -> L b) -> { bind (append xs ys) f == append (bind xs f) (bind ys f) } @-} bindAppend N _ _ = trivial bindAppend (C x xs) ys f = appendAssoc (f x) (bind xs f) (bind ys f) &&& bindAppend xs ys f

Monad Laws: Associativity


Lets prove the associativity monad law!

{-@ automatic-instances associativity @-} {-@ associativity :: m:L a -> f: (a -> L b) -> g:(b -> L c) -> {bind (bind m f) g == bind m (\x:a -> (bind (f x) g)) } @-} associativity m f g = undefined "Prove me!"

Prove fancy lists properties

  • Functor Laws
    • Identity: map id == id
    • Distribution: map (compose f g) == compose (map f) (map g)


  • Monoid Laws
    • Left Identity: append empty x == x
    • Right Identity: append x empty == x
    • Associativity: append xs (append ys zs) == append (append xs ys) zs


  • Monad Laws
    • Left Identity: bind (return x) f == f x
    • Right Identity: bind x return == x
    • Associativity: bind (bind m f) g == bind m (\x:a -> (bind (f x) g))

Recap


Refinements: Types + Predicates
Specification: Refined Input/Output Types
Verification: SMT-based Predicate Subtyping
Measures: Specify Properties of Data
Termination: Well-founded Metrics
Programs as Proofs: Theorem Proving in Haskell
Structural Induction: Theorems about Data Types



Next: Case Study: MapReduce: Program Properties that matter!

Appendix

{-@ LIQUID "--betaequivalence" @-} {-@ LIQUID "--higherorder" @-} {-@ LIQUID "--exact-data-cons" @-} length :: L a -> Int mapFusion :: (b -> c) -> (a -> b) -> L a -> Proof mapId :: L a -> Proof mapIdAuto :: L a -> Proof emptyLeft :: L a -> Proof emptyRight :: L a -> Proof appendAssoc :: L a -> L a -> L a -> Proof leftIdentity :: a -> (a -> L b) -> Proof rightIdentity :: L a -> Proof associativity :: L a -> (a -> L b) -> (b -> L c) -> Proof