types - F#中自然数的类型级编码

Question

我试图将自然数编码为 F# 中的一种类型，以便能够在编译时而不是运行时检查相等性。我能想到的最好的办法是

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)

我不确定我是否对代码感到满意。可以以我忽略的更好(或更简单)的方式完成吗？

我可以确保 AsInt是在编译时计算的？

Answer 1

在您的代码中，如果您尝试:

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

将产生错误。

这是一个没有接口(interface)的替代实现:

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

通过使用可区分联合，您还可以从结构平等中受益，因此在此解决方案中，您可以同时拥有类型(编译时)和值(运行时)平等。

通过使用内联，将在编译时解析要调用的方法。