问题标签 [type-theory]

这是同伦类型理论书中的一个练习。这是我所拥有的：

我不知道如何证明这一点recℕ z f (succ n) ≡ f n (recℕ z f n)。我需要证明：

在英语中，给定一个自然数n和归纳假设证明了结果。

中缀运算符_∘_是正常的函数组合。和数据类型定义为_≡_：_×_

我一直在想一个解决方案，但我不知道如何解决这个问题。

考虑这段代码：

这给了我一个错误：

类型参数 U 不在其范围内；应该扩展 V。

但是，除非可以构造 A 的实例，否则应该不可能调用此函数，那么为什么 foo 的声明需要确保 U 在其范围内呢？我知道您可以通过传入来违反这一点null，但我的直觉是，健全性仍然只要求“U 扩展 V”约束在构建 A 时是可证明的，而不是在使用它时。

那么，为什么 Java 要求“U 扩展 V”在此声明中是可证明的？为什么要这样设计类型系统？

我确信在 Haskell 中，类型总是在运行时之前被擦除。在 Agda 的情况下会发生什么？

依赖类型信息是否传递到运行时？

我听说 Agda 的 Martin-Lof Type Theory with Excluded Middle 是一致的。我将如何将其添加为假设？另外，添加LEM之后，是不是经典的一阶逻辑？我的意思是，我是否也有不（对所有人）=存在（不）等价？我不知道类型论，所以如果你引用类型论中的任何结果，请添加额外的解释。

我最近在这里回答了一个问题：如何在 Typescript 中表达这一点？

这是上面的代码片段：

我已经看到这个使用了几次：

但是，Identity在范畴论文献中这个（通常是类型或这种技术）的名称是什么？有Lift更好的名字吗？

递归类型是一种类型，它具有自身的基和递归案例。

我希望它实现“类型化列表”，即其 conses 仅允许相同元素类型或 nil 的列表。

我尝试了以下定义：

但是，由于编译器试图无限期地递归列表，这表明堆栈耗尽问题（至少在 SBCL 上）。是否可以定义这样的数据类型？

我会稍微抽象一点，使问题陈述简洁明了。出于所有目的，我们假设 .NET/C# 作为底层技术/语言。

假设您正在编写一个软件程序并设计一些类/类型来表示一些感兴趣的实体。您会发现该实体具有某种具有不同状态的生命周期。当该实体的实例从一种状态转换到另一种状态时，它们会获得某些属性/属性，但会失去其他属性。

现在，如果您正在设计一个类/类型来表示此类实体，那么一种设计选择是引入一种包罗万象的类类型，该类类型包括实体在其整个生命周期中所有可能属性的超集。

另一种选择是引入某种类型的层次结构，在这种层次结构中，您使用不同的类型来表示感兴趣的实体，每种类型都表示它处于特定状态。

现在我的问题是：

1. 一般来说，如何决定使用单一类型的属性/属性与不同类型的属性/属性是否能更好地表示实体的不同状态/方面？

2. 如果您选择使用多种类型来表示您的实体：

   一个。您将如何处理该实体的某些属性在多个状态中存在/定义的情况？

   湾。例如，如果您的实体使用 JSON 进行持久化/序列化怎么办？考虑到代表不同状态的所有不同类型，您将如何对其进行序列化和反序列化？

以下两种类型是等价的：

但是，两者都不能通过展开或替换从另一个中获得，也没有任何更通用的类型可以以这种方式派生出来（AFAICS）。显然第二种类型是最小的（因为它是递归的）。给定这种类型，是否有最小化算法？显然，每个都可以从另一个派生，因为它们使用跟踪来统一。

当记录中包含的函数返回与记录相同类型的值时，就会出现这些类型。我的问题是我的编译器在目标语言中生成了两种不同的不兼容表示。

一般来说，给定任何循环，我们可以通过选择一个起点，沿着部分循环，选择一个固定点，然后再次运行到固定点来推导出一个类型。

具有不同起点的两种类型是不同的，但是可以通过将一种回溯到另一种的起点来使它们相等。这是一张图片：

考虑以下在类型检查期间获得的规范化术语表示：

我希望能够在这个框架内表示一个固定点，或者至少以一种保留其 head-normal 属性的方式表示，这对于实现替换和定义相等非常方便。

起初，我想使用在微积分本身中定义的定点组合器。不过，Y 组合子是不可能的，因为对于这个术语表示，我不能将 lambda 应用于 lambda。Z 组合器接近我想要的，但假设结果是一个函数。

如果我只是简单地进行图形缩减，我会与 Haskell 本身打成一片，从而导致一个惰性无限语法树。但是，由于这被用于依赖类型检查器，我需要能够测试术语的定义相等性——这样会陷入无限循环。

在尝试理解 scala 的类型系统时，我遇到了 F 有界类型的存在量化。

让A成为一个类型

其中F是 的 F 有界自类型A。

还有B一些亚型A

如果我尝试用存在量化声明 a ListofA

分配a的List时出现错误B。由于某种原因，scala 推断出 type List[A[Nothing]]。

当应用简化规则 4（如scala-spec中所述）时，协变的出现T可能会被上限替换（这里A[T]：）

这两个例子应该是等价的（如果我没有误解的话），但简化的例子很好。此外，以下也是正确的，应该是等价的：

但是由于某种原因，类型c和类型b不相等。

所以我的问题是：这是 scala 编译器的错误还是我误解了一些重要的东西？

编辑：我的假设是否正确，即 和 的类型c不b相等，因为存在量化中c没有看到 的协变出现T？