Learning Elm has gotten me confused about static vs. dynamic typing

Re:Learning Elm has gotten me confused about static vs. dyna... by mkehrt on Tuesday June 14, 2016 @07:42PM (#11906269)

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

[ Parent | on HN ]

Re:Learning Elm has gotten me confused about static vs. dyna... by kazinator on Tuesday June 14, 2016 @08:03PM (#11906354)

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.

[ Parent | on HN ]

Re:Learning Elm has gotten me confused about static vs. dyna... by pka on Wednesday June 15, 2016 @12:16AM (#11907143)

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...

[ Parent | on HN ]

Re:Learning Elm has gotten me confused about static vs. dyna... by willtim on Wednesday June 15, 2016 @02:25AM (#11907493)

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

[ Parent | on HN ]

Re:Learning Elm has gotten me confused about static vs. dyna... by kazinator on Wednesday June 15, 2016 @02:10PM (#11910909)

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

[ Parent | on HN ]

Re:Learning Elm has gotten me confused about static vs. dyna... by pka on Thursday June 16, 2016 @11:55AM (#11916950)

For all I know

Agreed.

[ Parent | on HN ]

Re:Learning Elm has gotten me confused about static vs. dyna... by tome on Wednesday June 15, 2016 @03:23AM (#11907680)

> 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.

[ Parent | on HN ]

Re:Learning Elm has gotten me confused about static vs. dyna... by kazinator on Wednesday June 15, 2016 @03:39PM (#11911570)

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.

[ Parent | on HN ]

Re:Learning Elm has gotten me confused about static vs. dyna... by dllthomas on Wednesday June 15, 2016 @09:04PM (#11913308)

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.

[ Parent | on HN ]