Oct 272011
 

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 rather the type inference solving the operations.
What about subtraction?
We can try to solve 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 overloading 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.

Oct 052011
 

We know with static member constraints is possible to write more generic functions, duck typing is also possible.
In this series of posts I will show how combining static member constraints and operator resolution is possible to write code that otherwise is not possible with the current .Net Type System.

To illustrate this technique let’s think in an hypothetical situation where we want to implement an overloaded function that works with two different types, but we can’t change those type definitions.
So let’s create a function length : ‘a -> int and ‘a could be a list, an array or a string.

The first attempt may look like this:

type MyHelperType =
    static member length x = String.length x
    static member length x = List.length x
    static member length x = Array.length x

let length x = MyHelperType.length x

It doesn’t work, type inferred is

type MyHelperType =
  class
    static member length : x:string -> int
    static member length : x:'b list -> int
    static member length : x:'a [] -> int
  end
val length : string -> int

Although we can call MyHelperType.length [2;3;4] and MyHelperType.length “hello” we can’t get rid of the helper class at the calling site.
As we’ve seen before this is because .Net overloading is resolved at the calling site, so when we define length it picks up the first overload that match, in this case string.
Second try, we know those types have a Length property:

let inline length x = (^T: (member get_Length: unit -> int) (x))

Works, but we were lucky because we found a built-in method which exists in all those types.
However, we can’t always be that lucky, let’s try now to implement a function append (x:’a) (y:’a) where ‘a could be a string a list of chars or an array of chars.
If they were types we’re defining in the same module, no problem, we add a member cons then the rest is the same as previous solution.
Extension methods will not work, static constraints only look into the class definition.
Remember operators? They have a particular behavior, at operator resolution the compiler looks in every operand class, so for example if we have a binary operator $ : (‘a,’b) -> ‘c it looks first into class ‘a then into class ‘b for the operator definition.
So the trick is we will use an intermediary class with an operator with overloads for the second parameter.

type HelperType = HelperType with    
    static member (=>) (d:HelperType,x: list<char>) = fun y -> x @ y    
    static member (=>) (d:HelperType,x:array<char>) = fun y -> Array.append x y
    static member (=>) (d:HelperType,x:string     ) = fun y -> x + y

let inline append x = HelperType => x

The type inferred is

type HelperType =
  | HelperType
  with
    static member
      ( => ) : d:HelperType * x:char list -> (char list -> char list)
    static member
      ( => ) : d:HelperType * x:char array -> (char [] -> char [])
    static member ( => ) : d:HelperType * x:string -> (string -> string)
  end
val inline append :
   ^a ->  ^_arg3
    when (HelperType or  ^a) : (static member ( => ) : HelperType *  ^a ->
                                                            ^_arg3)

At this point we may wonder if it’s possible to write the same code without operators.
Just copy-paste the inferred type and try.

let inline append (x: ^a) :  ^_arg3 when (HelperType or  ^a) : (static member ( => ) : HelperType *  ^a ->  ^_arg3) = HelperType => x ;;

  let inline append (x: ^a) :  ^_arg3 when (HelperType or  ^a) : (static member ( => ) : HelperType *  ^a ->  ^_arg3) = HelperType => x ;;
  ------------------------------------------^^^^^^^^^^

stdin(3,43): error FS0010: Unexpected identifier in type constraint. Expected infix operator, quote symbol or other token.

It doesn’t work, I don’t know why, personally have no explanation why F# don’t accept the constraint itself infers.

Conclusion

As we’ve seen the trick consists in creating a type, specifically a discriminated union as intermediate type.
There we will implement the operators as static member, accepting an unused parameter which is a value of the DU intentionally to use an instance of that class later at the caller site, the other parameter is overloaded.
Then wrap with a function that will “hide” the DU and the operator.
This is very useful in those cases where we don’t have access to the source code of the type we’re overloading.
This way we can use inline to write more generic code, in future posts we will see more applications and more “tricks”.