是否有"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因为parametricity的.我很好奇是否有这个(或类似的)定义的实际用途.

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

除了例外的lambda演算,可以完全可逆的方式使用.

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