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

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!