why-dependent-types-matter:“为什么要依赖类型很重要”论文的配套代码

为什么依赖类型很重要 重要信息：该存储库现在。 在Agda，Idris ans Haskell的同伴代码中，Thorsten Altenkirch，Conor McBride和James McKinna撰写了“为什么从属类型很重要”一文。 本文中的原始代码使用Epigram语言，该语言已不再维护甚至不可用。 因此，我重写了现代功能语言。 有关更多信息，请参见有关， 和博客文章。