Type level number arithmetic

Question

I'm playing around with F#'s type inferrer. Trying to get type level natural number working.

Here's the part that I managed to get working

type Zero = Zero type Succ<'a> = None type True = True type False = False type IsZero = | IsZero static member instance (IsZero, _ : Succ<'a>, _) = fun () -> False static member instance (IsZero, _ : Zero, _) = fun () -> True module TypeArithmetic = let inline zero x = (Inline.instance (IsZero, x) : unit -> 'a)() let dec (_ : Succ<'a>) = Unchecked.defaultof<'a> let inc (_ : 'a) = Unchecked.defaultof<Succ<'a>>

The whole instance part is the same hack that makes FsControl possible. This file is also a part of my project.

So far this works. I can do things like

let a = inc Zero |> inc |> inc |> inc |> dec |> dec |> dec let b = dec a let x = zero a let y = zero b

And x and y get correctly inferred to False and True respectively (with a being inferred to Succ and b being Zero).

Now the tricky part. I want to make the function add. It needs to be able to take both Succ and Zero, so again I need to use the overloading hack to make it work.

type Add = | Add static member instance (Add, _ : Zero, _ : Zero, _) = fun () -> Zero static member instance (Add, x : Succ<'a>, _ : Zero, _) = fun () -> x static member instance (Add, _ : Zero, y : Succ<'a>, _) = fun () -> y static member instance (Add, _ : Succ<'a>, _ : Succ<'b>, _) = fun () -> Inline.instance(Add, Unchecked.defaultof<Succ<Succ<'a>>>, Unchecked.defaultof<'b>) ()

And as far as I can tell, this should work. Shouldn't it? But it doesn't. I get an error on the Inline.instance call saying the ambiguity can't be resolved with the information given prior to that point. I kind of get why, since I'm not in an inline function it tries to resolve to a concrete type, but it doesn't have one yet. But I still have a feeling that I should be able to make it work somehow.

Is there a way to make it work?

I can't quite figure out how to call that Add, but marking your last function as inline solves the immediate problem. — John Palmer
– John Palmer, Commented Sep 8, 2014 at 12:14

Gus · Accepted Answer · 2014-11-19 21:56:21Z

The problem is that only one overload should match.

You don't need more than two, you can add the Zero case and the one that will loop, which by the way should be marked inline as stated in the comments:

type Add = | Add static member instance (Add, _ :Zero , y , _) = fun () -> y static member inline instance (Add, _ :Succ<'a>, _:'b, _) = fun () -> Inline.instance(Add, Unchecked.defaultof<'a>, Unchecked.defaultof<Succ<'b>>) () let inline add x y = Inline.instance (Add, x, y)()

But then there is another problem, at the 2nd overload it will default to Zero, inferred from the 1st overload.

One trick to solve this is to add a dummy overload:

type Add = | Add static member instance (Add, _ :Add , y , _) = fun () -> y static member instance (Add, _ :Zero , y , _) = fun () -> y static member inline instance (Add, _ :Succ<'a> ,_:'b, _) = fun () -> Inline.instance(Add, Unchecked.defaultof<'a>, Unchecked.defaultof<Succ<'b>>) () let inline add x y = Inline.instance (Add, x, y)()

That way it will not default to Zero since it can't be inferred at compile time.

I did also an implementation of type level numbers some time ago, using overloaded operators and pattern matching.

UPDATE

You don't need the second argument to be polymorphic, this will also do the job:

type Add = | Add static member instance (Add, _ :Add , _) = id static member instance (Add, _ :Zero , _) = id static member inline instance (Add, _ :Succ<'a>, _) = fun (_:'b) -> Inline.instance(Add, Unchecked.defaultof<'a>) Unchecked.defaultof<Succ<'b>>

There are some differences between your implementation and the one I did (see the link) but I wouldn't use the inline helper, at least as it is defined in FsControl since it was designed specifically to infer based also in the return type.

Nice trick with the dummy overload to confuse it, but why does this work and my doesn't? Is there a case where more than one overload can match?
Also, the inferrence still doesn't work for me when I try to use the add function. let x = Zero |> inc |> inc; let y = Zero |> inc |> inc |> inc |> inc; let z = add x y Value restriction. The value 'z' has been inferred to have generic type val z : Succ<Succ< ^_a>> when (Add or Zero or Succ<Succ<Succ<Succ<Zero>>>> or ^_a) : (static member instance : Add * Zero * Succ<Succ<Succ<Succ<Zero>>>> * ^_a -> unit -> ^_a) Either define 'z' as a simple data term, make it a function with explicit arguments or, if you do not intend for it to be generic, add a type annotation
@LukaHorvat I see, but that's a value restriction, which is a minor problem, there are many ways to workaround it, for instance if you do something else with z it will be gone, e.g.: try adding this line let z_plus_1 = inc z
Oh. Ok. Is there a way to fix it other than using it somewhere or adding explicit types?
@LukaHorvat yes, I simplified the function and now it's gone, see the updated code.

Collectives™ on Stack Overflow

Type level number arithmetic

1 Answer 1

5 Comments

Linked

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

5 Comments

Linked

Related