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

Question

I've been reading 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)

But it's less clear to me (I am an F# newb) if I can do this at the type level rather than via a function. I've seen implementations of Peano numbers in F# so I feel like this should be possible.

Answer 1

Here's the black-magic:

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

Based on this implementation of Peano numbers and using operators to avoid writing constraints by hand, !. stands for odd and !! for even.

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

I use operators in order to show how easy is to go from the value-level solution to the type-level solution. Then you can go ahead and write the same with static constraints, for completeness here's that version:

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)

It's more verbose but reads better at intellisense, for instance the constrained function will read:

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

UPDATE

Here's an alternative solution which might be closer to what you have in mind:

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

So here you can get the result as a type and also the DU value from that type.

Answer 2

This isn't quite an ideal setup as their are two separate encodings for succ but it has got the basic idea of how it could work:

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