haskell - `newtype T = MkT (T -> T)` 有用例吗？

Question

Sulzmann、Chakravarty 和 Peyton Jones的论文“System F with Type Equality Coercions”newtype通过以下示例说明了 Haskell 到 System FC 的转换：

newtype T = MkT (T -> T)

据我了解，除了unsafePerformIO，这种类型的唯一可能值是MkT id和MkT undefined因为参数化。我很好奇这个（或类似的）定义是否有一些实际用途。

Answer 1

参数化是关于带变量的类型的值。 T没有变量，所以参数化不适用。事实上，T 有很多居民

ap :: T -> T -> T
ap (MkT f) t = f t

idT :: T
idT = MkT id

constT :: T
constT = MkT $ \t -> MkT $ \_ -> t

axiom_sT :: T
axiom_sT = MkT $ \f -> MkT $ \g -> MkT $ \a -> (g `ap` a) `ap` (f `ap` a)

该类型T是Untyped Lambda Calculus的一种实现，它是一种通用的形式系统，其功能等同于图灵机。上面的三个函数（加号ap）构成了 SKI 演算，一个等效的形式系统。

可以将任何 Haskell 数据类型编码为T. 考虑自然数的类型

data Nat = Zero | Succ Nat

我们可以编码Nat成T

church :: Nat -> T
church Zero     = MkT $ \f -> MkT $ \x -> x
church (Succ n) = MkT $ \f -> MkT $ \x -> f `ap` (church n)

现在，你是部分正确的。Haskell 中没有办法编写它的反函数（据我所知）。这真是一种耻辱。尽管您可以使用 type 编写一种伪逆T -> IO Nat。另外，我的理解是 GHCs 优化器可能会因递归而死newtypes（如果我对此有误，请有人纠正我，因为我想重新使用它们）。

相反，类型

data T = MkT (T -> T) | Failed String

和

ap (MkT f)    a = f a
ap (Failed s) _ = Failed s

这是有例外的 lambda 演算，可以以完全可逆的方式使用。

总之，从某种意义上说，T它根本不是一种有用的类型，但在另一种意义上，它是最有用的类型。