4 ms·

> 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 t

> 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!

titanomachy 10y ago
> 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.
- seanwilson 10y ago
  > 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". :)