Haskell 类型过于宽松 : need to apply continuation at most once

Question

假设我有以下类型:

type Control a = (a -> a) -> a -> a

我希望在普遍量化时恰好有两个值属于这种类型:

break :: Control a
break = const id

continue :: Control a
continue = id

但是，精明的人会注意到 Control a 的类型是 Church numerals ，其中有无穷多个。有没有办法限制这种类型，使得延续最多只能应用一次？也许使用依赖类型？

---

请注意，Control 可以出现在更大函数的上下文中。例如:

mult :: Int -> Control Int
mult 0 = \k a -> k 0
mult b = \k a -> k (b * a)

如您所见，\k a -> k (b * a) 既不是 break 也不是 continue，但仍然是 的有效居民控制。然而，它并不是Control a的居民。它是 Control Int 的居民。

因此，我真正要问的是是否有一种方法可以检查延续在类型级别最多应用一次。

Answer 1

我们可能会认识到 const id 是 Church 0，而 id 是 Church 1，因此我们需要小于 2 的 Church 自然数 - 但如果您想要一个二元素类型，为什么不使用Bool？然后将 True 解释为 const id，将 False 解释为 id，或者其他方式。我们还可以说，如果Control a值在解释的图像中，那么它们是有效的。

所有具有两个居民的类型都是同构的，因此如果您限制Control(您可以对某些依赖类型执行此操作)，那么它就与Bool同构。当子集没有紧凑的独立特征时，定义类型子集更有意义。