Слон и кит

Забавная танцевальная битва Idris vs. Scala, где Miles Sabin пытается на Скале воспроизвести пару примеров использования зависимых типов, показанных перед этим на Идрисе:
http://www.infoq.com/presentations/scala-idris (40 минут видео)
Не очень успешно.