问题标签 [type-theory]

在这个问题中，未标记的联合被描述为一种子类型。

类型类也是子类型的一种形式。

它们在概念上是否等效？他们是，我将如何在 Haskell 中实现这些？

在维基百科中，底部类型被简单地定义为“没有值的类型”。但是，如果b是这个空类型，那么产品类型(b,b)也没有值，但看起来与b. 我同意底部是无人居住的，但我认为这个属性不足以定义它。

通过Curry-Howard 对应关系，底部与数学错误相关联。现在有一个逻辑原则表明从 False 遵循任何命题。对于Curry-Howard，这意味着该类型forall a. bottom -> a是有人居住的，即存在一个函数族f :: forall a. bottom -> a。

那些功能是f什么？它们是否有助于定义底部，也许是所有类型的无限产物forall a. a？

显然， Haskell 中有一种叫做无限类型的东西。

例如，当我尝试iterate concatGHCi 时，我得到了这个：

我的问题是，究竟什么是无限类型？它们如何适应类型理论以及我可以从哪些资源中了解它们？是否有任何允许无限类型的编程语言？

我正在观看Bartosz Milewski 的这个讲座，他正在解释 coproduct 和 sum 类型。

在讲座上，他从一个到另一个。

联积与总和类型相同吗？

我一直在尝试围绕 Ada 进行研究，并且我一直在阅读一些关于Agda 和 Idris 中的依赖类型的内容。

是否可以说Ada 中的子类型等同于依赖类型？

我试图在精益中证明，如果一个项目小于排序列表的头部，它就不是列表的成员。

在匹配t列表的尾部 as(y::ys)之后，我预计该假设Hs: is_sorted (h::t)会被传播，并添加is_sorted (y::ys)为假设（我发现 Idris 正是这样做的），但在 Lean 中似乎并非如此。此外，没有传播相等性t = (y::ys)，所以我不确定如何证明is_sorted (y::ys).

当模式匹配传播这个假设时，我需要做一些额外的事情吗？

我将 is_sorted 定义为：

_作为占位符的上下文中的假设是：

作为参考，Idris 的定义is_sorted，它在 Idris 中产生所需的行为：

伊德里斯证明：

我还尝试将 Lean 定义为更接近 Idris 定义，:向左移动以允许模式匹配：

但在这种情况下，Lean 抱怨invalid pattern, 'x' already appeared in this pattern（也适用于 h、y 和 ys）。如果我例如重命名h为h1，那么它会抱怨given argument 'h1', expected argument 'h'。我发现实际上似乎可以通过将x,y和ys参数设置为is_sorted_many隐式来解决此问题，因此不必匹配它们，但这似乎有点 hacky。

使用依赖类型，可以为排序列表定义归纳类型，例如：

这可以用来推理排序列表。

在 Coq 中，也可以编写一个函数Fixpoint is_sorted: {A: Type} (l: List A) : bool，然后is_sorted someList = true通过unfold定义is_sorted. 后一种方法在 Idris 中是否可行，还是仅支持前一种方法？

此外，就我自己的理解而言：后一种情况是“反思证明”的一个例子，是否存在后一种方法比前一种方法更可取的情况？

Lean 带有一个decidable_linear_order类型类，其中包含关于排序及其与相等关系的有用引理，例如：

lemma eq_or_lt_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ a < b) : a = b ∨ b < a

这些排序中的等式都用 表示=：

我想知道是否有可能以某种方式扩展这个类（及其超类）以使用任意使用的定义相等关系R: α → α → Prop，该关系是自反的、对称的和传递的，或者这只能通过重写所有相关的引理及其证明来实现使用R而不是eq？

假设我有一个类型：

并且可以确定：

如果我有一个特定的列表：

def l1: list ℕ := [2,3,4,5,16,66]

是否可以证明它是在“编译时”排序的；生产is_sorted l1顶级产品？

我试过def l1_sorted: is_sorted l1 := if H: is_sorted l1 then H else sorry了，但我不知道如何证明后一种情况是不可能的。我也尝试过这种simp策略，但似乎没有帮助。

我可以用 来证明它#reduce，但不可能将它的输出分配给变量。