begriffs

Phantheck, the Type-Level QuickCheck

December 6, 2015

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.