News for hackers. Stuff that matters.

A comment on Why functional programming matters (1990) [pdf]. Parent comment

Re:Why functional programming matters (1990) [pdf] by lmm on Thursday May 07, 2015 @11:33AM (#9505790)
If "prover" just means "has dependent types" then that's a much larger class than it sounds like. I write a lot of Scala, which has dependent types, but most of the code I write is just ordinary web services.
[ Parent | on HN ]
Re:Why functional programming matters (1990) [pdf] by mafribe on Friday May 08, 2015 @01:44AM (#9510158)
I meant dependent types a la Agda, Coq etc that you can use for proving essentially arbitrary properties. Scala and Haskell do not have this.
[ Parent | on HN ]
Re:Why functional programming matters (1990) [pdf] by lmm on Friday May 08, 2015 @01:38PM (#9513040)
I don't understand the distinction you're drawing. Idris' type level functions are easier to write than Scala's but they don't seem to be able to do anything that Scala ones can't.
[ Parent | on HN ]