问题标签 [type-systems]

我正在阅读一篇关于 Haskell 以及 HList 是如何实现的研究论文，并想知道所描述的技术何时可以确定，何时不能确定类型检查器。此外，因为您可以使用 GADT 做类似的事情，所以我想知道 GADT 类型检查是否总是可确定的。

如果你有引用，我会更喜欢引用，这样我就可以阅读/理解解释。

谢谢！

与静态类型语言相比，动态类型语言的优点和局限性是什么？

另请参阅：对动态语言的热爱是什么（一个更具争议性的线程......）

我一直在尝试在 Scala 中编码一个关系代数（据我所知，它是最先进的类型系统之一），但似乎没有找到一种方法来达到我想要的位置。

由于我对编程语言设计的学术领域没有那么丰富的经验，所以我真的不知道要寻找什么功能。

那么，实现静态验证的关系代数需要哪些语言特性，哪些语言具有这些特性呢？

一些要求： 元组是一个函数，将名称从一组静态定义的元组有效名称映射到名称指定类型的值。让我们将此名称类型称为设置域。

关系是一组具有相同域的元组，因此任何元组的范围在集合中都是唯一的

到目前为止，模型可以很容易地在 Scala 中建模

Tuple 中的 vals、vars 和 defs 是上面定义的名称类型集。但是元组中不应该有两个同名的定义。vars 和 impure defs 也应该受到限制。

现在是棘手的部分：

两个关系的连接是一种关系，其中元组的域是来自操作数元组的域的并集。这样只保留它们域的交集具有相同范围的元组。

应该做的伎俩。

关系的投影是一个关系，其中元组的域是操作数元组域的子集。

这是我不确定是否有可能找到解决方案的地方。你怎么看？定义项目需要哪些语言特性？

上面暗示的是 API 必须是可用的。层层叠叠的样板是不可接受的。

The Wikipedia article on Effect system is currently just a short stub and I've been wondering for a while as to what is an effect system.

• Are there any languages that have an effect system in addition to a type system?
• What would a possible (hypothetical) notation in a mainstream language, that you're familiar, with look like with effects?

我通读了 Wikipedia 文章Existential types。我收集到它们被称为存在类型是因为存在运算符 (∃)。不过，我不确定这有什么意义。有什么区别

和

?

给定一个语法和附加的动作代码，是否有任何标准解决方案来推断每个产生式需要产生什么类型（因此，调用产生式应该期望从中得到什么类型）？

我正在考虑使用类似于 c#var语法的 OO 程序和操作代码（但我不是在寻找特定于 c# 的东西）。

如果不是函数重载和递归语法，这将是相当简单的。

像这样的情况会出现问题：

在静态类型的函数式编程语言中，如标准 ML、F#、OCaml 和 Haskell，函数通常会使用彼此分隔的参数和函数名称简单地通过空格来编写：

这里的类型是“ int -> (int -> int)”，即一个函数，它接受一个 int 并返回一个函数，该函数又接受一个 int 并最终返回一个 int。因此，柯里化成为可能。

也可以定义一个以元组作为参数的类似函数：

(int * int) -> int在这种情况下，类型变为“ ”。

从语言设计的角度来看，有什么理由不能简单地识别类型代数中的这两种类型模式？换句话说，使得“(a * b) -> c”简化为“a -> (b -> c)”，从而允许两个变体同样容易地被柯里化。

我想这个问题一定是在设计我提到的四种语言时出现的。那么有没有人知道任何原因或研究表明为什么所有这四种语言都选择不“统一”这两种类型模式？

我一直在网上四处寻找 Erlang 程序的各种打字实践，似乎有一些……尽管找到可靠的信息来源有点困难，即我正在寻找有关以下方面的实用信息：

1. -specs- 这个看起来很有吸引力。一些地方提到在编译时检查具有关联的 -specs 指令的函数（以确保正确的类型使用）......我似乎无法找到有关如何使用它的更多信息（使用哪个工具 - Dialyzer，打字机？）。我真的很想创建一个小的解析器/代码生成器，它可以从表单的函数声明中生成这些“规范”

我还没有看到是否-spec支持抽象类型（用户声明的类型 - “汽车”类型 -

2.这里提到的-deftype指令

如果我可以开始输入内容并在编译时检查它们，Erlang 对我来说将变得更加强大。我上面提到的解析器/代码生成的运行时将在输出源代码中生成保护类型检查。

它只存在于静态类型语言中吗？只有当语言不是强类型时才存在（即，Java 有强类型）吗？此外，它属于哪里 - 在编译阶段假设它是一种编译语言？

一般来说，当类型不明确时，规则是由语言规范规定还是由实现决定？

根据我在 StackOverflow 上找到的一些建议，我正在研究 Haskell。我很高兴看到 Haskell 的参数化类型的行为与 C# 泛型非常相似。两种语言都建议使用单个字母作为类型参数（通常），并且两种语言似乎都遵循类似的过程来用实际类型替换类型参数。因此，我很快就理解了这个概念。

这导致了这一点：Haskell 的参数化类型与 C# 泛型类型有哪些不同？我从学习 Ruby 中知道，如果你认为从一种语言熟悉的概念在你刚接触的另一种语言中是相同的，你可能会遇到很大的麻烦。通常，当功能实际上非常相似时，问题会更糟……因为它们通常不是100% 相同的。那么，如果我假设我根据我对 C# 泛型的了解理解了参数化类型，那么我可能会被哪些“陷阱”所困扰？

谢谢。