1

考虑从a's 到成对的b's 和c's,的函数类型a -> (b, c)。（我将使用 Haskell 表示法来表示类型和函数，但这不是关于 Haskell 本身的问题。）有许多这样的函数，包括那些同时、一个或不(b, c)依赖于输出的函数a。

假设，特别是，第一个输出取决于a，但第二个不依赖（例如在 中\a -> (a, ())）。是否可以在多态 lambda 演算或 Hindley-Milner 中编写一个类型来表征所有且仅此类函数 - 换句话说，其子空间与a -> (b, c)同构(a -> b, c)？换句话说，我们是否可以定义一个f :: d（对于某些类型d）使得f (\a -> (a, ())), f (\a -> (a, 1)), ... 都是正确类型的，但是f (\a -> (a, a)), f (\a -> (a, snd a)), ... 都不是？

或者，有什么方法可以静态地确保 的元素a -> (b, c)具有此属性？

4

1 回答 1

4

不，它不能在多态 lambda 演算或 Hindley-Milner 中完成。为此，您需要一个类型来讨论术语级计算的属性；这称为依赖类型。有各种依赖类型的逻辑。您可以将 Coq 或 Agda 视为基于这种逻辑的编程语言的范例。

为了使类型检查是可判定的，您通常会看到这样一个f定义为采用第二个参数，这证明它的第一个函数参数具有您声明的属性。在他们能够f完全应用之前，由程序员写出令人信服的证明。组成一些语法，你会有类似的东西

f :: (g :: a -> (b, c)) -> ((x :: a) -> (y :: a) -> snd (g x) == snd (g y)) -> ...

请注意，在这里，可以在编写类型时为函数的参数命名；然后可以在函数的结果类型中引用该名称。这是依赖类型提供的特殊功能之一。

于 2021-07-23T20:49:25.337 回答