Prop>. Int
-> Int
-> Int
@-} \end{code} Here, the definition says explicitly: *for any property* `p` that is a property of `Int`, the function takes two inputs each of which satisfy `p` and returns an output that satisfies `p`. That is to say, `Int
` is just an abbreviation for `{v:Int | (p v)}` **Digression: Whither Decidability?** At first glance, it may appear that these abstract `p` have taken us into the realm of higher-order logics, where we must leave decidable checking and our faithful SMT companion at that door, and instead roll up our sleeves for interactive proofs (not that there's anything wrong with that!) Fortunately, that's not the case. We simply encode abstract refinements `p` as *uninterpreted function symbols* in the refinement logic. \begin{code} Uninterpreted functions are special symbols `p` which satisfy only the *congruence axiom*. forall X, Y. if (X = Y) then p(X) = p(Y) \end{code} Happily, reasoning with such uninterpreted functions is quite decidable (thanks to Ackermann, yes, *that* Ackermann) and actually rather efficient. Thus, via SMT, LiquidHaskell happily verifies that `maxInt` indeed behaves as advertised: the input types ensure that both `(p x)` and `(p y)` hold and hence that the returned value in either branch of `maxInt` satisfies the refinement `{v:Int | p(v)}`, thereby ensuring the output type. By the same reasoning, we can define the `maximumInt` operator on lists: \begin{code} {-@ maximumInt :: forall
Prop>. x:[Int
] -> Int
@-} maximumInt (x:xs) = foldr maxInt x xs \end{code} Using Parametric Invariants --------------------------- Its only useful to parametrize over invariants if there is some easy way to *instantiate* the parameters. Concretely, consider the function: \begin{code} {-@ maxEvens1 :: xs:[Int] -> {v:Int | (Even v)} @-} maxEvens1 xs = maximumInt xs'' where xs' = [ x | x <- xs, isEven x] xs'' = 0 : xs' \end{code} \begin{code} where the function `isEven` is from the Language.Haskell.Liquid.Prelude library: {- isEven :: x:Int -> {v:Bool | (Prop(v) <=> (Even x))} -} isEven :: Int -> Bool isEven x = x `mod` 2 == 0 \end{code} where the predicate `Even` is defined as \begin{code} {-@ predicate Even X = ((X mod 2) = 0) @-} \end{code} To verify that `maxEvens1` returns an even number, LiquidHaskell 1. infers that the list `(0:xs')` has type `[{v:Int | (Even v)}]`, that is, is a list of even numbers. 2. automatically instantiates the *refinement* parameter of `maximumInt` with the concrete refinement `{\v -> (Even v)}` and so 3. concludes that the value returned by `maxEvens1` is indeed `Even`. Parametric Invariants and Type Classes -------------------------------------- Ok, lets be honest, the above is clearly quite contrived. After all, wouldn't you write a *polymorphic* `max` function? And having done so, we'd just get all the above goodness from old fashioned parametricity. \begin{code} That is to say, if we just wrote: max :: forall a. a -> a -> a max x y = if x > y then x else y maximum :: forall a. [a] -> a maximum (x:xs) = foldr max x xs \end{code} then we could happily *instantiate* the `a` with `{v:Int | v > 0}` or `{v:Int | (Even v)}` or whatever was needed at the call-site of `max`. Sigh. Perhaps we are still pining for Hindley-Milner. \begin{code} Well, if this was an ML perhaps we could but in Haskell, the types would be (>) :: (Ord a) => a -> a -> Bool max :: (Ord a) => a -> a -> a maximum :: (Ord a) => [a] -> a \end{code} Our first temptation may be to furtively look over our shoulders, and convinced no one was watching, just pretend that funny `(Ord a)` business was not there, and quietly just treat `maximum` as `[a] -> a` and summon parametricity. That would be most unwise. We may get away with it with the harmless `Ord` but what of, say, `Num`. \begin{code} Clearly a function numCrunch :: (Num a) => [a] -> a \end{code} is not going to necessarily return one of its inputs as an output. Thus, it is laughable to believe that `numCrunch` would, if given a list of of even (or positive, negative, prime, RGB, ...) integers, return a even (or positive, negative, prime, RGB, ...) integer, since the function might add or subtract or multiply or do other unspeakable things to the numbers in order to produce the output value. And yet, typeclasses are everywhere. How could we possibly verify that \begin{code} {-@ maxEvens2 :: xs:[Int] -> {v:Int | (Even v) } @-} maxEvens2 xs = maximumPoly xs'' where xs' = [ x | x <- xs, isEven x] xs'' = 0 : xs' \end{code} where the helpers were in the usual `Ord` style? \begin{code} maximumPoly :: (Ord a) => [a] -> a maximumPoly (x:xs) = foldr maxPoly x xs maxPoly :: (Ord a) => a -> a -> a maxPoly x y = if x <= y then y else x \end{code} The answer: abstract refinements. First, via the same analysis as the monomorphic `Int` case, LiquidHaskell establishes that \begin{code} {-@ maxPoly :: forall
Prop>. (Ord a) => x:a
-> y:a
-> a
@-} \end{code} and hence, that \begin{code} {-@ maximumPoly :: forall
Prop>. (Ord a) => x:[a
] -> a
@-} \end{code} Second, at the call-site for `maximumPoly` in `maxEvens2` LiquidHaskell instantiates the type variable `a` with `Int`, and the abstract refinement parameter `p` with `{\v -> (Even v)}` after which, the verification proceeds as described earlier (for the `Int` case). And So ------ If you've courageously slogged through to this point then you've learnt that 1. Sometimes, choosing the right type can be quite difficult! 2. But fortunately, with *abstract refinements* we needn't choose, but can write types that are parameterized over the actual concrete invariants or refinements, which 3. Can be instantiated at the call-sites i.e. users of the functions. We started with some really frivolous examples, but buckle your seatbelt and hold on tight, because we're going to see some rather nifty things that this new technique makes possible, including induction, reasoning about memoizing functions, and *ordering* and *sorting* data. Stay tuned. [blog-dbz]: /blog/2013/01/01/refinement-types-101.lhs/ [blog-len]: /blog/2013/01/31/safely-catching-a-list-by-its-tail.lhs/ [blog-vec]: /blog/2013/03/04/bounding-vectors.lhs/ [blog-set]: /blog/2013/03/26/talking/about/sets.lhs/ [blog-zip]: /blog/2013/05/16/unique-zipper.lhs/