In previous post we did some “tricks” to create a generic function without creating or changing the types that function handles.

We’re going to dig more into this technique.

We can apply this technique for Type Level Programming, I mean calculations at compile time using the type inference.

A typical example on Type Level Programming is Peano numbers, but before showing the implementation at Type Level let’s have a look at the implementation of Peano numbers as Values.

Peano numbers as values:

type Peano = | Zero | Succ of Peano with static member (+) (x,y) = match x,y with | (Zero ,b) -> b | (Succ a,b) -> Succ (a + b) static member (*) (x,y) = match x,y with | (Zero ,b) -> Zero | (Succ a,b) -> (b + (a * b))

In order to test them we can write:

let p1 = Succ Zero let p2 = p1 + p1 let p2' = Zero + p2 let p0 = Zero + Zero let p1' = p1 + p0 let p4 = p2 * p2 let p0' = p0 * p2 let p0'' = p2 * p0 let p0''' = p0 * p0

All variables have the proper value but they have the same type.

For the Type Level implementation we’ll have a different type for each number.

The implementation at Type Level could be:

type Zero = Zero type Succ<'a> = Succ of 'a with static member ( + ) (Zero , b) = b static member inline ( + ) (Succ a, b) = Succ (a + b) static member ( * ) (Zero,b ) = Zero static member inline ( * ) (Succ a, b) = b + (a * b)

The very basic translation rule between both implementations is, “for each case in the discriminated union create a separate type, for each case in the match create different overloads of the same method”.

But if we try to run the same tests:

let p0 = Zero + Zero ----------------^^^^ stdin(20,17): error FS0001: The type 'Zero' does not support any operators named '+'

As we showed previously the operator resolution looks in the type of both operands. In the first and the second line it finds the definition in the Type Succ but in the third line both operands are of type Zero so it will not look in Succ type.

We can fix it easily by moving the non-inline members to the type Zero.

type Zero = Zero with static member ( + ) (Zero , b) = b static member ( * ) (Zero , b) = Zero type Succ<'a> = Succ of 'a with static member inline ( + ) (Succ a, b) = Succ (a + b) static member inline ( * ) (Succ a, b) = b + (a * b)

Now if we try the test it will work, but it will take a few seconds to compile.

In fact we don’t need to run the code, just paste the tests in a script file and rollover with the mouse over the variables and you’ll see the results.

That’s the main difference, here it’s not the run-time, it’s the type inference resolving the operations.

What about subtraction?

We can try to resolve 3 – 1 a-la Prolog saying a is 1, a + b is 3, tell me about b:

let f (a:Succ<Zero>) b : Succ<Succ<Succ<Zero>>> = a + b val f : Succ<Zero> -> Succ<Succ<Zero>> -> Succ<Succ<Succ<Zero>>>

Type inference was able to figure out that the type of b is Succ < Succ < Zero > > .

But Type Inference is not a Prolog engine, this will not work with a, but we can implement (-) and other operations.

Here’s the full code:

type Yes = Yes type No = No type Zero = Zero with static member ( + ) (Zero , b ) = b static member ( - ) (a , Zero ) = a static member ( * ) (Zero , b ) = Zero static member (.<.) (a , Zero ) = No static member (.>.) (Zero , b ) = No static member (.=.) (a:Zero, b:Zero) = Yes type Succ<'a> = Succ of 'a with static member inline ( + ) (Succ a, b ) = Succ (a + b) static member inline ( - ) (Succ a, Succ b) = a - b static member inline ( * ) (Succ a, b ) = b + (a * b) static member inline (.<.) (Succ a, Succ b) = a .<. b static member (.<.) (Zero , Succ b) = Yes static member inline (.>.) (Succ a, Succ b) = a .>. b static member (.>.) (Succ a, Zero ) = Yes static member inline (.=.) (Succ a, Succ b) = a .=. b static member (.=.) (Zero , Succ b) = No static member (.=.) (Succ a, Zero ) = No

**Conclusion**

We saw how to do recursive inlining which is something we will be using (and abusing) in the next post.

We may wonder how is this useful in real-world code.

There are some cases where Type Level Programming will help, we will use it in future posts.

This is not useful to deal with user input, we can’t go from values to types.

But we can go the other way, so it may allow us to develop F# libraries with generic and well constrained functions.

Because the inline feature exists only in the F# world, this kind of libraries will be intended to be used only from F#, although we can expose to .NET non-inline functions.