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

问题描述

我一直在为 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 中，这样的程序将是有效的，即使我的类型验证器应该拒绝它。

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

是否有更原则性的方法可以在不依赖类型推断的情况下排除此类类型？

解决方法

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

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

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

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

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

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

ABORT

也许有更多经验的人可以判断我是否在正确的轨道上。