`newtype T = MkT（T - > T）`のユースケースはありますか？

Question

紙Sulzmann、Chakravartyによって"System F with Type Equality Coercions"、およびペイトンジョーンズは、次の例でHaskellのnewtypeシステムFCへの翻訳を示しています。私はunsafePerformIOがなければ、それを理解したよう

newtype T = MkT (T -> T) 

を、このタイプの唯一の可能な値は、パラメトリックのためMkT idとMkT undefinedです。私はこの（または同様の）定義に実際に使用されているものがあるかどうか不思議です。

Answer 1

パラメータの値は、の変数の型の値です。 Tには変数がないため、パラメトリックは適用されません。 Infactは、T型Tがチューリングマシンの電源ユニバーサル正式なシステムと同等、Untyped Lambda Calculusの実装である多くの住民

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) 

を有しています。上記の3つの機能（プラスap）は、同等の正式なシステムであるSKI計算を構成します。

任意のHaskellデータ型をTにエンコードすることは可能です。あなたはしかし、部分的に正しいか、今T

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

に我々はNatエンコードすることができ、自然数

data Nat = Zero | Succ Nat 

の型を考えてみましょう。 Haskellにはこれの逆関数を書く方法はありません（私が知る限り）。それは本当に残念です。あなたはタイプT -> IO Natで擬似逆数を書くことができますが。また、GHCのオプティマイザは再帰的に死ぬことができると私は理解していますnewtypes（私はこれについて間違っていると誰かが私を修正してください。

代わりに、タイプの例外を除いて、ラムダ計算で

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

と

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

は、完全に反転可能な方法で使用することができます。

結論として、ある意味ではTは有用なタイプではありませんが、別の意味では最も有用なタイプのすべてです。