` -> T= MkT (T `newtype )`有没有用例？
` -> T= MkT (T `newtype )`有没有用例？
提问于 2012-12-04 11:42:16
苏兹曼、查克拉瓦蒂和佩顿·琼斯的论文"System F with Type Equality Coercions"通过以下示例说明了如何将哈斯克尔的newtype转换为系统FC：
newtype T = MkT (T -> T)据我所知，由于参数的原因，除了unsafePerformIO之外，这种类型的唯一可能值是MkT id和MkT undefined。我很好奇这个(或类似的)定义是否有一些实际用途。
回答 1
Stack Overflow用户
回答已采纳
发布于 2012-12-04 12:00:59
参数化是关于具有变量的类型的值。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类型编写一种伪反函数。另外，我的理解是GHCs优化器可能会死于递归newtypes (如果我说错了，请有人纠正我，因为我想回去使用它们)。
相反，类型
data T = MkT (T -> T) | Failed String使用
ap (MkT f) a = f a
ap (Failed s) _ = Failed s它是带有异常的lambda演算，可以以一种完全可逆的方式使用。
总而言之，从某种意义上说，T根本不是一种有用的类型，但从另一种意义上讲，它是所有中最有用的类型。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/13695726
复制相关文章
相似问题
腾讯云开发者
