我一直在为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的复杂语法(。
我不能保证显式类型注释与给定的表达式匹配。然而，我应该能够排除这种根本没有居民的类型注释。
我对证明论没有任何经验，但我想序微积分已经接近我所需要的了。以下是将其应用于当前问题的尝试：
([a] -> [a]) -> [b] -> [c] -> ([b], [c])
f: [a] -> [a]
x: [b]
y: [c]
------------
goal: ([b], [c])
apply f
----------
subgoal: [a]
ABORT
如果我走在正确的轨道上，也许有更多经验的人可以告诉我。