q >a ->
(x:a -> ST r >b) ->
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 ->
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 ```