依赖类型是依赖于值的类型。很少有语言支持它们 - 例子包括Agda，ATS，Coq，Epigram，Scala（通过路径依赖类型，近似变体）和Idris，它们渴望生成系统级质量的本机代码。
这是一个最小的（非）工作示例。 中缀 4 _≡_ data _≡_ {a} {A : 设置 a} (x : A) : A → 设置 a 其中 参考：x == x {-# 内在平等 _≡_ #-} 数据类型₁：设置在哪里 id：类型₁ 非...
我正在尝试基于 CoqExtLib 中定义的有限映射来执行以下证明。但是，我遇到了一个问题，证明中显示的 RelDec 实例与实例不同......
在 Python 中，我经常编写函数来过滤集合以查找特定子类型的实例。 例如，我可能会在 DOM 中查找特定类型的节点，或者在......中查找特定类型的事件。
我尝试使用归纳数据类型的语法，但收到错误消息“互归纳类型必须编译为具有依赖性消除的基本归纳类型”。 以下是我的注意示例...
看起来依赖类型语言并不是图灵完备的。为什么我们不能允许每个函数都具有通用递归（这将使语言图灵完整）？ 有什么东西
例如： Agda：https://en.wikipedia.org/wiki/Agda_(programming_language)#:~:text=Agda%20is%20a%20total%20语言，可能%20to%20证明%20任意%20语句 Coq：有什么实用的
例如Agda和Coq。 与 Idris2 和 Fstar 相比。 另外，诸如 Agda 之类的依赖类型编程语言不是图灵完备的，是否存在实际缺点，或者它是……
我在 GHC.TypeNats 中找到了 withKnownNat 和 withSomeSNat 函数。根据它们的签名，可以将函数应用于动态类型参数。如果不可能，那么
我在理解依赖类型的模式匹配方面遇到了麻烦。假设我们有以下代码： 变体 Op := op1 |操作2。 变体 Res : Op -> Set := | r1：Res op1 | r2：Res op2 |...
我正在编写一些伪代码，并且想要指定具有与第一个 Int 参数相同的关联元数的函数类型 Combinator： F :: 整数 -> 列表 ->
我正在编写一些伪代码，并且想要指定具有与第一个 Int 参数相同的关联元数的函数类型 Combinator： F :: 整数 -> 列表 ->
以下段落出现在《精益定理证明 4》中关于量词和等式的章节的前面： 因此，构造微积分确定了依赖箭头类型...
如何在精益中证明a = b → a + 1 = b + 1？
我正在努力完成精益教程的第 4 章。 我希望能够证明简单的等式，例如 a = b → a + 1 = b + 1，而无需使用 calc 环境。在其他方面...
如何从命令行运行 Pie（来自 The Little Typer）？
我读《小打字机》已经有一段时间了，我现在想实际尝试一下 Pie，而不仅仅是阅读它。以下是我尝试在
我编写了一个玩具库，它使用依赖类型来表示货币及其类型签名中的货币： 数据货币 = CHF |欧元 |波兰语 |美元 派生库存（Bounded、Enum、Eq、Read、Show） d...
我有一个记录类型，在 Agda 中调用 if Foo。我可以通过生成字符串表示形式（显示 foo）并对结果字符串进行排序来对其进行排序。我有一个亲戚，请称呼它<=Foo, for comparing...
我很好奇是否存在类型名称本身不足以消除歧义的情况。 当使用类型名消歧符时，后面的限定 ID 必须是类型。 对于e...
在 Scala 3（点）或 Scala 2 中，如何使依赖类型具有传递性？
这是一个简单的例子： { // 函数中的依赖类型 def dep[B](a: 任意, bs: Seq[B]): Seq[(a.type, B)] = { val 结果：Seq[(a.type, B)] = bs.map { b => (a: a.type) ->...
我使用的是 M 型的通常共归纳定义，定义如下。 记录 M (S : 设置) (Q : S → 设置) : 设置在哪里 共感的 构造函数sup-M 场地 形状：S 位置 : Q 形状 → M ...
编辑：经过评论中的讨论，这是问题的技术部分。还有美学方面，如何巧妙地做到这一点。 如何创建依赖于参数的类，...