q >a ->
(x:a -> ST r >b
bind = undefined
pure :: rforall a, p. x:a -> ST p >a
pure = undefined
thenn :: rforall a, b, p, q, r.
ST q >a ->
ST r >b
thenn = \f g -> bind f (\underscore -> g)
fmap :: rforall a, b, p, q.
(underscore:a -> b) ->
ST q >a ->
ST q >b
fmap = \f x -> bind x (\xx -> pure (f xx))
```
> If a function type signature is failing to parse, try assigning a name to the
argument (e.g. `x:Int ->` instead of `Int ->`).
## Implicit pair types
Next, we demonstrate how to use another core feature unique to Mist: implicit
pair types as described in the paper. In the paper the syntax is
$[n:Int].\text{---}$, but in the implementation, we use `exists n. -`. Consider
iterating through an infinite stream of token handlers. The API for getting the
next token is:
```{include=tests/pos/paginationTokens.hs .haskell .numberLines startLine=37 endLine=42}
nextPage as
token:{v: Int | v ≠ done} ->
(exists tok:Int.
(ST <{v:Int | v = token}
>{v:Int | (v = tok) /\ (v ≠ token)}
>{v:Int | v = tok}))
```
> Remember to parenthesize both sides of conjunctions (`/\`)!
That is, given a token, `nextPage` give you a state action where it picks a new
token that's not equal to the old token, and updates the state of the world to
reflect the new token.
```{include=tests/pos/paginationTokens.hs .haskell .numberLines startLine=52 endLine=57}
client :: token:Int ->
(ST <{v:Int | v = token} >{v:Int | v = done} >Int)
client = \token ->
if token == done
then pure 1
else bind (nextPage token) (\tok -> client tok)
```
$ mist tests/pos/paginationTokens.hs
SAFE
And that concludes our short tutorial on `mist`. Go forth and verify!
\appendix
# Appendix : Measures
But these `List` constructors are all a bit boring --- what good are user
datatypes if we can't say anything about them at the type level?!
Until now, we've only been able to form refinements out of variables and
primitive functions such as `+` and `∩` on special types such as `Int` and `Set`.
We use (purely) refinement-level functions called measures (Vazou et al, ICFP 2014)
to extend the language of refinements and enrich the types of our constructors.
```{include=tests/pos/recursion.hs .haskell .numberLines startLine=1 endLine=1}
measure mNil :: List [>Int] -> Bool
```
> Measures use a different syntax for types --- type applications have a list
of parameters in `[`square`,` brackets`,` separated`,` by`,` commas`]`, unlike
applications of type constructors that produce refinement types, which use the
usual space-separated syntax.
This declares a measure `mNil` that takes a `List` of `Int`s and returns a `Bool`.
Measure have unrefined types.
> If you get an error message about free vars that implicates the start of the
file, you probably tried to use a measure you didn't declare. This will cause
the solver print a list of unbound measures and crash with some mumbo-jumbo
about `--prune-unsorted`. Measures always go at the top of the file.
We can use these measures in constructor axioms to effectively define
structurally recursive functions over a datatype.
```{include=tests/pos/recursion.hs .haskell .numberLines startLine=10 endLine=10}
nil as {v: List >Int | (mNil v) /\ (mLength v = 0) /\ (not (mCons v))}
```
```{include=tests/pos/recursion.hs .haskell .numberLines startLine=13 endLine=14}
cons as x:Int -> xs:(List >Int) -> {v: List >Int | (mCons v) /\ (mLength v = mLength xs + 1) /\ (not (mNil v))}
```
```{include=tests/pos/recursion.hs .haskell .numberLines startLine=17 endLine=17}
first as {v: List >Int | mCons v} -> Int
```
```{include=tests/pos/recursion.hs .haskell .numberLines startLine=20 endLine=22}
rest as rs:{v: List >Int | mCons v} -> {v: List >Int | mLength v + 1 == mLength rs }
```
and we can then use them in verification!
```{include=tests/pos/recursion.hs .haskell .numberLines startLine=24 endLine=100}
append :: xs:(List >Int) -> ys:(List >Int) -> {v: List >Int | mLength v = (mLength xs) + (mLength ys)}
append = \xs -> \ys ->
if empty xs
then ys
else cons (first xs) (append (rest xs) ys)
```
```{.console}
$ mist tests/pos/recursion.hs
SAFE
```
r >b) ->
ST
r >b ->
ST