Типовое кодирование натуральных чисел в F #

Я пытался кодировать натуральные числа как тип в F #, чтобы иметь возможность проверять равенство во время компиляции, а не во время выполнения. Лучшее, что я мог придумать, былоТиповое кодирование натуральных чисел в 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 был рассчитан во время компиляции?

источник

2014-11-19 Mathias Körner

Система типа F # позволяет вам немного программировать на уровне уровня, но не очень, поэтому я думаю, что этот подход не будет работать хорошо (если вы хотите использовать его для чего-то реального). Каков контекст, в котором вы пытаетесь это сделать? –

Я хотел создать средство для вычисления n-го момента ряда значений с возможностью объединения частичных результатов. Я бы сказал, что было бы аккуратно проверять во время компиляции, что я не могу совмещать разные моменты. Какой момент рассчитывается, фиксируется во время компиляции, а высокие моменты почти никогда не нужны. Помимо этого также любопытство :-) –

Это на самом деле похоже на довольно интересный вариант использования. Я полагаю, вы можете сделать эту работу (с тем, что у вас есть), хотя синтаксис будет не намного красивее. Возможно, вы можете написать провайдер типа для чего-то вроде этого, например, «Moment <3>' - который также растягивает систему типов, но может быть немного приятнее. См. Http://www.mindscapehq.com/blog/index.php/2011/09/19/f-type-providers-as-if-by-magic/ –

В вашем коде, если вы попробуете:

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

даст ложные.

Вот альтернативная реализация без интерфейсов:

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

Используя дискриминированных Союзы Вы получаете выгоду от структурного равенства, а также, так что в этом решении у вас есть оба типа (во время компиляции) и значения (во время выполнения) равенство.

С помощью встроенного метода метод, который будет вызываться, будет разрешен во время компиляции.

источник

2014-11-19 16:45:04 Gustavo

Спасибо. 'not (TNat.two = TNat.succ (TNat.one))' действительно уродливо. Я думал, что мне нужен интерфейс, чтобы иметь возможность называть '(!!)', но в вашей версии я мог бы просто встроить, чтобы получить статическое ограничение-член, т. Е. 'Let inline asInt (n: 'T) = !! n'. –

Да, я использую промежуточный оператор, чтобы заставить компилятор автоматически устанавливать статические ограничения. Затем, когда я определяю функцию nice asInt, распространяются ограничения. Вы также можете избавиться от оператора и написать ограничения вручную. – Gustavo

Мне нравится это решение много, но есть ли способ эффективно обернуть 'S' и' Z' обратно в тип 'NatNum', например, дискриминационный союз? –

Типовое кодирование натуральных чисел в F #

ответ

Смежные вопросы