f＃：（誘導型の）偶数および奇数をエンコードしますか？

Question

私はPractical Foundations for Programming Languagesを読んでおり、反復と同時帰納的定義が興味深いことがわかりました。私はかなり簡単に私はonline見つけた偶数と奇数の関数の相互再帰的なバージョンをエンコードすることができました。

let rec even = function 
| 0 -> true 
| n -> odd(n-1) 
and odd = function 
    | 0 -> false 
    | n -> even(n-1) 

printfn "%i is even? %b" 2 (even 2) 
printfn "%i is odd? %b" 2 (odd 2) 

しかし、関数ではなくタイプレベルでこれを行うことができれば、私には分かりません（私はF＃newbです）。私はF＃のPeano数の実装を見てきましたので、これが可能なはずです。

Answer 1

は、ここで黒魔術です：

type Yes = Yes 
type No = No 

type Zero = Zero with 
    static member (!!) Zero = Yes  
    static member (!.) Zero = No 

type Succ<'a> = Succ of 'a with 
    static member inline (!!) (Succ a) = !. a 
    static member inline (!.) (Succ a) = !! a 

let inline isEven x = !! x 
let inline isOdd x = !. x 

this implementation of Peano numbersに基づいて、手で制約を書くのを避けるために演算子を使用すると、!.は奇数を表し、偶数を表すのはを表します。

// Test 
let N1 = Succ Zero 
let N2 = Succ N1 
let N3 = Succ N2 
let N4 = Succ N3 

isOdd N3  // val it : Yes = Yes 
isEven N3  // val it : No = No 

// Test at type-level 
let inline doSomeOddStuff (x: ^t when ^t : (static member (!.) : ^t -> Yes)) =   
    () 

let x = doSomeOddStuff N3 
let y = doSomeOddStuff N4 // Doesn't compile 

私は演算子を使用して、値レベルのソリューションからタイプレベルのソリューションへの移行が簡単であることを示します。そして、あなたが先に行くと、ここでは完全を期すために、静的な制約と同じ書き込むことができるバージョンです：

type Zero = Zero with 
    static member Even Zero = Yes 
    static member Odd Zero = No 

type Succ<'a> = Succ of 'a with 
    static member inline Even (Succ a) : ^r = (^t : (static member Odd : ^t -> ^r) a) 
    static member inline Odd (Succ a) : ^r = (^t : (static member Even : ^t -> ^r) a) 

let inline isEven x : ^r = (^t : (static member Even : ^t -> ^r) x) 
let inline isOdd x : ^r = (^t : (static member Odd : ^t -> ^r) x) 

それはより冗長ですが、例えば制約関数は読み込みます、インテリセンスで良く読み：

val inline doSomeOddStuff : 
    x: ^t -> unit when ^t : (static member Odd : ^t -> Yes) 

UPDATE

はここであなたの心に持っているものに近いかもしれない代替ソリューションです：

type Parity = 
    | Even 
    | Odd 

type Even = Even with static member (!!) Even = Parity.Even 
type Odd = Odd with static member (!!) Odd = Parity.Odd 

type Zero = Zero with 
    static member (!!) Zero = Even 

type Succ<'a> = Succ of 'a with 
    static member inline (!!) (Succ (Succ a)) = !! a 
    static member  (!!) (Succ Zero)  = Odd 

let inline getParity x = !! x 
let inline getParityAsValue x = !! (getParity x) 

// Test 
let N1 = Succ Zero 
let N2 = Succ N1 
let N3 = Succ N2 
let N4 = Succ N3 

getParity N3  // val it : Yes = Yes 
getParity N4  // val it : No = No 
getParityAsValue N3 // val it : Parity = Odd 
getParityAsValue N4 // val it : Parity = Even 

// Test at type-level 
let inline doSomeOddStuff (x: ^t when ^t : (static member (!!) : ^t -> Odd)) =   
    () 

let x = doSomeOddStuff N3 
let y = doSomeOddStuff N4 // Doesn't compile 

ここで結果をタイプとして取得し、そのタイプのDU値も取得できます。

Answer 2

succのための2つの別々のエンコーディングが自分のしているように、これは非常に理想的な設定ではありませんが、それはそれは仕事ができるかの基本的な考え方を持っている：

type Even= 
|Zero 
|Succ of Odd 
and Odd = |Succ_ of Even