News for hackers. Stuff that matters.

A comment on Notes on Idris (2017). Parent comment

Re:Notes on Idris (2017) by KirinDave on Thursday June 07, 2018 @04:33PM (#17259998)
I've got a few network services working with Idris and they run okay. The compilation time grows so quickly you can't use it for very large projects though.

Honestly, Haskell dependent-typing is SO MUCH MORE COMPLEX than Idris's "well what if I just write a function that takes a type?" approach, it's not even funny. Even the author of singleton says it's a rough landscape.

Haskell's going to get much closer with QuantifiedConstraints in ghc 8.6, in that it'll simplify a lot of this work, but it's still years out from the simplicity and library unification.

[ Parent | on HN ]
Re:Notes on Idris (2017) by matt-noonan on Thursday June 07, 2018 @06:29PM (#17260913)
Can you elaborate on the DT / QuantifiedConstraints connection a bit? I haven't thought enough yet about QuantifiedConstraints to see the everyday benefits, but I'm getting contact-excited by everybody else's anticipation of it. I'd love to get some concrete benefits to hold in mind.
[ Parent | on HN ]