<commit_before>Numeric Measures {#numericmeasure}
================

\begin{comment}
\begin{code}
{-@ LIQUID "--short-names"    @-}
{-@ LIQUID "--no-termination" @-}

module NumericMeasures 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

{-@ invariant {v:[a] | 0 <= size v} @-}
\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 [<NAME>][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, lets
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    :: xs:[a] -> {v:Nat | v = size xs} @-}
size []     = 0
size (_:rs) = 1 + size rs
\end{code}

\newthought{Measures Refine Constructors}
As with [refined data definitions](#autosmart), the<commit_msg>Fix #40<commit_after>Numeric Measures {#numericmeasure}
================

\begin{comment}
\begin{code}
{-@ LIQUID "--short-names"    @-}
{-@ LIQUID "--no-termination" @-}

module NumericMeasures 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

{-@ invariant {v:[a] | 0 <= size v} @-}
\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 [<NAME>][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, lets
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 []     = 0
size (_:rs) = 1 + size rs
\end{code}

\newthought{Measures Refine Constructors}
As with [refined data definitions](#autosmart), the
{'fraction_non_alphanumeric': 0.10915601023017903, 'fraction_numerical': 0.001227621483375959, 'mean_word_length': 2.9419354838709677, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 54, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1840473', 'n_tokens_mistral': 3000, 'n_tokens_neox': 2818, 'n_words': 1330}