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

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 ]