Hacker News new | past | comments | ask | show | jobs | submit login

Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work?

I've played around with Coq a little and it certainly feels more like a proof assistant than a programming language. It was fairly confusing and unfamiliar, but interesting nonetheless. Something with slightly more traditional ergonomics might be easier to pick up.




> Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work?

The learning curve is almost vertical to be completely honest from personal experience. I find most tutorials are written by people with a strong background in logic, type systems and mathematics, so it's a struggle to rely only on your knowledge of mainstream programming languages as you're learning lots of new things at once (e.g. formal proofs, formal specifications, logic, pure functional programming).

It's a super interesting area if you can stick with it though so keep at it!


> most tutorials are written by people with a strong background in logic, type systems, and mathematics...

I'm a little used to this from Haskell, although I imagine the dependently-typed languages are even worse in that regard. Working through the Idris tutorial now and at least the syntax is familiar.


> I'm a little used to this from Haskell, although I imagine the dependently-typed languages are even worse in that regard. Working through the Idris tutorial now and at least the syntax is familiar.

That's what I mean by the difficultly jump. Like when you go from C++ to Java or the other way around, there's a lot of familiar things to cling on to while you make the transition. With dependently typed languages, there's a massive pile of unfamiliar stuff so the steep learning curve is unavoidable really. Someone needs to write a "dependently typed programming for Java programmers guide". :)


I found Idris pretty easy to get started with - that's part of it's goal, making dependent types easier to get started with. From there I think it would be easier to go to Agda or Coq, but I haven't explored much there myself.


+1 for Idris. The tutorials were pretty solid for it too when I tried it, and the mailing list was very helpful when I had questions [1]. There's even a WIP book! [2]

[1] https://groups.google.com/forum/#!forum/idris-lang

[2] https://www.manning.com/books/type-driven-development-with-i...


Their main docs are pretty good too: http://docs.idris-lang.org


Thanks. I've started with the tutorials but have yet to see an example that convinces me it's worth all the pain. I'll carry on a little further, though.

EDIT: the pain of such a strict language, not necessarily idris in particular.


I have very limited experience, but it's worth saying that Idris was designed by an experienced Haskell user with the intention of using it to write practical programs.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: