问题标签 [type-theory]
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.
types - What are "vocabulary types", and how many exist?
Across programming languages, I've encountered similar composite types with different names:
People often use the term vocabulary type,
yet I've never seen a definition of what makes a type "vocabulary".
Does this term have a loose definition?
What does type theory and other programming languages have to say about vocabulary types?
Is everything above a vocabulary type? Are there more?
haskell - 观察类型理论中的模式匹配
在Towards Observational Type Theory的“5. Full OTT”部分的最后，作者展示了如何在 OTT 中定义 coercible-under-constructors 索引数据类型。这个想法基本上是将索引数据类型转换为参数化，如下所示：
康纳还在观察型理论（交付）的底部提到了这种技术：
当然，解决方法是做 GADT 人所做的事情，并将归纳族明确定义为命题平等。然后你当然可以通过传递性来传输它们。
然而，Haskell 中的类型检查器知道范围内的相等约束，并在类型检查期间实际使用它们。例如我们可以写
它在类型论中不起作用，因为仅仅有一个a ~ b范围内的证明来能够用这个等式重写是不够的：这个证明也必须是refl，因为在错误假设的情况下，类型检查变得无法确定，因为终止问题（类似这样）。Fin m因此，当您在 Haskell中进行模式匹配时，m会在每个分支中重写suc n，但这在类型论中不会发生，而是留下了suc n ~ m. 在 OTT 中，根本不可能对证明进行模式匹配，因此您既不能假装证明是refl，也不能真正要求它。只能提供证明coerce或忽略它。
这使得编写任何涉及索引数据类型的东西变得非常困难。例如，向量的通常三行（包括类型签名）lookup变成了这个野兽：
可以稍微简化一下，因为如果具有可判定相等的数据类型的两个元素明显相等，那么它们在通常的内涵意义上也相等，并且自然数确实具有可判定相等，因此我们可以强制所有方程为它们的内涵对应物和模式匹配，但这会破坏一些计算属性vlookup并且无论如何都是冗长的。在更复杂的情况下处理无法确定相等性的索引几乎是不可能的。
我的推理正确吗？OTT 中的模式匹配如何工作？如果这确实是一个问题，有什么方法可以缓解它？
equality - Proof in Coq that equality is reflexivity
The HOTT book writes on page 51:
... we can prove by path induction on p: x = y that
Can someone show me how to prove this in Coq?
coq - COQ 中的 Set 到底是什么
我仍然对COQ 中的 sort Set意味着什么感到困惑。我什么时候使用Set什么时候使用Type？
在 Hott 中，集合被定义为一种类型，其中身份证明是唯一的。但我认为在 Coq 中它有不同的解释。
haskell - 将数字限制在一个范围内（Haskell）
我公开了一个带有两个参数的函数，一个是最小界限，另一个是最大界限。如何使用类型确保例如最小界限不大于最大界限？
我想避免创建一个智能构造函数并返回一个 Maybe，因为它会使整个使用变得更加麻烦。
谢谢
type-theory - 子类型和包含有什么区别？
子类型和包含有什么区别？包容是否意味着隐性强制？
haskell - 有什么方法可以限制 ADT 数据，以便只能构造有效数据？
当我想定义Integer时，我尝试了这个
但是写了上面的代码后，发现Pos Zero和Neg Zero都是可以构造的，没想到。
而当我想定义Rational时，同样的问题又出现了
我期待任何Rational n m，它应该满足m > 0 && gcd n m == 1
但我不知道如何确保我的 ADT 数据满足这些属性。因此，当我编写一些将其作为输入处理的函数时，我必须考虑这些非法情况。我希望有一些方法可以在定义 ADT 时定义一次属性，而不是每次使用它时都检查属性。
haskell - RankNTypes 和 Church 数字
我试图通过给数字一个这样的类型来研究 Haskell 中的教堂数字，其想法是自然数n基本上是将以下类型中的函数应用于时间类型值的t表达式n。
有了这个想法，我可以通过以下方式定义zero, successor, plus, ：mult
当我尝试定义幂运算时，我想尝试应用允许我定义乘法的相同推理，即将时间应用于mult m n1.
这导致以下代码
但这确实会检查来自 GHC 的以下错误：
该错误似乎表明类型检查器没有n正确实例化类型，理想情况下，类型t应该用另一个 ( t -> t) 实例化，以便表达式通过。
让我感到困惑的是以下代码类型检查：
有人介意解释这里有什么问题吗？为什么第一个定义exp'不是类型检查而是第二个exp类型检查？
谢谢！
types - 编写现实世界的程序是否需要既不是归纳也不是共归纳的类型？
或者只是有时很难证明一个类型是一个共归纳类型？
我说的是一种完全的编程语言，这意味着它不是图灵完备的，递归都是有根据的，核心递归都是有效的。图灵完备是否真的带来了比这种语言更多的东西？
haskell - 为什么我们需要 Sum 类型？
想象一种不允许数据类型使用多个值构造函数的语言。而不是写
我们会有
where :|:（这里不是|为了避免与 sum 类型混淆）是一个内置类型联合运算符。模式匹配将以相同的方式工作
如您所见，与副产品相比，它产生了扁平结构，因此您不必处理注射。而且，与 sum 类型不同，它允许随机组合类型，从而获得更大的灵活性和粒度：
我相信构造递归数据类型也不是问题
我知道联合类型存在于 TypeScript 和其他语言中，但为什么 Haskell 委员会选择 ADT 而不是它们？