submited by

Style Pass

With refinement types, we can annotate a base-type (like Int or Bool) with a logical predicate that restricts the possible values inhabitants of the type may take. For example, in Liquid Haskell we can define the following type for non-zero integers.

We can then use this type to constrain the input and output types of functions. For example, we can specify div as a function that takes a non-zero integer, and returns its first input x divided by its second one, y.

The type system then proves at compile-time, that whenever we call div (at runtime), its second argument must indeed be non-zero. This rules out division by zero errors. Great!

What makes refinement types so powerful is their modularity. To check if a program respects all the restrictions imposed by the types – and their refinements – the checker only needs to look at “what’s written on the tin”. That is, the type-checker only works with what we explicitly know from the types, and doesn’t need to perform any additional costly analysis, say, by enumerating program traces.

It’s exactly this modularity that allows refinement types to scale to more advanced features like higher-order functions, datatypes and polymorphism. For example, if we define the type Nat to represent the natural numbers

Read more vusecpl.gith...