Eliminating Bugs with Dependently Typed Haskell
Please log in to watch this conference skillscast.
Using dependent types in production Haskell code is a practical way to eliminate errors. While there are many examples of using dependent Haskell to prove invariants about code, few of these are applied to large scale production systems. Critics claim that dependent types are only useful in toy examples and that they are impractical for use in the real world. This talk analyzes real world examples where dependent types have enabled us to find and eliminate bugs in production Haskell code.
Q&A
Question: How did you find the ergonomics of using Dependent Typing in Haskell? eg compile times, error messages
Answer: I haven't done any scientific measurements, but anecdotally speaking compile times were not a problem. For error messages, it depends a lot on what you're doing. For basic usages of GADTs, you'll get a friendly "expected X, but got Y". If you start using a lot of type families and existential types, then you can run into some crazy stuff. There's one error that says "my brain just exploded", that one isn't so friendly
Question: Is the Thrift IDL Haskell implementation available as open source?
Answer: Yep! We open sourced it earlier this year! https://github.com/facebookincubator/hsthrift
Question: looking at hsthrift, it looks like the
Util.* modules reimplement half of the Haskell ecosystem!
Answer: It's sort of meta. Those utility functions are for generating Haskell ASTs
Question: God, I love this sort of type level programming so much. It feels tedious and complex in small projects, but scales really well in my experience
Answer: Thanks! I agree, I think it does scale well and in fact it helps the entire project scale by adding more structure. One thing I didn't mention is that any sort of refactoring in these projects was super easy because the compiler would tell us everything that needed to be updated
If you like this stuff, you can see an example where I went totally overboard and tried to encode the runtime complexity of sorting algorithms in Haskell's type system. It worked ok for insertion sort, but the GHC constraint solver didn't like dealing with log very much
https://github.com/zilberstein/verified-complexity/blob/master/Algorithm/Sorting.hs
Question: Do you have any further suggestions on where the line crosses to "my brain just exploded"? And any evidence of how that has changed over time with newer releases of GHC?
Answer: "My brain just exploded" happens when existentially quantified type variables escape their defining scope. It can happen pretty easily when using GADTs because you often want to use an existential type to normalize the type of a GADT. It sometimes is easy to fix by adding a type signature to the output. Usually if you can't fix it easily, then you really are doing something unsafe. Still, the error message isn't that helpful in finding and fixing the bug.
YOU MAY ALSO LIKE:
Thank you to our sponsors and partners
Platinum
Silver
Bronze
Eliminating Bugs with Dependently Typed Haskell
Noam Zilberstein
Software EngineerFacebook