9 ms·

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

by mkehrt 10y ago

kazinator 10y ago
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.
- pka 10y ago
  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.agda http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.a...
  - willtim 10y ago
    This is a great example. I also recall seeing refinement types (Liquid Haskell) used to prove termination of Euclids GCD.
  - kazinator 10y ago
    For all I know, the GCD function buried in that gobbledygook could actually be calculating the LCM, and the proof could be of that.
    - pka 10y ago
      For all I know Agreed.
- tome 10y ago
  > 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.
  - kazinator 10y ago
    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.
    - dllthomas 10y ago
      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.

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

by mkehrt 10y ago

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.

pka 10y ago
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.agda http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Nat/GCD.a...
- willtim 10y ago
  This is a great example. I also recall seeing refinement types (Liquid Haskell) used to prove termination of Euclids GCD.
- kazinator 10y ago
  For all I know, the GCD function buried in that gobbledygook could actually be calculating the LCM, and the proof could be of that.
  - pka 10y ago
    For all I know Agreed.
tome 10y ago
> 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.
- kazinator 10y ago
  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.
  - dllthomas 10y ago
    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.