我开始深入研究依赖类型的编程,并发现Agda和Idris语言最接近Haskell,所以我从那里开始.
我的问题是:它们之间的主要区别是什么？类型系统在两者中是否同样具有表现力？能够进行全面的比较和关于利益的讨论会很棒.
我已经能够发现一些:
编辑:此问题的Reddit页面中有更多答案:http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/
我最近完成了一个大学课程,其中包括Haskell和Agda(一种依赖类型的函数式编程语言),并且想知道是否有可能用组合逻辑替换这些中的lambda演算.使用Haskell,这似乎可以使用S和K组合器,从而使其无点.我想知道Agda的等价物是什么.即,可以在不使用任何变量的情况下制作与Agda等效的依赖类型的函数式编程语言吗？
此外,是否有可能以某种方式用组合器取代量化？我不知道这是巧合,但通用量化例如使类型签名看起来像lambda表达式.有没有办法从类型签名中删除通用量化而不改变其含义？例如:
forall a : Int -> a < 0 -> a + a < a
如果不使用forall可以表达同样的事情吗？
在编写校样时,我注意到Agda的自动校对搜索经常找不到对我来说显而易见的解决方案.不幸的是,提出一个小例子,说明问题似乎很难,所以我试着描述最常见的模式.
-m到孔中以使Agda查看模块范围.我可以将该标志设为默认值吗？会有什么缺点？-m,Agda也不会考虑在let或where子句中引入的函数参数或符号.简单地尝试所有这些都有问题吗？let或where子句中引入的符号.为什么？使用auto更有效的其他习惯是什么？
依赖类型通常被宣传为一种方法,使您能够断言程序是否符合规范.因此,例如,要求您编写一个对列表进行排序的代码- 您可以通过将"sort"的概念编码为类型并编写诸如的函数来证明代码是正确的List a -> SortedList a.但是,您如何证明规范SortedList是正确的？难道不是这样,您的规范越复杂,您对该规范作为类型的编码就越不可能吗？
有一个伊德里斯教程后,阿格达教程和许多其他的教程式的论文和介绍材料与永无止境的事情引用还得学习.我有种爬行在所有这些中间,大部分时间我坚持用数学符号和新的术语没有解释突然出现.也许我的数学很糟糕:-)
是否有任何有纪律的方法来处理依赖类型编程？就像当你想学习Haskell中,你开始与"教你一个Haskell",当你想了解斯卡拉,你开始Odersky的书,对Ruby你读与它的突变臭虫怪异的教程.但我不能用他们的书开始阿格达或伊德里斯.他们远远超过我的头脑.我试过Coq并且陷入了它的全部证明风格.Agda需要巨大的数学背景和伊德里斯,好吧,让我们暂时离开吧!
我非常了解静态类型系统,我对Scala非常熟练,如果有必要,我可以使用Haskell.我理解功能范例并且日复一日地使用它,我理解代数数据类型和GADT(实际上相当顺利),我最近成功地理解了Lambda Cube.不过,我缺乏数学和逻辑部分.
既阿格达和伊德里斯有效地禁止图案类型的值相匹配Type.似乎Agda总是在第一种情况下匹配,而Idris只是抛出一个错误.
那么,为什么typecase是一件坏事呢？它会破坏一致性吗？我无法找到有关该主题的更多信息.
我一直在研究依赖类型,我理解以下内容:
?(x:A).B(x)表示"对于所有x类型,A都有类型的值B(x)".因此它表示为其中,当给定一个功能的任何值x类型的A返回类型的值B(x).?(x:A).B(x)表示"存在有x类型A值的类型B(x)".因此,它表示为一对,其第一个元素是类型的特定值x,A其第二个元素是类型的值B(x).旁白:值得注意的是,通用量化总是与物质含义一起使用,而存在量化始终与逻辑联合使用.
无论如何,关于依赖类型的维基百科文章指出:
与从属类型相反的是从属对类型,从属和类型或西格玛类型.它类似于副产品或不相交的联合.
对类型(通常是产品类型)是如何类似于不相交的联合(这是一种和型)？这一直困扰着我.
此外,依赖函数类型如何与产品类型类似？
关于这是一个数学问题还是一个问题,我有点犹豫不决,但我怀疑数学家一般不太可能不太了解或关心这个类别,而Haskell程序员可能会这么做.
因此,我们知道Hask或多或少都有产品(当然,我正在使用idealized-Hask).我对它是否有均衡器感兴趣(在这种情况下它将具有所有有限的限制).
直观地看起来并不是这样,因为你不能像套装一样进行分离,因此一般来说,子对象看起来很难构建.但是对于你想要提出的任何特定情况,似乎你可以通过在Set中计算均衡器并计算它来破解它(因为毕竟,每个Haskell类型都是可数的,并且每个可数集都是同形或者是有限类型,也可以是自然类,Haskell都有.所以我看不出我是如何寻找反例的.
现在,阿格达似乎更有前途一点:那里是比较容易形成子对象.显而易见的sigma类型? A (? x ? f x == g x)是均衡器吗？如果细节不起作用,它在道德上是均衡器吗？
(作为借口:标题模仿了为什么我们需要monad？)
有容器(和索引的)(和无用的)和描述.但是容器是有问题的,根据我很小的经验,就容器而言,比描述更难以思考.非索引容器的类型是同构的?- 这是非常不明确的.形状和位置描述有帮助,但在
?_?? : ? {? ? ?} -> Container ? ? -> Set ? -> Set (? ? ? ? ?)
? Sh ? Pos ?? A = ? ? sh -> Pos sh -> A
K? : ? {? ?} -> Set ? -> Container ? ?
K? A = A ? const (Lift ?)
我们本质上是使用?而不是形状和位置.
容器上的严格正面免费monad的类型有一个相当简单的定义,但Freermonad 的类型对我来说看起来更简单(在某种意义上,Freer …
我被告知在依赖类型系统中,"类型"和"值"是混合的,我们可以将它们都视为"术语".
但是有一些我无法理解的东西:在没有Dependent Type(如Haskell)的强类型编程语言中,在编译时决定(推理或检查)类型,但是在运行时决定(计算或输入)值.
我认为这两个阶段之间肯定存在差距.试想一下如果从STDIN以交互方式读取一个值,我们如何在必须决定AOT的类型中引用该值？
例如,我需要从STDIN中读取一个自然数n和一个自然数列表xs(包含n个元素),如何将它们放入数据结构中Vect n Nat？