Различия между Agda и Idris

Я начинаю погружаться в программирование с зависимой типизацией и обнаружил, что языки Agda и Idris наиболее близки к Haskell, поэтому я начал с них.

У меня вопрос: каковы основные различия между ними? Являются ли системы типов одинаково выразительными в них обоих? Было бы здорово провести подробное сравнение и обсудить преимущества.

Мне удалось обнаружить некоторые из них:

• Идрис имеет классы типов а-ля Haskell, тогда как Agda использует аргументы экземпляра
• Идрис включает монадическую и аппликативную нотации
• Оба они, похоже, имеют своего рода синтаксис с возможностью повторной привязки, хотя не совсем уверен, одинаковы ли они.

Изменить : на странице Reddit есть еще несколько ответов на этот вопрос: http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/