Eric Easley wants to get code invariants out of programmers’ heads and into the type system. After trying a dependently typed language he felt it was slow going and decided to try a leaner approach in Haskell. He has invented a library called Phantheck to bring property based testing into the types themselves. This video shows how it works.

Summary

• Phantheck weaves together quickcheck properties and Haskell’s type system
• Motivating example
  • a function which finds the minimum integer in a list
  • we could make it fast if we could guarantee its input is pre-sorted
  • the sortedness is an invariant which is not captured in the type system
• How to add invariants?
  • could use comments but they are not enforced
  • a graph of assurance vs implementation cost
  • on the far side of the graph are dependent types
  • a quick example of dependent types
  • Phantheck offers good assurance with lower implementation cost than say Agda
• We annotate functions with quickcheck properties which express invariants
• Livecoding
  • the library uses a trick from the GHC DataKinds extension
  • using phantom types to more precisely match functions and inputs
  • we would like evidence that values match our blind assertions
  • hooking up QuickCheck to check the phantom type assertions
• In the status quo we have two techniques for code correctness: types and tests
  • we write these tests, we run them, and look at their output
  • but the output only exists in the mind of the programmer
  • we’re not able to feed that back into the machine
  • Phantheck closes the loop
• This currently a proof of concept library
  • Eric is interested in developing it further and happy to help you use it
• Want to write Haskell every day? Front Row Education is hiring.