f #: kodowanie parzystych i nieparzystych typów (indukcyjnych)?

Question

Czytałem Practical Foundations for Programming Languages i odkryłem, że interesujące są iteracyjne i symultaniczne definicje. Udało mi się dość łatwo zakodować wzajemnie rekursywną wersję parzystych i nieparzystych funkcji, które znalazłem online.

let rec even = function 
| 0 -> true 
| n -> odd(n-1) 
and odd = function 
    | 0 -> false 
    | n -> even(n-1) 

printfn "%i is even? %b" 2 (even 2) 
printfn "%i is odd? %b" 2 (odd 2) 

Ale jest to mniej oczywiste dla mnie (jestem newb F #), czy mogę to zrobić na poziomie typu raczej niż za pomocą funkcji. Widziałem implementacje liczb Peano w F #, więc uważam, że to powinno być możliwe.

Answer 1

oto czarno-magiczne:

type Yes = Yes 
type No = No 

type Zero = Zero with 
    static member (!!) Zero = Yes  
    static member (!.) Zero = No 

type Succ<'a> = Succ of 'a with 
    static member inline (!!) (Succ a) = !. a 
    static member inline (!.) (Succ a) = !! a 

let inline isEven x = !! x 
let inline isOdd x = !. x 

Na podstawie this implementation of Peano numbers i za pomocą operatorów, aby uniknąć ograniczeń zapisu ręcznie, !. oznacza nieparzyste i !! dla parzystych.

// Test 
let N1 = Succ Zero 
let N2 = Succ N1 
let N3 = Succ N2 
let N4 = Succ N3 

isOdd N3  // val it : Yes = Yes 
isEven N3  // val it : No = No 

// Test at type-level 
let inline doSomeOddStuff (x: ^t when ^t : (static member (!.) : ^t -> Yes)) =   
    () 

let x = doSomeOddStuff N3 
let y = doSomeOddStuff N4 // Doesn't compile 

Używam operatorów, aby pokazać, jak łatwo można przejść z rozwiązania poziomu wartości do rozwiązania typu poziomowego. Następnie można śmiało napisać to samo z ograniczeniami statycznymi, dla kompletności tutaj jest, że wersja:

type Zero = Zero with 
    static member Even Zero = Yes 
    static member Odd Zero = No 

type Succ<'a> = Succ of 'a with 
    static member inline Even (Succ a) : ^r = (^t : (static member Odd : ^t -> ^r) a) 
    static member inline Odd (Succ a) : ^r = (^t : (static member Even : ^t -> ^r) a) 

let inline isEven x : ^r = (^t : (static member Even : ^t -> ^r) x) 
let inline isOdd x : ^r = (^t : (static member Odd : ^t -> ^r) x) 

To bardziej gadatliwy ale brzmi lepiej intellisense, na przykład funkcja ograniczona będzie czytać:

val inline doSomeOddStuff : 
    x: ^t -> unit when ^t : (static member Odd : ^t -> Yes) 

UPDATE

Oto alternatywne rozwiązanie, które może być bliżej do tego, co masz na myśli:

type Parity = 
    | Even 
    | Odd 

type Even = Even with static member (!!) Even = Parity.Even 
type Odd = Odd with static member (!!) Odd = Parity.Odd 

type Zero = Zero with 
    static member (!!) Zero = Even 

type Succ<'a> = Succ of 'a with 
    static member inline (!!) (Succ (Succ a)) = !! a 
    static member  (!!) (Succ Zero)  = Odd 

let inline getParity x = !! x 
let inline getParityAsValue x = !! (getParity x) 

// Test 
let N1 = Succ Zero 
let N2 = Succ N1 
let N3 = Succ N2 
let N4 = Succ N3 

getParity N3  // val it : Yes = Yes 
getParity N4  // val it : No = No 
getParityAsValue N3 // val it : Parity = Odd 
getParityAsValue N4 // val it : Parity = Even 

// Test at type-level 
let inline doSomeOddStuff (x: ^t when ^t : (static member (!!) : ^t -> Odd)) =   
    () 

let x = doSomeOddStuff N3 
let y = doSomeOddStuff N4 // Doesn't compile 

Tutaj można uzyskać wynik jako typ, a także wartość DU z tego typu.

Answer 2

To nie jest całkiem idealne ustawienie jako ich są dwie oddzielne kodowania dla succ ale ma podstawowe pojęcia jak to może działać:

type Even= 
|Zero 
|Succ of Odd 
and Odd = |Succ_ of Even