13

Sulzmann、Chakravarty、および Peyton Jones による論文「System F with Type Equality Coercions」ではnewtype、次の例で Haskell の System FC への変換について説明しています。

newtype T = MkT (T -> T)

私が理解しているように、を除いてunsafePerformIO、このタイプの唯一の可能な値はパラメトリック性のためですMkT id。MkT undefinedこの（または同様の）定義に実際の用途があるかどうか、興味があります。

4

1 に答える 1

20

パラメトリック性とは、変数を持つ型の値に関するものです。 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)

この型は、チューリング マシンと同等の機能を備えた汎用形式システムであるUntyped Lambda CalculusTの実装です。上記の 3 つの関数 (および) は、同等の形式システムである SKI 計算を形成します。ap

任意の 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。また、私の理解では、GHC オプティマイザは再帰的に停止する可能性がありますnewtypes(これについて間違っている場合は、誰かが私を訂正してください。私はそれらを使用することに戻りたいからです)。

代わりに、タイプ

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

と

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

これは例外のあるラムダ計算であり、完全に可逆な方法で使用できます。

結論として、ある意味でTはまったく有用な型ではありませんが、別の意味では最も有用な型です。

于 2012-12-04T04:00:59.190 に答える