title: Differences between Agda and Idris
body: <p>I'm starting to dive into dependently-typed programming and have found that the Agda and Idris languages are the closest to Haskell, so I started there.</p>
  
  <p>My question is: which are the main differences between them? Are the type systems equally expresive in both of them? It would be great to have a comprehensive comparative and a discussion about benefits.</p>
  
  <p>I've been able to spot some:</p>
  
  <ul>
  <li>Idris has type classes à la Haskell, whereas Agda goes with instance arguments</li>
  <li>Idris includes monadic and applicative notation</li>
  <li>Both of them seem to have some sort of rebindable syntax, although not really sure if they are the same.</li>
  </ul>
  
  <hr>
  
  <p><em>Edit</em>: there are some more answers in the Reddit page of this question: <a href="http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/" rel="noreferrer">http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/</a></p>