There is an interactive tutorial at [1].

I find this quite amazing. With refinement types one can say/prove things like:

- This function only returns even numbers.

- The input for this function is not just any vector, it must be an ordered vector.

- It's possible to make compile time unit tests. Where we write a function that exercises the code, and returns True if the test succeeds. Then one adds a refinement type saying that the function must always evaluate to true. The theorem prover does the rest.

[1] - http://ucsd-progsys.github.io/liquidhaskell-tutorial/02-logi...