3

F# で教会の数字を実装しようとしています。彼らは大学のコースで簡単に紹介されましたが、それ以来、私はうさぎの穴を少し下ったかもしれません. Predecessor、Successor、Add、および Operations を実行していますが、Subtract を実行できません。前任者を複数回適用する減算bを実装しようとしています。私が独特だと思うのは、私のコードの最後から 2 番目の行は機能しますが、同等であると私が想定する最後の行は機能しないということです。タイプの不一致があります。

私はF#に非常に慣れていないので、助けていただければ幸いです。ありがとうございました。

//Operations on tuples
let fst (a,b) = a
let snd (a,b) = b
let pair a b = (a,b)

//Some church numerals
let c0 (f:('a -> 'a)) = id
let c1 (f:('a -> 'a)) = f 
let c2 f = f << f
let c3 f = f << f << f
let c4 f = f << f << f << f

// Successor and predecessor
let cSucc (b,(cn:('a->'a)->('a->'a))) = if b then (b, fun f -> f << (cn f)) else (true, fun f -> (cn f))
let cPred (cn:('a->'a)->('a->'a)) = fun f -> snd (cn cSucc (false, c0)) f
//let cSucc2 cn = fun f -> f << (cn f)

// Add, Multiply and Subtract church numerals
let cAdd cn cm = fun f -> cn f << cm f
let cMult cn cm = cn >> cm
let cSub cn cm = cm cPred cn

//Basic function for checking validity of numeral operations
let f = (fun x -> x + 1)

//This works
(cPred << cPred) c3 f 0

//This doesn't
c2 cPred c3 f 0

これは、指定されたタイプの不一致エラーです (Intellisense は、これはコードの最後の行にある cPred のエラーであると言います)。出力タイプが間違っていると推測されていることがわかります。それを修正する方法はありますか、またはこの実装の記述方法に根本的な問題がありますか?

'((bool * (('a -> 'a) -> 'a -> 'a) -> bool * (('a -> 'a) -> 'a -> 'a)) -> bool * (('a -> 'a) -> 'a -> 'a) -> bool * (('a -> 'a) -> 'a -> 'a)) -> (bool * (('a -> 'a) -> 'a -> 'a) -> bool * (('a -> 'a) -> 'a -> 'a)) -> bool * (('a -> 'a) -> 'a -> 'a) -> bool * (('a -> 'a) -> 'a -> 'a)'    
but given a
    '((bool * (('a -> 'a) -> 'a -> 'a) -> bool * (('a -> 'a) -> 'a -> 'a)) -> bool * (('a -> 'a) -> 'a -> 'a) -> bool * (('a -> 'a) -> 'a -> 'a)) -> ('a -> 'a) -> 'a -> 'a'    
The types ''a' and 'bool * (('a -> 'a) -> 'a -> 'a)' cannot be unified.
4

1 に答える 1

5

type CN<'a> = ('a -> 'a) -> 'a -> 'a以下の説明では、説明を短くして煩雑さを軽減するために、(「CN」は「Church Numeral」の略)の定義を仮定します。

type の引数が必要ですが、そのような関数ではないため、 c2toの適用の試みはcPred失敗します。c2'a -> 'acPred

cPredとして宣言したため、期待される型と一致することが期待されるかもしれCN<'a> -> CN<'a>ませんが、それは真の型ではありません。引数cnを type bool*CN<'a> -> bool*CN<'a>( の型) に適用しているためcSucc、コンパイラはが のcn型を持っている必要があると推測し、期待されるものと一致しないの型を取得します。CN<bool*CN<'a>>cPredCN<bool*CN<'a>> -> CN<'a>c2

これはすべて、次の事実に帰着します。関数は、値として渡すとジェネリック性を失います。

より簡単な例を考えてみましょう:

let f (g: 'a -> 'a list) = g 1, g "a"

'aは のパラメータであり、 のパラメータではfないため、このような定義はコンパイルされませんg。したがって、 の特定の実行でfは、特定の'aものを選択する必要があり、同時に と のint両方にすることはできません。したがって、 と の両方に適用することはできません。stringg1"a"

同様に、cnincPredは type に固定されるため、それ自体bool*CN<'a> -> bool*CN<'a>の型は とcPred互換性がなくなりCN<_>ます。

単純なケースでは、明白な回避策があります: g2 回パスします。

let f g1 g2 = g1 1, g2 "a"
let g x = [x]
f g g
// > it : int list * string list = [1], ["a"]

この方法でgは、両方の回で汎用性が失われますが、異なる型 (最初のインスタンスは to int -> int list、2 番目のインスタンスは to ) に特化されstring -> string listます。

ただし、これは半分の方法であり、最も単純なケースにのみ適しています。'a一般的な解決策では、 のパラメーターでgはなく のパラメーターになりたいことをコンパイラーが理解する必要がありますf(これは通常、「上位型」と呼ばれます)。Haskell (具体的には GHC) では、拡張機能を有効にして、これを行う簡単な方法があります。RankNTypes

f (g :: forall a. a -> [a]) = (g 1, g "a")
g x = [x]
f g
==> ([1], ["a"])

ここでは、型宣言に含めることで、パラメーターgに独自のジェネリック パラメーターがあることをコンパイラに明示的に伝えています。aforall a

F# には、このような明示的なサポートはありませんが、同じ結果を達成するために使用できる別の機能であるインターフェイスを提供します。インターフェイスにはジェネリック メソッドが含まれる場合があり、これらのメソッドは、インターフェイス インスタンスが渡されるときにジェネリック性を失うことはありません。したがって、上記の単純な例を次のように再定式化できます。

type G = 
    abstract apply : 'a -> 'a list

let f (g: G) = g.apply 1, g.apply "a"
let g = { new G with override this.apply x = [x] }
f g
// it : int list * string list = ([1], ["a"])

確かに、そのような「上位関数」を宣言するための構文は重いですが、F# が提供する必要があるのはそれだけです。

CNしたがって、これを元の問題に適用するには、インターフェイスとして宣言する必要があります。

type CN = 
    abstract ap : ('a -> 'a) -> 'a -> 'a

次に、いくつかの数値を構築できます。

let c0 = { new CN with override __.ap f x = x }
let c1 = { new CN with override __.ap f x = f x }
let c2 = { new CN with override __.ap f x = f (f x) }
let c3 = { new CN with override __.ap f x = f (f (f x)) }
let c4 = { new CN with override __.ap f x = f (f (f (f x))) }

次にcSucc、次のようにしcPredます。

let cSucc (b,(cn:CN)) = 
    if b 
    then (b, { new CN with override __.ap f x = f (cn.ap f x) }) 
    else (true, cn)

let cPred (cn:CN) = snd (cn.ap cSucc (false, c0))

cPredの型が推測されていることに注意してくださいCN -> CN。まさに必要なものです。
算術関数:

let cAdd (cn: CN) (cm: CN) = { new CN with override __.ap f x = cn.ap f (cm.ap f x) }
let cMult (cn: CN) (cm: CN) = { new CN with override __.ap f x = cn.ap cm.ap f x }
let cSub (cn: CN) (cm: CN) = cm.ap cPred cn

予想どおり、それらはすべて の推論された型を取得することに注意してくださいCN -> CN -> CN。

そして最後に、あなたの例:

let f = (fun x -> x + 1)

//This works
((cPred << cPred) c3).ap f 0

//This also works now
(c2.ap cPred c3).ap f 0
于 2018-01-17T03:36:28.720 に答える