RankNTypesとChurch numbers

Question

ハスケルで教会の数字を勉強しようとしています。自然数がnという数字は基本的に次のタイプの関数を値に適用する式ですタイプtはn回です。考えと

type Nat = forall t. (t -> t) -> t -> t 

、私は次の方法でzero、successor、plus、multを定義することができます。私は、べき乗を定義しようとすると

zero :: Nat 
zero = \f t -> t 

succ :: Nat -> Nat 
succ n = \f -> f . (n f) 

plus :: Nat -> Nat -> Nat 
plus m n = \f -> (m f) . (n f) 

mult :: Nat -> Nat -> Nat 
mult m n = \f -> m (n f) -- Equal to \f -> (m . n) f 

-- Pointfree version 
mult' :: Nat -> Nat -> Nat 
mult' = (.) 

、私は同じ推論を適用してみたいのですが私は乗算を定義することができました。mult mnを1に適用しました。

これは、次のコード

exp' :: Nat -> Nat -> Nat 
exp' m n = n (mult m) (succ zero) 

につながる。しかし、これはGHCから次のエラーで確認してください入力しない：

Couldn't match type ‘t’ with ‘t1’ 
    ‘t’ is a rigid type variable bound by 
    the type signature for: 
     exp' :: forall t. Nat -> Nat -> (t -> t) -> t -> t 
    at church.lhs:44:3 
    ‘t1’ is a rigid type variable bound by 
    a type expected by the context: 
     forall t1. (t1 -> t1) -> t1 -> t1 
    at church.lhs:44:17 
    Expected type: ((t -> t) -> t -> t) -> (t -> t) -> t -> t 
    Actual type: Nat -> Nat 

エラーは型チェッカーは、タイプのためにインスタンス化されていないと言っているようだ

nが適切です。理想的には、式tを別の式（t -> t）でインスタンス化して式を実行する必要があります。また、私を混乱させているもの

次のコードtypechecksことです：

exp :: Nat -> Nat -> Nat 
exp m n = n ((.) m) (succ zero) -- replace mult by (.) 

誰かがここで問題に何を説明する気にしませんか？ exp'の最初の定義はtypecheckではなく、2番目のexpのtypecheksはなぜですか？

ありがとうございます！

Answer 1

それがうまくいかない理由は、Haskellで通常許可されていないいくつかの批判的なインスタンス化です。あなたは-XImpredicativeTypesをオンにした場合、あなたはそれがコンパイルするために得ることができます：

{-# LANGUAGE ImpredicativeTypes #-} 

... 

exp' :: Nat -> Nat -> Nat 
exp' m n = n (mult m) (succ zero) 

秒バージョンtypechecks mult'はとても異なっ進む型チェック、それは(.)にdefinitionally同じであっても、上位のタイプを持っているので。 (.)のタイプはより簡単です（ランク1）ので、タイプチェックはより頻繁に成功します。

GHCドキュメントの警告ImpredicativeTypesが機能しないため、私はそれを使用しないように注意します。簡単な使用にこの問題を回避newtypeそれを得るための一般的な方法：アクションでimpredicativeインスタンス化を確認するには

newtype Nat' = N { instN :: Nat } 

exp'' :: Nat -> Nat -> Nat 
exp'' m n = instN $ n (\(N q) -> N $ mult m q) (N $ succC zero) 

---

は、あなたが入力した穴を使用することができます。

exp' :: Nat -> Nat -> Nat 
exp' m n = _ (mult m) (succC zero) 

これは、タイプを報告しますforall a . (Nat -> Nat) -> Nat -> (a -> a) -> a -> a、これは(Nat -> Nat) -> Nat -> Natと同じです。nを配置したので、forall a . (a -> a) -> a -> aでこのタイプを統一する必要があります。これには、タイプ変数aをポリタイプNatでインスタンス化する必要があります。