f#：在（归纳）类型中编码偶数和奇数？

Question

我一直在阅读Practical Foundations for Programming Languages and found the Iterated and Simultaneous Inductive definitions interesting. I was able to pretty easily encode a mutually recursive version of even and odd functions I found 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

这不是一个理想的设置，因为它们是 succ 的两个独立编码，但它已经了解了它如何工作的基本概念：

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

Answer 2

这是黑魔法：

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

f#：在（归纳）类型中编码偶数和奇数？

f#: encoding even and odd in (inductive) types?

types

f#

type-theory