问题标签 [agda]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
haskell - Agda,布尔命题
前言注意这是一个作业。已经针对第一个问题提出了一个问题。所以我们有数据类型:
现在我们被要求写这个命题
应该返回BoolProp
false
我只是对如何做到这一点感到困惑。Ptrue
但是返回BoolProp true
数据类型por
采用两个Bool
's not BoolProp
'。可能是数据类型错误。任何抬头都会很棒
我应该补充一点,eval 代码是 haskell 代码的一个片段
注意:对其进行了编辑以不放弃所有内容
agda - Agda 和二叉搜索树
请注意,这是一个作业,所以最好不要发布完整的解决方案,相反,我只是卡住了,需要一些关于我接下来应该看什么的提示。
这些已经导入:
我们需要实现这个扩大 BST 范围的函数:
到目前为止我有这个:
现在这显然不起作用,因为新边界不必严格小于/大于最小值/最大值。给出了一个提示:It is not strictly necessary, but you may find it helpful to implement an auxiliary function that widens the range of a strictly smaller than relation of the form min < max.
这就是我在这里所做的,显然我需要改变一些事情,但我认为基本的想法就在那里。
这就是我所处的位置,我只是真的不知道从这里去哪里,我已经做了尽可能多的研究,但是没有很多关于使用 Agda 的阅读材料。我是否可能需要使用 ≤-refl 或 ≤-trans?
agda - 是否有在生产中运行的示例 Agda 代码?
Agda 是一种很好的编程语言,可以探索依赖类型,玩转直觉类型理论,并试验这些东西的实现。但是已经有用 Agda 编写的“真实”程序的例子了吗?甚至可能是展示其功能的示例(类似于 xmonad 经常被称为“真实”Haskell 程序的示例)?
haskell - 直觉型理论的组合逻辑等价物是什么?
我最近完成了一门以 Haskell 和 Agda(一种依赖类型的函数式编程语言)为特色的大学课程,并且想知道是否可以用组合逻辑替换其中的 lambda 演算。使用 Haskell 似乎可以使用 S 和 K 组合器,从而使其无点。我想知道 Agda 的等价物是什么。即,可以在不使用任何变量的情况下制作一种与 Agda 等效的依赖类型函数式编程语言吗?
此外,是否有可能以某种方式用组合器代替量化?我不知道这是否是巧合,但通用量化例如使类型签名看起来像一个 lambda 表达式。有没有办法从类型签名中删除通用量化而不改变其含义?例如在:
不使用 forall 可以表达同样的事情吗?
haskell - Agda:我的代码没有类型检查(如何正确获取隐式参数?)
"checkSimple" 获取 u,Universe U 的一个元素,并检查 (nat 1) 是否可以转换为给定 u 的 agda 类型。返回转换的结果。
现在我尝试编写一个控制台程序并从命令行获取“someU”。
因此,我将“checkSimple”的类型更改为包含一个 (u: Maybe U) 作为参数(可能是因为来自控制台的输入可能是“无”)。但是我无法获取代码进行类型检查。
parsing - Agda:解析嵌套列表
我正在尝试解析 Agda 中的嵌套列表。我在谷歌上搜索,我发现最接近的是 Haskell 中的解析,但通常使用像“parsec”这样的库,这些库在 Agda 中不可用。
所以我想"((1,2,3),(4,5,6))"
用(List (List Nat))
.
并且应该支持进一步的嵌套列表(直到深度 5),例如,深度 3 将是(List (List (List Nat)))
.
我的代码很长很麻烦,它只适用于嵌套列表,(List (List Nat))
但不适用于进一步的嵌套列表。我自己没有取得任何进展。
如果有帮助,我想重用我的一个旧帖子splitBy
的第一个答案。
编辑1 **
康纳在 ICFP 的演讲是在线的——标题是“Agda-curious?”。
这是两天前的事。看看这个!!
.
观看视频:
http ://www.youtube.com/watch?v=XGyJ519RY6Y
--
EDIT2:
我发现一个链接似乎几乎是我解析所需的代码。
提供了一个tokenize
功能:
https ://github.com/fkettelhoit/agda-prelude/blob/master/Examples/PrefixCalculator.agda
--
EDIT3:
我终于找到了一个应该足够快的简单组合库。库中没有包含示例,因此我仍然需要查看如何解决问题。
链接在这里:
https://github.com/crypto-agda/agda-nplib/blob/master/lib/Text/Parser.agda
有更多来自 Nicolas Pouillard 的在线代码:
https ://github.com/crypto-agda
agda - 在 agda 中包含 with/rewrite 子句的类型,或者,如何使用 rewrite 而不是 subst?
首先是一些无聊的导入:
现在假设我有一个类型,例如由 naturals 索引。
我想证明在这种类型上运行的函数的一些等式Foo
。因为 agda 不是很聪明,所以这些将是异构的平等。一个简单的例子是
酒吧的目标是
这些|
目标在做什么?我什至如何开始构建这种类型的术语?
在这种情况下,我可以通过手动进行替换来解决这个问题subst
,但是对于较大的类型和方程式来说,这变得非常丑陋和乏味。
types - 为什么 (Set -> Set) 不能有 Set 类型?
在 Agda 中, a 的类型以如下方式forall
确定:Set1
Set1
Set
A
Set
但是,以下具有类型Set
:
我知道如果Set
有 type Set
,会有矛盾,但我看不出,如果上述三个术语中的任何一个有 type Set
,我们就会有矛盾。这些可以用来证明False吗?它们可以用来证明Set : Set
吗?