5

I was trying to encode the natural numbers as a type in F# to be able to check an equality at compile-time instead of run-time. The best I could come up with was

type Nat<'T> = abstract member AsInt : int type Z() = interface Nat<Z> with member __.AsInt = 0 type S<'P>(prev : Nat<'P>) = interface Nat<S<'P>> with member __.AsInt = 1 + prev.AsInt type TNat = static member zero = Z() :> Nat<Z> static member succ (prev : Nat<'P>) = S(prev) :> Nat<S<'P>> static member one = TNat.succ(TNat.zero) static member two = TNat.succ(TNat.one)

I'm not sure if I'm happy with the code. Can it be done in a better (or easier) way that I am overlooking?

And can I ensure that AsInt is calculated at compile time?

Improve this question
4
  • The F# type system lets you do a little bit of type-level programming, but not very much - so I think this approach is not going to work well (if you want to use this for something real). What is the context in which you're trying to do this? Commented Nov 19, 2014 at 14:21
  • 1
    I wanted to create a facility to calculate the n-th moment of a series of values with the ability to combine partial results. I though it would be neat to check at compile time that I cannot combine different moments. Which moment is calculated is fixed at compile time and high moments are almost never needed. Apart from that also curiosity :-) Commented Nov 19, 2014 at 15:06
  • 1
    That actually sounds like a pretty interesting use case. I suppose you can make that work (with what you have), though the syntax won't be much prettier. You might be able to write a type provider for something like this too i.e. Moment<3> - which is stretching the type system too, but might be a bit nicer. See mindscapehq.com/blog/index.php/2011/09/19/… Commented Nov 19, 2014 at 15:11
  • Thanks for the hint. Actually, given the nicer syntax, I think I would prefer type providers and will try them. Commented Nov 19, 2014 at 15:21

1 Answer 1

Reset to default
7

In your code, if you try:

TNat.two = TNat.succ(TNat.one)

will yield false.

Here's an alternative implementation without interfaces:

type Z = Z with static member (!!) Z = 0 type S<'a> = S of 'a with static member inline (!!) (S a) = !!a + 1 let inline asInt x = !! x let one = S Z let two = S one

By using Discriminated Unions you benefit of structural equality as well, so in this solution you have both type (at compile time) and value (at run time) equality.

By using inline, the method to be called will be resolved at compile time.

Improve this answer
Sign up to request clarification or add additional context in comments.

4 Comments

Thanks. not (TNat.two = TNat.succ(TNat.one)) is indeed ugly. I thought I needed an interface to be able to call (!!) but in your version I could simply inline to get a static member constraint, i.e. let inline asInt (n : 'T) = !!n.
Yes, I use an intermediate operator to make the compiler infer the static constraints automatically. Then when I define the nice asInt function the constraints are propagated. You can also get rid of the operator and write the constraints by hand.
I like this solution a lot, but is there any way to effectively wrap S and Z back into a NatNum type, like a discriminated union?
Sure, just change the implementation of (!!) to return a DU.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.