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'. –

예, 중간 연산자를 사용하여 컴파일러에서 정적 제약 조건을 자동으로 추론하도록합니다. 그런 다음 멋진 asInt 함수를 정의하면 제약 조건이 전파됩니다. 연산자를 제거하고 손으로 제약 조건을 작성할 수도 있습니다. – Gustavo

나는이 솔루션을 많이 좋아하지만,'S'와'Z'를'NatNum' 타입으로 효과적으로 감싸는 방법은 무엇입니까? –

F #의 자연수의 유형 레벨 인코딩

답변

관련 문제