having fun with type-level numbers using a type-provider

If you just want to see the code or even play with it, you can just grab it from Github

graphics-christmas-reindeer-808473

It all started with me promising I would try to write an article how to use F# type providers to express prime numbers as types.

Having had not much exposure to type providers prior to that the claim haunted me for the last couple of days (the subtle things that drives you nuts … ). But in the end it was a real fun thing to do and maybe you find some enjoyment here – just don’t expect to use this in your next project ;)

I had to first come up with some kind of context – some semi-use-case where prime-numbers as types might really come in handy. The easiest thing I could think of was their connections to the ring of integers modulo n (that will turn into a field if n is a prime). So let’s try to make illegal operations unrepresentable so that for example you cannot add \(3 + 4\mathbf{Z}\) to \(2 + 5\mathbf{Z}\) or try to divide by \(2 + 8\mathbf{Z}\)

some background

Just as a quick reminder (I think most programmers have a basic grasp on this stuff):

Modular arithmetic – often called clock arithmetic because everyone knows this from dealing with time – is just your every-day arithmetic: \( 11 + 5 = 16 \) but returning only the remainder after division by a fixed number \(n\).

The clock example would work with \(n = 12\) and so \( 11 + 5 = 4\ (mod\ 12) \) because if you go to bed at 11 PM and sleep for 5 hours you will wake up at 4 AM the next day ;)

Now math has some scary-sounding names and abstract concepts to describe this in more detail but I will just hand-wave over most of this stuff – it’s only the stage for my types after all. If you like you can find much on this if you browse Wikipedia, maybe starting at quotient rings. Anyway – one important property is this:

If \(p\) is a prime then \( \mathbf{Z}/{p\mathbf{Z}} \) is a field and you can divide \( mod\ p \)!

The constructive proof using the extended Euclidean algorithm is quite simple so the nerd in me just have to give you a glimpse: Starting from two natural numbers (better forget 0 for now) \(a\) and \(b\) you can use the algorithm to constructs two more integers \(x\) and \(y\)) such that

$$ ax + by = gcd(a,b) $$

where \(gcd\) is the greatest-common-divisor. Now if \(p\) is prime and \(a\) some natural number between \(1\) and \(p-1\) (exactly those we are interested in) then of course
\(p\) and \(a\) are co-prime (just meaning their \(gcd\) is 1) and (using the algorithm) we have can find integers such that:

$$ ax + py = gcd(a,p) = 1 $$

Now \(mod p\) this simplifies to

$$ ax = 1 (mod\ p)$$

which shows that \(x\) is the inverse of \(a\) in our little ring (that really is a field now).

So you can use the extended Euclidean Algorithm to construct a inverse – that’s exactly what I am gonna do next – finally in code again ;)

working the math out in Fsharp

As you’ve seen above we only really need to implement the extended Euclidean algorithm and for this I need a small helper function first:

let mod' a b =
    match a % b with
    | pos when pos >= 0 -> pos
    | neg               -> -neg

I need this because the inbuilt mod operator just does not deal with negative numbers in the way I need here. In math and for the algorithm we are gonna implement next we need that

$$ 0 \leq a \ mod\ n < n $$

for all \(a\) and \(n\) but for example (-5) % 3 will return -2 instead of the 1 we are expecting (because \( -5 = -2 \cdot 3 + 1 \)). The helper function fixes that.

Now the implementation of the extended Euclidean algorithm just follows the Wiki:

let rec extEulkid a b =
    match (a,b) with
    | (a,0) -> (a,1,0)
    | (a,b) ->
        let (d,s,t) = extEulkid b (mod' a b)
        (d,t,s - t * (a / b))

natural numbers as types

Next I want to express numbers \(mod \ n\) as a data-type – now the usual way would be to include n as an parameter to the constructor or something similar. But I want to make it part of the type-definition in a generic way instead, as this will help us make those mixed operations (I mentioned above) impossible to compile.

Let’s just use simple data-types for numbers (later provided for us) that all implement this interface:

type INum =
    abstract GetValue : unit -> int

The types themselfes will be singleton types (with only one type-inhabitant – but I will not enforce this) having a parameter-less constructor like this:

type N4 () =
  interface INum with
    member i.GetValue () = 4

disclaimer

You might already see some strange design decisions here. For example why a function instead of a property?

Most of this is just me being pragmatic. I had some problems implementing interfaces inside a type-provider (for example I could figure out how to implement methods but had problems with properties/fields) and so I decided to stop here – make sure to read the other great posts on type-providers on the advent calendar too – for example yesterdays – most likely you can see how to really do it there ;)

primes

Prime numbers will just implement another interface too:

type IPrime =
    inherit INum

so inside of .net’s type system I can use those interfaces to constraint generic parameters to a number or even a prime number this way.

providing the types

This is where I cheat a bit. The main idea was to use types to make invalid states unrepresentable instead of throwing runtime exceptions (as a smart-constructor or operations with guards might). But of course I just refactor this runtime checks out into the type-provider ;)

Anyway after struggling a bit I managed to implement the type provider for numbers/primes you can use like this:

type numbers = Numbers.NumbersProvider<"4,5">

type N5 = numbers.N5
type N4 = numbers.N4

The type-provider will just take the static parameters you gave as a string (representing a list of numbers you want) and provide a type for each one of these. The types will all implement INum and those representing primes will implement IPrime as well.

The code itself is highly technical and a bit boring so please just have a look at the github repository if you are interested in all of it. I’ll just give you some hints on things I struggled with.

The first thing I had to learn was that I may not use erased types if I want to interfaces. Basically that means to set IsErased to false for each provided type. But this alone will just give you some interesting errors. Right now the trick seems to be that you have to add all types provided in that way to an temporary assembly on disk too and register it within your provider – so the basic layout of my provider looks like this:

[<TypeProvider>]
type NumbersProvider (config : TypeProviderConfig) as this =
    inherit TypeProviderForNamespaces ()

    let ns  = "Numbers"
    let asm = Assembly.GetExecutingAssembly()

    let tempAsmPath = 
       System.IO.Path.ChangeExtension(
          System.IO.Path.GetTempFileName(), ".dll")

    let tempAsm     = ProvidedAssembly tempAsmPath

    let numbersProvider = 
       ProvidedTypeDefinition(
          asm, ns, "NumbersProvider", 
          Some(typeof<obj>), IsErased = false)

    let parameters = 
       [ ProvidedStaticParameter("Numbers", typeof<string>) ]

    // (snip .. the details)

    do
        numbersProvider.DefineStaticParameters (
            parameters, 
            fun typeName args ->
                let numbers =
                    args.[0] :?> string
                    |> fun s -> s.Split ([|','; ';'|])
                    |> Array.map Int32.Parse

                let templateType = 
                    ProvidedTypeDefinition(asm, ns, typeName, 
                                           Some typeof<obj>, 
                                           IsErased = false)
                    |> addEmptyConstructor

                numbers |> Seq.iter (addNumberType templateType)

                tempAsm.AddTypes [templateType]
                templateType
            )

        this.RegisterRuntimeAssemblyLocationAsProbingFolder config
        tempAsm.AddTypes [numbersProvider]
        this.AddNamespace(ns, [numbersProvider])

Inside (the snip comment) I use a couple of helper functions:

To add an empty constructor to a type (I need this for example to instantiate one of the number-types to get to their GetValue later):

let addEmptyConstructor (t : ProvidedTypeDefinition) =
    let ctor = ProvidedConstructor []
    ctor.InvokeCode <- (fun _ -> <@@ () @@>)
    t.AddMember ctor
    t

To add a Value property and the implementation for the INum interface to a type:

let addValueProperty 
    (numberType : ProvidedTypeDefinition) 
    (n : int) =
    let valueProp = 
       ProvidedProperty("Value", 
                        typeof<int>, 
                        IsStatic = false,
                        GetterCode = (fun args -> <@@ n @@>))
    numberType.AddMemberDelayed (fun () -> valueProp)

    let igetMeth = typeof<INum>.GetMethod "GetValue"
    let getV = 
        let code (_args: Expr list) = <@@ n @@>
        let m = ProvidedMethod(
                  "GetValue", [ ], 
                  typeof<int>, InvokeCode=code) 
        m.SetMethodAttrs(MethodAttributes.Virtual 
                         ||| MethodAttributes.HasSecurity 
                         ||| MethodAttributes.Final 
                         ||| MethodAttributes.NewSlot 
                         ||| MethodAttributes.Private)
        m
    numberType.AddInterfaceImplementation typeof<INum>
    numberType.DefineMethodOverride(getV, igetMeth)
    numberType.AddMembers [ (getV :> MemberInfo) ]

This is the one I was struggling with a bit – I had to find the needed Attributes from a real-life implementation on github.

And finally to add a provided number type:

let addNumberType 
    (toType : ProvidedTypeDefinition) 
    (n : int) =
    let typeName = sprintf "N%d" n
    let numberType = 
        ProvidedTypeDefinition(
           typeName, Some typeof<obj>, 
           IsErased = false)
        |> addEmptyConstructor

    if isPrime n
    then numberType.AddInterfaceImplementation typeof<IPrime>

    addValueProperty numberType n
    toType.AddMemberDelayed (fun () -> numberType)

As you can see I provide a non-erased type named N5 (for example) that implements INum (will happen inside addValueProperty and IPrime (if the number n was a prime number) together with an empty default-constructor.

If you are wondering: isPrime is just a small helper function checking if n is a prime number:

let isPrime n =
    if n = 1 then false else
    [2 .. n-1]
    |> Seq.takeWhile (fun d -> d*d <= n)
    |> Seq.forall    (fun d -> n % d <> 0)

representing the integers modulo n with a type

Now it’s not that hard to wrap up the numbers mod n inside a type – we can use generic constraints to only allow INum types having a default-constructor (remember all our provided types will have) and implement the type like this:

type Mod<'n when 'n :> INum 
            and 'n : (new : unit -> 'n)> x =
    let n = (new 'n ()).GetValue()
    let value = mod' x n

    member private __.Value      = value
    override       __.ToString() = 
        sprintf "%d (MOD %d)" value n

    static member (+) (a : Mod<'n>, b : Mod<'n>) =
        Mod<'n> (a.Value + b.Value)

    static member ( * ) (a : Mod<'n>, b : Mod<'n>) =
        Mod<'n> (a.Value * b.Value)

    static member (-) (a : Mod<'n>, b : Mod<'n>) =
        Mod<'n> (a.Value - b.Value)

    static member create x = Mod<'n> x

Please note that I use the mod' helper function from above to constraint the represented numbers to \(0 .. n-1\) in the constructor and I get the value out of the type by using the default constructor and the GetValue method from the INum interface – that’s the hacky part here.

That’s it – we can finally have some fun:

let modN<'n when 'n :> INum and 'n : (new : unit -> 'n)> x =
    Mod<'n>.create x

let res : Mod<N5> = modN 3 + modN 3 * modN 2;;
val res : Mod<N5> = 4 (MOD 5)

let res = (modN 3 : Mod<N4>) + (modN 4 : Mod<N5>);;
error FS0001: Type constraint mismatch.

primes and the field

Sadly I could not think of a nice way (unlike my Haskell example for this) to reuse the code so I need to redo the work and make another type for fields:

type ModF<'p when 'p :> IPrime and 'p : (new : unit -> 'p)> x =
    let p = (new 'p ()).GetValue()

    // (snip) ... same as before

    static member (/) (a : ModF<'p>, b : ModF<'p>) =
        ModF<'p> (a.Value * invMod<'p> b.Value)

    static member create x = ModF<'p> x

But having that we can now divide in a type-safe way too:

let modF<'p when 'p :> IPrime and 'p : (new : unit -> 'p)> x =
    ModF<'p>.create x

// ho ho ho ... 
printfn "4 / 3 = %A" (modF 4 / modF 3 : ModF<N5>)
// = 4 / 3 = 3 (MOD 5)

// you are naughty
printfn "4 / 3 = %A" (modF 4 / modF 3 : ModF<N4>)
// -> error FS0001: The type 'N4' is 
// not compatible with the type 'IPrime'

conclusion

I love Making illegal states unrepresentable and I hope I could show you that you can indeed take this idea quite a long way if you really want.

Type providers give us the power to cheat where Fsharps type system is lacking in power (to a certain degree), although I still would prefer a improved type system where I could express more invariants directly in code but I guess this will not happen :(

Many thanks to

Michael Newton helped my quite a bit on twitter. I basically followed his guide to build my provider: Type providers from the ground up and he did yesterdays advent calendar post too – so make sure to say Hello!

FunctionalSanta