Tutorial_01_Introduction.lhs

Introduction {#intro}
============

\begin{comment}
\begin{code}
{-# LANGUAGE CPP #-}

module Tutorial_01_Introduction where
main = putStrLn "Intro"

-- {-@ ignore average @-}

\end{code}
\end{comment}

One of the great things about Haskell is its brainy type system that
allows one to enforce a variety of invariants at compile time, thereby
nipping in the bud a large swathe of run-time [errors](#getting-started).

Well-Typed Programs Do Go Wrong {#gowrong}
------------------------------------------

Alas, well-typed programs *do* go quite wrong, in a variety of ways.

\newthought{Division by Zero} This innocuous function computes the average
of a list of integers:

\begin{code}
average    :: [Int] -> Int
average xs = sum xs `div` length xs
\end{code}

We get the desired result on a non-empty list of numbers:

~~~~~{.ghci}
ghci> average [10, 20, 30, 40]
25
~~~~~

However, if we call it with an empty list, we get a rather unpleasant crash:
^[We could write `average` more *defensively*, returning
a `Maybe` or `Either` value. However, this merely kicks
the can down the road. Ultimately, we will want to extract
the `Int` from the `Maybe` and if the inputs were invalid
to start with, then at that point we'd be stuck.]

~~~~~{.ghci}
ghci> average []
*** Exception: divide by zero
~~~~~

\newthought{Missing Keys}
Associative key-value maps are the new lists; they come "built-in"
with modern languages like Go, Python, JavaScript and Lua; and of
course, they're widely used in Haskell too.

~~~~~{.ghci}
ghci> :m +Data.Map 
ghci> let m = fromList [ ("haskell", "lazy")
                       , ("ocaml"  , "eager")]

ghci> m ! "haskell"
"lazy"
~~~~~

Alas, maps are another source of vexing errors that are tickled
when we try to find the value of an absent key: ^[Again, one could
use a `Maybe` but it's just deferring the inevitable.]

~~~~~{.ghci}
ghci> m ! "javascript"
"*** Exception: key is not in the map
~~~~~


\newthought{Segmentation Faults}
Say what? How can one possibly get a segmentation fault with a *safe*
language like Haskell. Well, here's the thing: every safe language is
built on a foundation of machine code, or at the very least, `C`.
Consider the ubiquitous `vector` library:

~~~~~{.ghci}
ghci> :m +Data.Vector
ghci> let v = fromList ["haskell", "ocaml"]
ghci> unsafeIndex v 0
"haskell"
~~~~~

However, invalid inputs at the safe upper
levels can percolate all the way down and
stir a mutiny down below:
^[Why use a function marked `unsafe`?
Because it's very fast! Furthermore, even if we used
the safe variant, we'd get a *run-time* exception
which is only marginally better. Finally, we should remember
to thank the developers for carefully marking it unsafe,
because in general, given the many layers of abstraction,
it is hard to know which functions are indeed safe.]


~~~~~{.ghci}
ghci> unsafeIndex v 3
'ghci' terminated by signal SIGSEGV ...
~~~~~


\newthought{Heart Bleeds}
Finally, for certain kinds of programs, there is a fate worse than death.
`text` is a high-performance string processing library for Haskell, that
is used, for example, to build web services.

~~~~~{.ghci}
ghci> :m +Data.Text Data.Text.Unsafe
ghci> let t = pack "Voltage"
ghci> takeWord16 5 t
"Volta"
~~~~~

A cunning adversary can use invalid, or rather,
*well-crafted*, inputs that go well outside the size of
the given `text` to read extra bytes and thus *extract secrets*
without anyone being any the wiser.

~~~~~{.ghci}
ghci> takeWord16 20 t
"Voltage\1912\3148\SOH\NUL\15928\2486\SOH\NUL"
~~~~~

The above call returns the bytes residing in memory
*immediately after* the string `Voltage`. These bytes
could be junk, or could be either the name of your
favorite TV show, or, more worryingly, your bank
account password.

Refinement Types
----------------

Refinement types allow us to enrich Haskell's type system with
*predicates* that precisely describe the sets of *valid* inputs
and outputs of functions, values held inside containers, and
so on. These predicates are drawn from special *logics* for which
there are fast *decision procedures* called SMT solvers.

\newthought{By combining types with predicates} you can specify *contracts*
which describe valid inputs and outputs of functions. The refinement
type system *guarantees at compile-time* that functions adhere to
their contracts. That is, you can rest assured that
the above calamities *cannot occur at run-time*.

\newthought{LiquidHaskell} is a Refinement Type Checker for Haskell, and in
this tutorial we'll describe how you can use it to make programs
better and programming even more fun. ^[If you are familiar with
the notion of Dependent Types, for example, as in the Coq proof
assistant, then Refinement Types can be thought of as restricted
class of the former where the logic is restricted, at the cost of
expressiveness, but with the reward of a considerable amount of
automation.]


Audience
--------

Do you

* know a bit of basic arithmetic and logic?
* know the difference between a `nand` and an `xor`?
* know any typed languages e.g. ML, Haskell, Scala, F# or (Typed) Racket?
* know what `forall a. a -> a` means?
* like it when your code editor politely points out infinite loops?
* like your programs to not have bugs?

Then this tutorial is for you!

Getting Started
---------------

As of July 2020, LiquidHaskell, version 0.8.10 onwards, is available
as a [GHC plugin](https://downloads.haskell.org/~ghc/8.10.1/docs/html/users_guide/extending_ghc.html).

This means, roughly, that you need simply 

1. Add LH to your project dependencies, after which 
2. GHC produces LH type errors whenever you compile the code, so that you can
3. View errors using your favorite editor's existing Haskell tooling.

\newthought{LiquidHaskell Requires} (in addition to the cabal
dependencies) a binary for an `SMTLIB2` compatible
solver, e.g. one of

+ [Z3][z3] (which we recommend)
+ [CVC4][cvc4]
+ [MathSat][mathsat]

\newthought{This Tutorial} is written in literate Haskell and
the code for it is available [here][liquid-tutorial].
Hence, we *strongly* recommend you grab the code, and follow
along, and especially that you do the exercises, via two steps.

**Step 1** Clone the code repository,

~~~~~{.sh}
git clone --recursive https://github.com/ucsd-progsys/liquidhaskell-tutorial.git
~~~~~

**Step 2:** Try building the code using

~~~~~{.sh}
cabal v2-build
~~~~~

or

~~~~~{.sh}
stack build --fast --file-watch
~~~~~

If your environment is set up correctly,
compilation will stop with a Liquid type error:

~~~~~{.spec}
src/Tutorial_01_Introduction.lhs:30:27: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v >= 0
                                && v == len xs}
    .
    is not a subtype of the required type
      VV : {VV : GHC.Types.Int | VV /= 0}
    .
    in the context
      xs : {v : [GHC.Types.Int] | len v >= 0}
   |
30 | average xs = sum xs `div` length xs
   |                           ^^^^^^^^^
~~~~~

**Step 3:** Iteratively edit-compile the code in `src/`
until it _builds_ without any liquid type errors.

The above workflow will let you use whatever GHC/Haskell tooling you use for your
favorite editor, to automatically display LH errors as well.

If you'd like to copy and paste code snippets into the
web demo, instead of cloning the repo, note that you may
need to pass `--no-termination` to `liquid`, or equivalently,
add the pragma `{-@ LIQUID "--no-termination" @-}` to the top
of the source file. (By default, `liquid` tries to ensure that
all code it examines will terminate. Some of the code in this
tutorial is written in such a way that termination is not
immediately obvious to LH.)

**Note:** This tutorial is a *work in progress*, and we will
be **very** grateful for feedback and suggestions, ideally
via pull-requests on github.

\noindent Lets begin!