Wyrażanie typów egzystencjalnych w F #

Question

O ile mogę powiedzieć, F # nie ma żadnego wsparcia dla typów egzystencjalnych. Tak więc szukam innego sposobu na wyrażenie mojego pomysłu.

Mam strukturę danych, a jej zawartość można interpretować na wiele różnych sposobów. W tym konkretnym przykładzie ja przypuszczam może być postrzegane jako int lub rzeczywistego:

type Packed = (* something sensible *) unit 

type PackedType = | PackedInt 
        | PackedReal 


let undefined<'a> : 'a = failwith "undefined" 

let unpackInt : Packed -> int = undefined 
let unpackReal : Packed -> real = undefined 

let packInt : int -> Packed = undefined 
let packReal : real -> Packed = undefined 

gdzie real jest czymś znaczącym, powiedzieć:

type real = int * int 

let addReal : real -> real -> real = undefined 

Teraz muszę funkcję addPacked : PackedType -> Packed -> Packed -> Packed. Chciałbym go mieć ogólnie, to jest:

type NumberOp = [forall t] { opPack : 't -> Packed; opUnpack : Packed -> 't; opAdd : 't -> 't -> 't } 

let getNumberOp (t : PackedType) = 
    match t with 
    | PackedInt -> { opPack = packInt; opUnpack = unpackInt; opAdd = (+) } 
    | PackedReal -> { opPack = packReal; opUnpack = unpackReal; opAdd = addReal } 


let addPacked (t : PackedType) (a : Packed) (b : Packed) = 
    let { opPack = pack; opUnpack = unpack; opAdd = add } = getNumberOp t 
    pack <| add (unpack a) (unpack b) 

Tutaj skończyło się NumberOp będąc existetial. Pytam więc, czy istnieje inny sposób wyrażenia tego. Nie mogę zmienić funkcji Packed, [un]pack* i typu .

Znalazłem odpowiedź this. Stwierdza, że ​​istnieje "dobrze znany wzorzec", ale tekst jest trudny do odczytania i nie mogłem go uruchomić.

Answer 1

Ogólnie można zakodować typ

∃t.F<t> 

jak

∀x.(∀t.F<t> → x) → x 

Niestety, każdy kwantyfikator ogólny wymaga stworzenia nowego typu w F #, więc wiernym kodowania wymaga dwóch typów oprócz F. Oto, jak możemy to zrobić na Twój przykład:

type 't NumberOps = { 
    opPack : 't -> Packed 
    opUnpack : Packed -> 't 
    opAdd : 't -> 't -> 't 
} 

type ApplyNumberOps<'x> = 
    abstract Apply : 't NumberOps -> 'x 

// ∃ 't. 't NumberOps 
type ExNumberOps = 
    abstract Apply : ApplyNumberOps<'x> -> 'x 

// take any 't NumberOps to an ExNumberOps 
// in some sense this is the only "proper" way to create an instance of ExNumberOps 
let wrap n = { new ExNumberOps with member __.Apply(f) = f.Apply(n) } 

let getNumberOps (t : PackedType) = 
    match t with 
    | PackedInt -> wrap { opPack = packInt; opUnpack = unpackInt; opAdd = (+) } 
    | PackedReal -> wrap { opPack = packReal; opUnpack = unpackReal; opAdd = addReal } 

let addPacked (t : PackedType) (a : Packed) (b : Packed) = 
    (getNumberOps t).Apply 
     { new ApplyNumberOps<_> with 
      member __.Apply({ opPack = pack; opUnpack = unpack; opAdd = add }) = 
       pack <| add (unpack a) (unpack b) } 

Jest wiele boi niestety tutaj. Ponadto użyłem nieprzydatnych nazw Apply dla abstrakcyjnych członków każdego typu pomocnika - możesz swobodnie zastąpić coś bardziej znaczącego, jeśli znajdziesz nazwy, które wolisz. Próbowałem zachować dość blisko twojego stylu, ale w moim własnym kodzie prawdopodobnie uniknęłabym destrukcji rekordu w addPacked, używając zamiast tego bezpośrednio akceleratorów polowych.