f#:编码偶数和奇数(归纳)类型？

Question

我一直在阅读编程语言的实用基础,并发现迭代和同时归纳定义很有趣.我能够非常轻松地编码我在网上找到的偶数和奇数函数的相互递归版本.

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

基于皮亚诺数的这种实现，并使用运算符来避免手工编写约束，!.代表奇数和!!偶数。

// 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)

更新

这是一个替代解决方案，可能更接近您的想法：

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 值。