类型级别数字算法 [英] Type level number arithmetic

问题描述

我在玩F#的类型推断器.试图使类型级别的自然数起作用.

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>>

整个instance部分与使 FsControl 成为可能的黑客相同.这个文件也是我项目的一部分.

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

x和y分别正确地推断为False和True(a推断为Succ，b推断为零).

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

现在棘手的部分.我要使函数add. 它必须能够同时使用Succ和Zero，所以我再次需要使用重载hack使其正常工作.

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>) ()  

据我所知，这应该有效.不是吗但事实并非如此.我在Inline.instance调用中遇到一个错误，说无法用在此之前给出的信息解决歧义.我有点明白为什么，因为我不在内联函数中，所以它尝试解析为具体类型，但是还没有一个.但是我仍然觉得我应该能够以某种方式使其工作.

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?

推荐答案

问题是只有一个重载可以匹配.

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.

更新

您不需要第二个参数是多态的，这也可以完成工作:

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>>

您的实现和我实现的实现之间有一些区别(请参阅链接)，但是我不会使用内联帮助器，至少由于FsControl中已定义它，因为它专门设计为在返回时也基于推断类型.

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.

这篇关于类型级别数字算法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！