Hacker News Reader

Comment by mkehrt | Hacker News Reader

Luckily, my compiler writes large piles of tests for me. I call it the typechecker.

These tests only cover the type space, which is trivial. And doesn't vary at run time. Even under dynamic typing, it's by large immutable: short of special tricks like change-class in Common Lisp, objects are immutable, and most data flow paths carry the same types all the time.

For instance, consider a function which calculates the GCD of two integers. Everything in that function is an integer. Your compiler tests it for you: nope, no strings or floats in there: nothing but integers, check!

It's basically one test, and it has nothing to do with whether that function calculates the GCD correctly. It will pass even if that function calculates the LCM due to misunderstood requirements.

There [0]: the GCD m n d type proves that the greatest common divisor of m and n is d.

[0] http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.a...

This is a great example. I also recall seeing refinement types (Liquid Haskell) used to prove termination of Euclids GCD.

For all I know, the GCD function buried in that gobbledygook could actually be calculating the LCM, and the proof could be of that.

For all I know

Agreed.

> These tests only cover the type space, which is trivial.

Granted it's not enormous, but if you think it's trivial you'll probably be surprised by the range of things you can encode in the Haskell type system.

That encoding requires you to be a type system expert, and write reams of additional code surrounding the actual code. That additional code has to be well thought out and designed; proofs don't just pop out of thin air, all ready to go and represented as type via Curry-Howard!

Ordinary code does not encode very interesting things about itself via its typing. Well typed usually just means "there is no trivial mistake here", on about the same level as a missing semicolon in a C struct declaration.

That's just not true.

I have some interest in types (mostly practical, some theoretical) but I have no graduate degree, I still regularly encounter both theory and type voodoo I don't understand, and I wouldn't consider myself a "type system expert".

On a recent project I was able to use the type checker to help me catch things including 1) passing a bid price where I meant an ask price, 2) using an index into the wrong array, 3) calling a function not permitted to run on the thread in question (because of data access or deliberate marking).

This wasn't Haskell - it was C.

Reply on news.ycombinator.com