标签: idris

我开始深入研究依赖类型的编程,并发现Agda和Idris语言最接近Haskell,所以我从那里开始.

我的问题是:它们之间的主要区别是什么？类型系统在两者中是否同样具有表现力？能够进行全面的比较和关于利益的讨论会很棒.

我已经能够发现一些:

• Idris有类型类la Haskell,而Agda有实例参数
• 伊德里斯包括monadic和applicative符号
• 它们似乎都有某种可重新绑定的语法,虽然不确定它们是否相同.

编辑:此问题的Reddit页面中有更多答案:http://www.reddit.com/r/dependent_types/comments/q8n2q/agda_vs_idris/

Edwin C. Brady撰写的关于Idris影响的"使用代数效应和依赖类型进行编程和推理"的论文包含(未引用的)声明:

尽管[效果和单子变换器]在功率上并不相同 - monad和monad变换器可以表达更多概念 - 但是捕获了许多常见的有效计算.

哪些例子可以通过monad变换器建模而不是效果？

依赖类型通常被宣传为一种方法,使您能够断言程序是否符合规范.因此,例如,要求您编写一个对列表进行排序的代码- 您可以通过将"sort"的概念编码为类型并编写诸如的函数来证明代码是正确的List a -> SortedList a.但是,您如何证明规范SortedList是正确的？难道不是这样,您的规范越复杂,您对该规范作为类型的编码就越不可能吗？

有一个伊德里斯教程后,阿格达教程和许多其他的教程式的论文和介绍材料与永无止境的事情引用还得学习.我有种爬行在所有这些中间,大部分时间我坚持用数学符号和新的术语没有解释突然出现.也许我的数学很糟糕:-)

是否有任何有纪律的方法来处理依赖类型编程？就像当你想学习Haskell中,你开始与"教你一个Haskell",当你想了解斯卡拉,你开始Odersky的书,对Ruby你读与它的突变臭虫怪异的教程.但我不能用他们的书开始阿格达或伊德里斯.他们远远超过我的头脑.我试过Coq并且陷入了它的全部证明风格.Agda需要巨大的数学背景和伊德里斯,好吧,让我们暂时离开吧!

我非常了解静态类型系统,我对Scala非常熟练,如果有必要,我可以使用Haskell.我理解功能范例并且日复一日地使用它,我理解代数数据类型和GADT(实际上相当顺利),我最近成功地理解了Lambda Cube.不过,我缺乏数学和逻辑部分.

是否有任何可用于研究并可能将其用于通用/"现实世界"应用的Idris的例子？

我对Haskell有一定的精通,其中Idris似乎借用了很多,官方常见问题/文档相当不错,但是有一些更大的例子可供探讨.目标是尝试使用Idris进行实际的软件开发.TIA.

既阿格达和伊德里斯有效地禁止图案类型的值相匹配Type.似乎Agda总是在第一种情况下匹配,而Idris只是抛出一个错误.

那么,为什么typecase是一件坏事呢？它会破坏一致性吗？我无法找到有关该主题的更多信息.

我想知道在Haskell或Idris等类型语言中表达智能合约的最佳方式是什么(例如,您可以将其编译为在以太坊网络上运行).我主要担心的是:哪种类型可以捕获合同可以执行的所有操作？

天真的解决方案:EthIO

一个天真的解决方案是将合同定义为EthIO类型的成员.这种类型就像Haskell一样IO,但它不是启用系统调用,而是包括区块链调用,即它可以读取和写入区块链的状态,调用其他合同,获取块数据等等.

-- incrementer.contract

main: EthIO
main = do
   x <- SREAD 0x123456789ABCDEF
   SSTORE (x + 1) 0x123456789ABCDEF

这显然足以执行任何合同,但是:

1. 太强大了.

2. 特别是与以太坊区块链非常相关.

保守解决方案:事件采购模式

根据这个想法,合同将被定义为一系列行动的折叠:

type Contract action state = {
    act  : UserID -> action -> state -> state,
    init : state
}

所以,程序看起来像:

incrementer.contract

main : Contract
main = {
    act _ _ state = state + 1,
    init          = 0
}

也就是说,您可以定义初始状态,操作类型以及用户提交操作时该状态的更改方式.这将允许人们定义任何不涉及发送/接收资金的任意合同.大多数区块链都有某种货币,大多数有用的合约都是以某种方式涉及金钱,所以这种类型的限制性太强了.

不太保守的解决方案:事件+货币

我们可以通过将货币逻辑硬编码到上面的类型中来使上述类型知道货币.因此,我们得到类似的东西:

type Contract action state = {
    act        : UserID -> …

我一直在研究依赖类型,我理解以下内容:

1. 为什么通用量化表示为依赖函数类型.?(x:A).B(x)表示"对于所有x类型,A都有类型的值B(x)".因此它表示为其中,当给定一个功能的任何值x类型的A返回类型的值B(x).
2. 为什么存在量化表示为依赖对类型.?(x:A).B(x)表示"存在有x类型A值的类型B(x)".因此,它表示为一对,其第一个元素是类型的特定值x,A其第二个元素是类型的值B(x).

旁白:值得注意的是,通用量化总是与物质含义一起使用,而存在量化始终与逻辑联合使用.

无论如何,关于依赖类型的维基百科文章指出:

与从属类型相反的是从属对类型,从属和类型或西格玛类型.它类似于副产品或不相交的联合.

对类型(通常是产品类型)是如何类似于不相交的联合(这是一种和型)？这一直困扰着我.

此外,依赖函数类型如何与产品类型类似？

我被告知在依赖类型系统中,"类型"和"值"是混合的,我们可以将它们都视为"术语".

但是有一些我无法理解的东西:在没有Dependent Type(如Haskell)的强类型编程语言中,在编译时决定(推理或检查)类型,但是在运行时决定(计算或输入)值.

我认为这两个阶段之间肯定存在差距.试想一下如果从STDIN以交互方式读取一个值,我们如何在必须决定AOT的类型中引用该值？

例如,我需要从STDIN中读取一个自然数n和一个自然数列表xs(包含n个元素),如何将它们放入数据结构中Vect n Nat？

我只能以相当笨拙的方式在Idris 0.9.12中执行rank-n类型:

tupleId : ((a : Type) -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f _ a, f _ b)

我需要在有类型应用程序的地方使用下划线,因为当我尝试隐藏(嵌套)类型参数时,Idris会抛出解析错误:

tupleId : ({a : Type} -> a -> a) -> (a, b) -> (a, b) -- doesn't compile

一个可能更大的问题是我根本不能在更高级别的类型中进行类约束.我无法将以下Haskell函数转换为Idris:

appShow :: Show a => (forall a. Show a => a -> String) -> a -> String
appShow show x = show x

这也防止我使用伊德里斯用作类型同义词类型,例如Lens,这是Lens s t a b = …