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

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.

[ 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 ]