content: Numeric Measures {#numericmeasure}
  ================
  
  \begin{comment}
  \begin{code}
  {-@ LIQUID "--short-names"    @-}
  {-@ LIQUID "--no-termination" @-}
  
  module Tutorial_07_Measure_Int where
  import Prelude  hiding  (map, zipWith, zip, take, drop, reverse)
  
  {-@ type TRUE = {v:Bool | v} @-}
  
  {-@ die :: {v:_ | false} -> a @-}
  die msg = error msg
  take, drop, take' :: Int -> [a] -> [a]
  txgo              :: Int -> Int -> Vector (Vector a) -> Vector (Vector a)
  quickSort         :: (Ord a) => [a] -> [a]
  size              :: [a] -> Int
  flatten :: Int -> Int -> Vector (Vector a) -> Vector a
  test4 :: [String]
  
  -- {-@ ignore dotProd @-}
  -- {-@ ignore matProd @-}
  -- {-@ ignore prop_map @-}
  -- {-@ ignore reverse @-}
  -- {-@ fail test1 @-}
  -- {-@ fail test2 @-}
  -- {-@ fail test3 @-}
  -- {-@ fail test4 @-}
  -- {-@ fail test5 @-}
  -- {-@ fail test6 @-}
  -- {-@ fail test10 @-}
  -- {-@ ignore drop @-}
  -- {-@ ignore zipOrNull @-}
  -- {-@ fail badVec @-}
  -- {-@ fail product @-}
  -- {-@ fail bad1 @-}
  -- {-@ fail bad2 @-}
  -- {-@ fail mat23 @-}
  -- {-@ fail matProduct @-}
  
  -- {-@ ignore for @-}
  \end{code}
  \end{comment}
  
  
  Many of the programs we have seen so far, for example those in
  [here](#vectorbounds), suffer from *indexitis*. This is a term
  coined by [Richard Bird][bird-pearls] which describes a tendency
  to perform low-level manipulations to iterate over the indices
  into a collection, opening the door to various off-by-one
  errors. Such errors can be eliminated by instead programming
  at a higher level, using a [wholemeal approach][hinze-icfp09]
  where the emphasis is on using aggregate operations, like `map`,
  `fold` and `reduce`.
  
  \newthought{Wholemeal programming is no panacea} as it still
  requires us to take care when operating on *different* collections;
  if these collections are *incompatible*, e.g. have the wrong dimensions,
  then we end up with a fate worse than a crash, a possibly meaningless
  result. Fortunately, LiquidHaskell can help. Lets see how we can use
  measures to specify dimensions and create a dimension-aware API for
  lists which can be used to implement wholemeal
  dimension-safe APIs.^[In a [later chapter](#kmeans-case-study)
  we will use this API to implement K-means clustering.]
  
  Wholemeal Programming
  ---------------------
  
  Indexitis begone! As an example of wholemeal programming, let's
  write a small library that represents vectors as lists and
  matrices as nested vectors:
  
  \begin{code}
  data Vector a = V { vDim  :: Int
                    , vElts :: [a]
                    }
                deriving (Eq)
  
  data Matrix a = M { mRow  :: Int
                    , mCol  :: Int
                    , mElts :: Vector (Vector a)
                    }
                deriving (Eq)
  \end{code}
  
  \newthought{The Dot Product} of two `Vector`s can be easily computed using a fold:
  
  \begin{code}
  dotProd       :: (Num a) => Vector a -> Vector a -> a
  dotProd vx vy = sum (prod xs ys)
    where
      prod      = zipWith (\x y -> x * y)
      xs        = vElts vx
      ys        = vElts vy
  \end{code}
  
  \newthought{Matrix Multiplication} can similarly be expressed
  in a high-level, wholemeal fashion, by eschewing low level index
  manipulations in favor of a high-level *iterator* over the `Matrix` elements:
  
  \begin{code}
  matProd       :: (Num a) => Matrix a -> Matrix a -> Matrix a
  matProd (M rx _ xs) (M _ cy ys)
                = M rx cy elts
    where
      elts      = for xs (\xi ->
                    for ys (\yj ->
                      dotProd xi yj
                    )
                  )
  \end{code}
  
  \newthought{The Iteration} embodied by the `for` combinator, is simply
  a `map` over the elements of the vector.
  
  ~~~~~{.spec}
  for            :: Vector a -> (a -> b) -> Vector b
  for (V n xs) f = V n (map f xs)
  ~~~~~
  
  \newthought{Wholemeal programming frees} us from having to fret
  about low-level index range manipulation, but is hardly a panacea.
  Instead, we must now think carefully about the *compatibility*
  of the various aggregates. For example,
  
  + `dotProd` is only sensible on vectors of the same dimension;
    if one vector is shorter than another (i.e. has fewer elements)
    then we will won't get a run-time crash but instead will get
    some gibberish result that will be dreadfully hard to debug.
  
  + `matProd` is only well defined on matrices of compatible
    dimensions; the number of columns of `mx` must equal the
    number of rows  of `my`. Otherwise, again, rather than an
    error, we will get the wrong output.^[In fact, while the
    implementation of `matProd` breezes past GHC it is quite
    wrong!]
  
  Specifying List Dimensions
  --------------------------
  
  In order to start reasoning about dimensions, we need a way
  to represent the *dimension* of a list inside the refinement
  logic. ^[We could just use `vDim`, but that is a cheat as
  there is no guarantee that the field's value actually equals
  the size of the list!]
  
  \newthought{Measures} are ideal for this
  task. [Previously](#boolmeasures) we saw how we could lift
  Haskell functions up to the refinement logic. Lets write a
  measure to describe the length of a list: ^[[Recall](#usingmeasures)
  that these must be inductively defined functions, with a single
  equation per data-constructor]
  
  \begin{code}
  {-@ measure size @-}
  {-@ size :: [a] -> Nat @-}
  size []     = 0
  size (_:rs) = 1 + size rs
  \end{code}
  
  \newthought{Measures Refine Constructors}
  As with [refined data definitions](#autosmart), the
  measures are translated into strengthened types for
  the type's constructors. For example, the `size`
  measure is translated into:
  
  ~~~~~{.spec}
  data [a] where
    []  :: {v: [a] | size v = 0}
    (:) :: a -> xs:[a] -> {v:[a]|size v = 1 + size xs}
  ~~~~~
  
  \newthought{Multiple Measures} may be defined for the same data
  type. For example, in addition to the `size` measure, we can define a
  `notEmpty` measure for the list type:
  
  \begin{code}
  {-@ measure notEmpty @-}
  notEmpty       :: [a] -> Bool
  notEmpty []    = False
  notEmpty (_:_) = True
  \end{code}
  
  
  \newthought{We Compose Different Measures}
  simply by *conjoining* the refinements in the strengthened
  constructors. For example, the two measures for lists end
  up yielding the constructors:
  
  ~~~~~{.spec}
  data [a] where
    []  :: {v: [a] | not (notEmpty v) && size v = 0}
    (:) :: a
        -> xs:[a]
        -> {v:[a]| notEmpty v && size v = 1 + size xs}
  ~~~~~
  
  \noindent
  This is a very significant advantage of using measures
  instead of indices as in [DML][dml] or [Agda][agdavec],
  as *decouples property from structure*, which crucially
  enables the use of the same structure for many different
  purposes. That is, we need not know *a priori* what indices
  to bake into the structure, but can define a generic
  structure and refine it *a posteriori* as needed with
  new measures.
  
  We are almost ready to begin creating a dimension aware API
  for lists; one last thing that is useful is a couple of aliases
  for describing lists of a given dimension.
  
  \newthought{To make signatures symmetric} let's define an alias for
  plain old (unrefined) lists:
  
  \begin{code}
  type List a = [a]
  \end{code}
  
  <div class="toolinfo">
  \newthought{A ListN} is a list with exactly `N` elements, and a
  `ListX` is a list whose size is the same as another list `X`.  Note
  that when defining refinement type aliases, we use uppercase variables
  like `N` and `X` to distinguish *value* parameters from the lowercase
  *type* parameters like `a`.
  </div>
  
  \begin{code}
  {-@ type ListN a N = {v:List a | size v = N} @-}
  {-@ type ListX a X = ListN a {size X}        @-}
  \end{code}
  
  
  Lists: Size Preserving API
  --------------------------
  
  With the types and aliases firmly in our pockets, let us
  write dimension-aware variants of the usual list functions.
  The implementations are the same as in the standard library
  i.e. [`Data.List`][data-list], but the specifications are
  enriched with dimension information.
  
  <div class="hwex" id="Map">
  \newthought{map} yields a list with the same size as the input.
  Fix the specification of `map` so that the `prop_map` is verified.
  </div>
  
  \begin{code}
  {-@ map      :: (a -> b) -> xs:List a -> List b @-}
  map _ []     = []
  map f (x:xs) = f x : map f xs
  
  {-@ prop_map :: List a -> TRUE @-}
  prop_map xs = size ys == size xs
    where
      ys      = map id xs
  \end{code}
  
  <div class="hwex" id="Reverse"> \singlestar
  We can `reverse` the elements of a list as shown below, using the
  tail recursive function `go`. Fix the signature for `go`
  so that LiquidHaskell can prove the specification for `reverse`.
  </div>
  
  \hint How big is the list returned by `go`?
  
  \begin{code}
  {-@ reverse       :: xs:List a -> ListX a xs @-}
  reverse xs        = go [] xs
    where
      go acc []     = acc
      go acc (x:xs) = go (x:acc) xs
  \end{code}
  
  
  \newthought{zipWith} requires both lists to have the *same* size,
  and produces a list with that same size. ^[As made explicit by
  the call to `die`, the input type *rules out* the case where one
  list is empty and the other is not, as in that case the former's
  length is zero while the latter's is not, and hence, different.]
  
  \begin{code}
  {-@ zipWith :: (a -> b -> c) -> xs:List a
                               -> ListX b xs
                               -> ListX c xs
    @-}
  zipWith f (a:as) (b:bs) = f a b : zipWith f as bs
  zipWith _ [] []         = []
  zipWith _ _  _          = die "no other cases"
  \end{code}
  
  \newthought{unsafeZip} The signature for `zipWith` is quite severe -- it
  rules out the case where the zipping occurs only up to the shorter input.
  Here's a function that actually allows for that case, where the output
  type is the *shorter* of the two inputs:
  
  \begin{code}
  {-@ zip :: as:[a] -> bs:[b] -> {v:[(a,b)] | Tinier v as bs} @-}
  zip (a:as) (b:bs) = (a, b) : zip as bs
  zip [] _          = []
  zip _  []         = []
  \end{code}
  
  \noindent The output type uses the predicate `Tinier Xs Ys Zs`
  which defines the length of `Xs` to be the smaller of that of
  `Ys` and `Zs`.^[In logic, `if p then q else r` is the same as
  `p => q && not p => r`.]
  
  \begin{code}
  {-@ predicate Tinier X Y Z = Min (size X) (size Y) (size Z) @-}
  {-@ predicate Min X Y Z = (if Y < Z then X = Y else X = Z)  @-}
  \end{code}
  
  
  
  
  <div class="hwex" id="Zip Unless Empty"> \doublestar
  In my experience, `zip` as shown above is far too
  permissive and lets all sorts of bugs into my code. As middle
  ground, consider `zipOrNull` below. Write a specification
  for `zipOrNull` such that the code below is verified by
  LiquidHaskell.
  </div>
  
  \begin{code}
  zipOrNull       :: [a] -> [b] -> [(a, b)]
  zipOrNull [] _  = []
  zipOrNull _ []  = []
  zipOrNull xs ys = zipWith (,) xs ys
  
  {-@ test1 :: {v: _ | size v = 2} @-}
  test1     = zipOrNull [0, 1] [True, False]
  
  {-@ test2 :: {v: _ | size v = 0} @-}
  test2     = zipOrNull [] [True, False]
  
  {-@ test3 :: {v: _ | size v = 0} @-}
  test3     = zipOrNull ["cat", "dog"] []
  \end{code}
  
  \hint Yes, the type is rather gross; it uses a bunch of
        disjunctions `||` , conjunctions `&&` and implications `=>`.
  
  Lists: Size Reducing API {#listreducing}
  ------------------------
  
  Next, let's look at some functions that truncate lists, in one way or another.
  
  \newthought{Take} lets us grab the first `k` elements from a list:
  
  \begin{code}
  {-@ take'     :: n:Nat -> ListGE a n -> ListN a n @-}
  take' 0 _      = []
  take' n (x:xs) = x : take' (n-1) xs
  take' _ _      = die "won't  happen"
  \end{code}
  
  \noindent The alias `ListGE a n` denotes lists whose
  length is at least `n`:
  
  \begin{code}
  {-@ type ListGE a N = {v:List a | N <= size v} @-}
  \end{code}
  
  <div class="hwex" id="Drop">
  `Drop` is the yang to `take`'s yin: it returns the remainder after extracting
  the first `k` elements. Write a suitable specification for it so that the below
  typechecks.
  </div>
  
  \begin{code}
  drop 0 xs     = xs
  drop n (_:xs) = drop (n-1) xs
  drop _ _      = die "won't happen"
  
  {-@ test4 :: ListN String 2 @-}
  test4 = drop 1 ["cat", "dog", "mouse"]
  \end{code}
  
  <div class="hwex" id="Take it easy">
  The version `take'` above is too restrictive;
  it insists that the list actually have at least `n` elements.
  Modify the signature for the *real* `take` function so that
  the code below is accepted by LiquidHaskell.
  </div>
  
  \begin{code}
  take 0 _       = []
  take _ []      = []
  take n (x:xs)  = x : take (n-1) xs
  
  {-@ test5 :: [ListN String 2] @-}
  test5 = [ take 2  ["cat", "dog", "mouse"]
          , take 20 ["cow", "goat"]        ]
  \end{code}
  
  \newthought{The Partition} function breaks a list into two
  sub-lists of elements that either satisfy or fail a user
  supplied predicate.
  
  \begin{code}
  partition          :: (a -> Bool) -> [a] -> ([a], [a])
  partition _ []     = ([], [])
  partition f (x:xs)
    | f x            = (x:ys, zs)
    | otherwise      = (ys, x:zs)
    where
      (ys, zs)       = partition f xs
  \end{code}
  
  We would like to specify that the *sum* of the output tuple's
  dimensions equal the input list's dimension. Lets write measures
  to access the elements of the output:
  
  ~~~~~{.spec}
  {-@ measure fst @-}
  fst  (x, _) = x
  
  {-@ measure snd @-}
  snd (_, y) = y
  ~~~~~
  
  \noindent We can now refine the type of `partition` as:
  
  \begin{code}
  {-@ partition :: _ -> xs:_ -> {v:_ | Sum2 v (size xs)} @-}
  \end{code}
  
  \noindent where `Sum2 V N` holds for a pair of lists dimensions add to `N`:
  
  \begin{code}
  {-@ predicate Sum2 X N = size (fst X) + size (snd X) = N @-}
  \end{code}
  
  <div class="hwex" id="QuickSort">
  Use `partition` to implement `quickSort`.
  </div>
  
  \begin{code}
  -- >> quickSort [1,4,3,2]
  -- [1,2,3,4]
  
  {-@ quickSort    :: (Ord a) => xs:List a -> ListX a xs @-}
  quickSort []     = []
  quickSort (x:xs) = undefined
  
  {-@ test10 :: ListN String 2 @-}
  test10 = quickSort (drop 1 ["cat", "dog", "mouse"])
  \end{code}
  
  
  Dimension Safe Vector API
  -------------------------
  
  We can use the dimension aware lists to create a safe vector API.
  
  \newthought{Legal Vectors} are those whose `vDim` field actually
   equals the size of the underlying list:
  
  \begin{code}
  {-@ data Vector a = V { vDim  :: Nat
                        , vElts :: ListN a vDim }         
    @-}
  \end{code}
  
  When `vDim` is used a selector function, it returns the `vDim` field of `x`.
  
  \begin{code}
  {-@ vDim :: x:_ -> {v: Nat | v = vDim x} @-}
  \end{code}
  
  \noindent
  The refined data type prevents the creation of illegal vectors:
  
  \begin{code}
  okVec  = V 2 [10, 20]       -- accepted by LH
  
  badVec = V 2 [10, 20, 30]   -- rejected by LH
  \end{code}
  
  \noindent
  As usual, it will be handy to have a few aliases.
  
  \begin{code}
  -- | Non Empty Vectors
  {-@ type VectorNE a  = {v:Vector a | vDim v > 0} @-}
  
  -- | Vectors of size N
  {-@ type VectorN a N = {v:Vector a | vDim v = N} @-}
  
  -- | Vectors of Size Equal to Another Vector X
  {-@ type VectorX a X = VectorN a {vDim X}        @-}
  \end{code}
  
  \newthought{To Create} a `Vector` safely, we can
  start with the empty vector `vEmp` and then add
  elements one-by-one with `vCons`:
  
  \begin{code}
  {-@ vEmp :: VectorN a 0 @-}
  vEmp = V 0 []
  
  {-@ vCons :: a -> x:Vector a -> VectorN a {vDim x + 1} @-}
  vCons x (V n xs) = V (n+1) (x:xs)
  \end{code}
  
  \newthought{To Access} vectors at a low-level, we can use
  equivalents of *head* and *tail*, which only work on
  non-empty `Vector`s:
  
  \begin{code}
  {-@ vHd :: VectorNE a -> a @-}
  vHd (V _ (x:_))  = x
  vHd _            = die "nope"
  
  {-@ vTl          :: x:VectorNE a -> VectorN a {vDim x - 1} @-}
  vTl (V n (_:xs)) = V (n-1) xs
  vTl _            = die "nope"
  \end{code}
  
  \newthought{To Iterate} over a vector we can use the `for` combinator:
  
  \begin{code}
  {-@ for        :: x:Vector a -> (a -> b) -> VectorX b x @-}
  for (V n xs) f = V n (map f xs)
  \end{code}
  
  
  
  \newthought{Binary Pointwise Operations} should only be applied
  to *compatible* vectors, i.e. vectors with equal dimensions.
  We can write a generic binary pointwise operator:
  
  \begin{code}
  {-@ vBin :: (a -> b -> c) -> x:Vector a
                            -> VectorX b x
                            -> VectorX c x
    @-}
  vBin op (V n xs) (V _ ys) = V n (zipWith op xs ys)
  \end{code}
  
  \newthought{The Dot Product} of two `Vector`s can be now implemented
  in a wholemeal *and* dimension safe manner, as:
  
  \begin{code}
  {-@ dotProduct :: (Num a) => x:Vector a -> VectorX a x -> a @-}
  dotProduct x y = sum $ vElts $ vBin (*) x y
  \end{code}
  
  <div class="hwex" id="Vector Constructor">
  Complete the *specification* and *implementation* of `vecFromList`
  which *creates* a `Vector` from a plain list.
  </div>
  
  \begin{code}
  vecFromList     :: [a] -> Vector a
  vecFromList xs  =  undefined
  
  test6  = dotProduct vx vy    -- should be accepted by LH
    where
      vx = vecFromList [1,2,3]
      vy = vecFromList [4,5,6]
  \end{code}
  
  <div class="hwex" id="Flatten">
  \singlestar Write a function to `flatten` a nested `Vector`.
  </div>
  
  \begin{code}
  {-@ flatten :: n:Nat
              -> m:Nat
              -> VectorN (VectorN a m) n
              -> VectorN a {m * n}
    @-}
  flatten = undefined
  \end{code}
  
  \newthought{The Cross Product} of two vectors can now be
  computed in a nice wholemeal style, by a nested iteration
  followed by a `flatten`.
  
  \begin{code}
  {-@ product   :: xs:Vector _
                -> ys:Vector _
                -> VectorN _ {vDim xs * vDim ys}
    @-}
  product xs ys = flatten (vDim ys) (vDim xs) xys
    where
      xys       = for ys $ \y ->
                    for xs $ \x ->
                      x * y
  \end{code}
  
  
  Dimension Safe Matrix API
  -------------------------
  
  The same methods let us create a dimension safe Matrix API which
  ensures that only legal matrices are created and that operations
  are performed on compatible matrices.
  
  \newthought{Legal Matrices} are those where the dimension of the
  outer vector equals the number of rows `mRow` and the dimension
  of each inner vector is `mCol`. We can specify legality in a
  refined data definition:
  
  \begin{code}
  {-@ data Matrix a =
        M { mRow  :: Pos
          , mCol  :: Pos
          , mElts :: VectorN (VectorN a mCol) mRow
          }
    @-}
  \end{code}
  
  \noindent Notice that we avoid disallow degenerate matrices by
  requiring the dimensions to be positive.
  
  \begin{code}
  {-@ type Pos = {v:Int | 0 < v} @-}
  \end{code}
  
  \noindent It is convenient to have an alias for matrices of a given size:
  
  \begin{code}
  {-@ type MatrixN a R C   = {v:Matrix a | Dims v R C } @-}
  {-@ predicate Dims M R C = mRow M = R && mCol M = C   @-}
  \end{code}
  
  \noindent For example, we can use the above to write type:
  
  \begin{code}
  {-@ ok23 :: MatrixN _ 2 3 @-}
  ok23     = M 2 3 (V 2 [ V 3 [1, 2, 3]
                        , V 3 [4, 5, 6] ])
  \end{code}
  
  <div class="hwex" id="Legal Matrix">
  Modify the definitions of `bad1` and `bad2`
  so that they are legal matrices accepted by
  LiquidHaskell.
  </div>
  
  \begin{code}
  bad1 :: Matrix Int
  bad1 = M 2 3 (V 2 [ V 3 [1, 2   ]
                    , V 3 [4, 5, 6]])
  
  bad2 :: Matrix Int
  bad2 = M 2 3 (V 2 [ V 2 [1, 2]
                    , V 2 [4, 5] ])
  \end{code}
  
  <div class="hwex" id="Matrix Constructor">
  \singlestar Write a function to construct
  a `Matrix` from a nested list.
  </div>
  
  \begin{code}
  matFromList      :: [[a]] -> Maybe (Matrix a)
  matFromList []   = Nothing
  matFromList xss@(xs:_)
    | ok           = Just (M r c vs)
    | otherwise    = Nothing
    where
      r            = size xss
      c            = size xs
      ok           = undefined
      vs           = undefined
  \end{code}
  
  <div class="hwex" id="Refined Matrix Constructor">
  \doublestar Refine the specification for `matFromList`
  so that the following is accepted by LiquidHaskell.
  </div>
  
  \begin{code}
  {-@ mat23 :: Maybe (MatrixN Integer 2 2) @-}
  mat23     = matFromList [ [1, 2]
                          , [3, 4] ]
  \end{code}
  
  \hint It is easy to specify the number of rows from `xss`.
  How will you figure out the number of columns? A measure
  may be useful.
  
  \newthought{Matrix Multiplication} Finally, let's implement matrix
  multiplication. You'd think we did it already, but in fact the
  implementation at the top of this chapter is all wrong (run it and
  see!) We cannot just multiply any two matrices: the number of
  *columns* of the first must equal to the *rows* of the second -- after
  which point the result comprises the `dotProduct` of the rows of the
  first matrix with the columns of the second.
  
  \begin{code}
  {-@ matProduct :: (Num a) => x:Matrix a
                            -> y:{Matrix a  | mCol x = mRow y}
                            -> MatrixN a (mRow x) (mCol y)
    @-}
  matProduct (M rx _ xs) my@(M _ cy _)
                   = M rx cy elts
    where
      elts         = for xs (\xi ->
                       for ys' (\yj ->
                         dotProduct xi yj
                       )
                     )
      M _ _ ys'    = transpose my
  \end{code}
  
  \noindent To iterate over the *columns* of the matrix
  `my` we just `transpose` it so the columns become rows.
  
  \begin{code}
  -- >>> ok32 == transpose ok23
  -- True
  ok32 = M 3 2 (V 3 [ V 2 [1, 4]
                    , V 2 [2, 5]
                    , V 2 [3, 6] ])
  \end{code}
  
  <div class="hwex" id="Matrix Transpose">
  \doublestar Use the `Vector` API to complete the implementation
  of `txgo`. For inspiration, you might look at the implementation
  of `Data.List.transpose` from the [prelude][URL-transpose].
  Better still, don't.
  </div>
  
  \begin{code}
  {-@ transpose :: m:Matrix a -> MatrixN a (mCol m) (mRow m) @-}
  transpose (M r c rows) = M c r $ txgo c r rows
  
  {-@ txgo      :: c:Nat -> r:Nat
                -> VectorN (VectorN a c) r
                -> VectorN (VectorN a r) c
    @-}
  txgo c r rows = undefined
  \end{code}
  
  \hint As shown by `ok23` and `ok32`, `transpose` works by
  stripping out the `head`s of the input rows, to create the
  corresponding output rows.
  
  
  Recap
  -----
  
  In this chapter, we saw how to use measures to describe
  numeric properties of structures like lists (`Vector`)
  and nested lists (`Matrix`).
  
  1. Measures are *structurally recursive* functions, with a single
     equation per data constructor,
  
  2. Measures can be used to create refined data definitions
     that prevent the creation of illegal values,
  
  3. Measures can then be used to enable safe wholemeal programming,
     via dimension-aware APIs that ensure that operators only apply to
     compatible values.
  
  We can use numeric measures to encode various other
  properties of data structures. We will see examples
  ranging from high-level [AVL trees](#case-study-avltree),
  to low-level safe [pointer arithmetic](#case-study-pointers).
  