types - 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# 新手)是否可以在类型级别而不是通过函数执行此操作。我已经在 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)

更新

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

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