4 ms·

I've also bought and worked through the book. It's excellent. My conclusion was that Idris is an academic language (lack of libraries), followed by realizing t

I've also bought and worked through the book. It's excellent. My conclusion was that Idris is an academic language (lack of libraries), followed by realizing that the parts of Idris that I like, are almost all covered by Haskell extensions. For me, Idris is a great peek into what Haskell should/could be, if extensions were better documented and the synergy between them, explained to mere mortals.

pjmlp 8y ago
For me it was also very interesting read, and I also reached a similar conclusion. Such language features are still too complex for the regular kind of software development many of us do, as the whole team has to fully grasp it.
moosefish 8y ago
Any thoughts on Agda? I've always thought that since it's embedded in Haskell, even though it's less 'practical' than Idris it would benefit from the extensive libraries that Haskell brings to the table.
- Zalastax 8y ago
  Usually, Agda programs would not use Haskell libraries very much, even though they could. The reason seems to be that it is an unstable language and we are still figuring out how to do dependent types correctly. To me, working in Agda is like working in a very powerful version of Haskell, but for most people it's more about working in a research language. Idris and Agda are quite similar: don't build a company on them, but expect really cool ideas to spawn from them. Dependent types is really an awesome idea.
fiddlerwoaroof 8y ago
I’ve often thought Idris would be useful for expressing the core business logic of your program, and the you’d use the Haskell or JS backend to do the user-facing parts.
KirinDave 8y ago
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.
- matt-noonan 8y ago
  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.

pjmlp 8y ago

For me it was also very interesting read, and I also reached a similar conclusion. Such language features are still too complex for the regular kind of software development many of us do, as the whole team has to fully grasp it.

moosefish 8y ago

Any thoughts on Agda? I've always thought that since it's embedded in Haskell, even though it's less 'practical' than Idris it would benefit from the extensive libraries that Haskell brings to the table.

Zalastax 8y ago
Usually, Agda programs would not use Haskell libraries very much, even though they could. The reason seems to be that it is an unstable language and we are still figuring out how to do dependent types correctly. To me, working in Agda is like working in a very powerful version of Haskell, but for most people it's more about working in a research language. Idris and Agda are quite similar: don't build a company on them, but expect really cool ideas to spawn from them. Dependent types is really an awesome idea.

fiddlerwoaroof 8y ago

I’ve often thought Idris would be useful for expressing the core business logic of your program, and the you’d use the Haskell or JS backend to do the user-facing parts.

KirinDave 8y ago

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.

matt-noonan 8y ago
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.