如何在不依赖类型推断的情况下排除无意义的类型？

Posted 2023-05-08

【中文标题】如何在不依赖类型推断的情况下排除无意义的类型？

【英文标题】：How to exclude nonsensical types without relying on type inference?

【发布时间】：2021-07-10 14:07:46

【问题描述】：

我一直在为 javascript 开发一个类型验证器，以便为最初为动态类型设计的语言启用渐进类型。

类型验证意味着只对带有显式类型注释的术语进行类型检查，但没有推理。不幸的是，这种方法是不合理的，因为它允许键入以下程序：

foo :: ([a] -> [a]) -> [b] -> [c] -> ([b], [c])
foo f xs ys = undefined
-- foo f xs ys = (f xs, f ys)

rev :: [d] -> [d]
rev xs = undefined
-- rev = foldl (flip (:)) []    

r = foo rev ['a', 'b'] [True, False]

这种类型检查，因为类型推断被绕过。但是，r 没有任何价值，因为函数应用需要更高级别的类型。虽然 Haskell 会在执行 r 的评估后立即终止程序，但在 Javascript 中这样的程序将是有效的，即使我的类型验证器应该拒绝它。

我的第一个想法是分析类型注释并检查函数参数是否与其他参数之一兼容，但这样的方法感觉不对。

是否有更原则性的方法来排除此类类型而不依赖类型推断？

【问题讨论】：

如果您不进行类型推断，foo f xs ys = (f xs, f ys) 肯定不应该验证，因为f 接受[a] 的参数，而您正在传递它[b] 和[c]，我们不能统一这些类型，因为我们不进行推理？

即既然你都注释了它们，为什么不允许更高级别的类型，这就是我想说的。我想知道如果您将 all 函数参数视为多态，即将所有高阶函数的类型视为高阶函数，会发生什么？无论如何，您的系统可能更多地处于动态方面。 （我只是在这里大声思考）。

我不得不说这个问题我有很多不明白的地方。一些例子：forall a b c. ([a] -> [a]) -> [b] -> [c] -> ([b], [c]) 和forall b c. (forall a. [a] -> [a]) -> [b] -> [c] -> ([b], [c]) 是非常不同的类型，它们都不匹配问题的其余部分。对于第一种类型，应该不可能给r 一个通过验证的类型注释，这违反了您的“这种类型检查”断言。对于第二种类型，foo 不应通过验证。另一方面，未注释的r 首先不需要验证，那你为什么是 1/？

期望此处显示的代码失败？当然当然未经验证的代码可能会做不合理的事情。 “绕过类型推断并启动惰性评估”是什么意思？类型检查/验证在任何计算开始之前完成；惰性求值，如果它发生的话，会在计算过程中发生。第二个怎么可能导致第一个，当它稍后发生时？ “r 没有价值，因为函数应用需要更高级别的类型”是什么意思？为什么更高级别的类型会与评估发生冲突？您的声明“Haskell 在r 的 2/? 时立即终止程序？

执行了评估”，但这...是不正确的。要么它在评估开始之前就被终止，完全独立于r的评估是否被强制执行，或者它运行完成，即使在r的评估被强制执行之后。所以......在尝试对所有这些不正确的假设/断言进行心理纠正之后，我处于一切看起来都很好和健全的状态（除非没有-type-validated 代码，无法修复），并且完全不确定问题是什么。3/3

【参考方案1】：

我们的目标是排除无意义的类型注释而不从术语推断类型，因为检查定义不是我的类型验证器的一部分（很难考虑 JS 的复杂语法）。

我不能保证显式类型注释与给定表达式匹配。但是，我应该能够排除这种根本没有居民的类型注释。

我没有任何证明理论的经验，但我猜sequent calculus 接近我所需要的。以下是尝试将其应用于手头的问题：

([a] -> [a]) -> [b] -> [c] -> ([b], [c])

f: [a] -> [a]
x: [b]
y: [c]
------------
goal: ([b], [c])

apply f
----------
subgoal: [a]

ABORT

如果我走在正确的轨道上，也许有更多经验的人可以判断。

【讨论】：

在“应用f”之后，“子目标：[a]”指的是什么？论据，还是应用的结果？ （因为fix f :: [a]...）。

BTW foo :: ([a] -> [a]) -> [b] -> [c] -> ([b], [c]); foo _f a b = (a,b) 类型检查，所以类型 是 微不足道的居住。

@WillNess 子目标指的是论点。

@WillNess 是的，但这就是我所说的无意义类型。这个声明只有在_f 无效时才有意义。所以我又错了。无论如何，我需要通过引入显式类型等式来指导统一算法，有点像 GADT。这就是我这个周末要尝试的。感谢您的耐心：D

（所以，对于fix，我们不需要参数）。