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

Question

论文"System F with Type Equality Coercions" Sulzmann、Chakravarty 和 Peyton Jones 所著的翻译说明了 Haskell 的 newtype 的翻译。使用以下示例进入系统 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 中没有办法编写它的反函数(据我所知)。这真是一种耻辱。尽管您可以编写一种类型为 T -> IO Nat 的伪逆.另外，我的理解是 GHC 优化器可能会在递归 newtypes 上死掉。 (如果我对此有误，请有人纠正我，因为我想回去使用它们)。
相反，类型

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

和

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

这是有异常(exception)的 lambda 演算，可以以完全可逆的方式使用。
总之，在某种意义上 T根本不是一个有用的类型，但在另一种意义上它是 最有用的类型 .