F #: coding even and odd in (inductive) types?

Question

I read the Practical Basics of Programming Languages and found interesting and repeating inductive definitions. I managed to pretty easily code the mutually recursive version of the even and odd functions that I found on the Internet .

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 this is less clear to me (I am F # newb) if I can do this at the type level and not through a function. I have seen implementations of Peano numbers in F #, so I feel this should be possible.

Answer 1

Here is 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 manually writing constraints, !. means 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 to show how easy it is to move from a value level decision to a type decision. Then you can go ahead and write the same thing with static constraints, for completeness here, 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) 

This is more verbose but read better in intellisense, for example, a limited function will read:

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

UPDATE

Here's an alternative solution that may be closer to what you mean:

 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, as well as the DU value of this type.

Answer 2

This is not quite an ideal setup, as they are two separate encodings for succ , but it has a basic idea of ​​how it can work:

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