问题标签 [dependent-type]

减少这种类型有什么技巧吗？我那里有一个多余x的。

Monad 是一个类型类：(Set -> Set) -> Type

假设我有一个函数（它确实像名字所说的那样）：

现在，我想以某种方式与我返回的依赖对一起工作。我写了简单的head函数：

这当然可以完美地工作。但这让我想知道：有什么方法可以确保该函数只能用 调用n ≥ 1？

理想情况下，我想做函数head : ∀ {A} → ∃ (λ n → Vec A n) → IsTrue (n ≥ succ zero) → A；但这失败了，因为n当我在IsTrue.

谢谢你的时间！

IsTrue是这样的：

"checkSimple" 获取 u，Universe U 的一个元素，并检查 (nat 1) 是否可以转换为给定 u 的 agda 类型。返回转换的结果。

现在我尝试编写一个控制台程序并从命令行获取“someU”。

因此，我将“checkSimple”的类型更改为包含一个 (u: Maybe U) 作为参数（可能是因为来自控制台的输入可能是“无”）。但是我无法获取代码进行类型检查。

我有以下使用 ghcs 扩展的固定长度向量的定义GADTs，TypeOperators并且DataKinds：

以及 TypeOperator 的以下定义:+：

为了使我的整个意图库有意义，我需要将类型的固定长度向量函数(Vec n b)->(Vec m b)应用于较长向量的初始部分Vec (n:+k) b。让我们调用那个函数prefixApp。它应该有类型

这是一个示例应用程序，其change2定义如下：

prefixApp应该能够应用于change2任何长度> = 2的向量的前缀，例如

有谁知道如何实施prefixApp？（问题是，必须使用固定长度向量函数类型的一部分来获取正确大小的前缀......）

编辑：Daniel Wagners（非常聪明！）解决方案似乎与 ghc 7.6 的一些候选版本（不是官方版本！）一起使用。恕我直言，它不应该工作，但是，有两个原因：

1. for 的类型声明在上下文中prefixApp缺少一个（用于正确类型检查。VNum mprepend (f b)
2. 更有问题：ghc 7.4.2 不假设 TypeOperator:+在其第一个参数中是单射的（也不是第二个，但这里不是必需的），这会导致类型错误：从类型声明中，我们知道vec必须有type并且类型检查器为定义右侧Vec (n:+k) a的表达式推断出. 但是：类型检查器无法推断出这一点（因为没有单射的保证）。split vecVec (n:+k0) ak ~ k0:+

有谁知道第二个问题的解决方案？我怎样才能在它的第一个论点中声明:+是单射的和/或我怎样才能完全避免遇到这个问题？

我正在尝试解析 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

有路径依赖类型，我认为可以在 Scala 中表达 Epigram 或 Agda 等语言的几乎所有特性，但我想知道为什么 Scala 不更明确地支持这一点，就像它在其他领域做得很好（比如, DSL) ? 我错过了什么，比如“没有必要”？

由于_+_-Operation forNat通常是在第一个参数中递归定义的，因此类型检查器知道它显然不是微不足道的i + 0 == i。但是，当我在固定大小的向量上编写函数时，我经常遇到这个问题。

一个例子：我如何定义一个 Agda 函数

哪个将第一个n值放在向量的末尾？

由于 Haskell 中的一个简单解决方案是

我在 Agda 中类似地尝试过，如下所示：

但是类型检查器失败并显示消息（与{zero}上述swap-Definition 中的 -case 相关）：

所以，我的问题是：如何教 Agda m == m + zero？以及如何swap在 Agda 中编写这样的函数？

我看到一些消息来源回应了“Haskell 正在逐渐成为一种依赖类型的语言”的观点。这似乎意味着随着越来越多的语言扩展，Haskell 正在朝着这个大方向发展，但还没有。

基本上有两件事我想知道。首先，很简单，“作为一种依赖类型的语言”实际上是什么意思？（希望不要太技术化。）

第二个问题是……缺点是什么？我的意思是，人们知道我们正朝着那个方向前进，所以它一定有一些优势。然而，我们还没有到那里，所以一定有一些不利因素阻止人们一路前进。我的印象是，问题是复杂性急剧增加。但是，我不确定什么是依赖类型，我不确定。

我所知道的是，每次我开始阅读有关依赖类型编程语言的内容时，文本都是完全难以理解的......大概就是这个问题。（？）

我写了一个 Agda 函数prefixApp，它将向量函数应用于向量的前缀：

我喜欢这样一个事实，它prefixApp可以在不明确提供长度参数的情况下使用，例如

（xorV : Vec Bool 2 -> Vec Bool 1向量异或函数在哪里）

不幸的是，我不知道如何编写一个postfixApp可以在不显式提供长度参数的情况下使用的函数。到目前为止，我的函数定义如下所示：

然而，这似乎postfixApp总是需要一个长度参数。例如

有谁知道如何消除这种不对称性，即如何编写一个postfixApp没有显式长度参数的函数。我想，我需要另一个split-function？