Map eine Teilmenge einer polymorphen Variante

Question

Ich möchte oft eine Funktion auf die Werte innerhalb einer Variante anwenden, so dass das Ergebnis der Funktion den gleichen Typ wie die Eingabe hat. Wie kann ich die Typen trainieren? Hier ist meine aktuelle Versuch:

module T : sig 
    type generic = 
    [ `Foo of int 
    | `Bar of int ] 

    val map : (int -> int) -> ([< generic] as 'a) -> 'a 

(* val a : [`Foo of int] *) 
end = struct 
    type generic = 
    [ `Foo of int 
    | `Bar of int ] 

    let map fn = function 
    | `Foo x -> `Foo (fn x) 
    | `Bar x -> `Bar (fn x) 
    let map : (int -> int) -> ([< generic] as 'a) -> 'a = Obj.magic map 

(* 
    let a : [`Foo of int] = `Foo 1 |> map succ 
    let b : [`Bar of int] = `Bar 1 |> map succ 
*) 
end 

Das funktioniert, wie sie ist, aber wenn ich Kommentar- der let a Linie dann bekomme ich:

Values do not match: 
    val map : (int -> int) -> [ `Foo of int ] -> [ `Foo of int ] 
    is not included in 
    val map : (int -> int) -> ([< generic ] as 'a) -> 'a 

Es ist wie a definieren scheint hat die Art der map geändert, das scheint ungerade.

Auf der anderen Seite, das nach dem Ende des Moduls setzen funktioniert:

open T 
let a : [`Foo of int] = `Foo 1 |> map succ 
let b : [`Bar of int] = `Bar 1 |> map succ 

Schließlich, wenn ich die Definition von map zu ändern:

let map : 'a. (int -> int) -> ([< generic] as 'a) -> 'a = Obj.magic map 

(dh einer expliziten gerade hinzufügen 'a. zu Beginn), dann klagt er:

Error: This definition has type (int -> int) -> ([< generic ] as 'a) -> 'a 
    which is less general than 
    'b. (int -> int) -> ([< generic ] as 'b) -> 'b 

Kann jemand erklären, was vor sich geht? Gibt es einen besseren Weg, dies zu tun? Ich kann eine GADT verwenden, um die Obj.magic zu vermeiden, aber dann muss ich es an jeden Funktionsaufruf übergeben, den ich vermeiden möchte.

Hinweis über das reale System

In meinem aktuellen Programm habe ich verschiedene Arten Knoten (Area, Project, Action, Contact, usw.) und verschiedene Operationen gelten für verschiedene Arten, aber einige sind weit verbreitet.

Zum Beispiel kann with_name jeden Knotentyp umbenennen, aber wenn ich einen Action umbenenne, dann muss das Ergebnis eine andere Aktion sein. Wenn ich ein [Area | Project | Action] umbenennen dann muss das Ergebnis ein [Area | Project | Action] sein usw.

ich ursprünglich ein Tupel verwendet, mit den gemeinsamen Details außerhalb (zB (name * Action ...)), aber das macht es schwierig für die Nutzer auf die verschiedenen Typen entsprechen (insbesondere Sie sind abstrakt) und einige Merkmale sind Teilmengen gemeinsam (z. B. können nur Project s und Action s markiert werden).

Answer 1

Sie haben gerade bei der Werteinschränkung gestochen. Der Typchecker, der die Typen in Obj.magic map und insbesondere deren Injektivität/Varianz nicht kennt, kann nicht sofort verallgemeinern und wartet auf eine Modulgrenze. Wenn Sie mit merlin schauen, zeigt es Ihnen diesen Typ an: (int -> int) -> (_[< generic ] as 'a) -> 'a. Beachten Sie die _, die eine monomorphe Typvariable zeigt. Die Typvariable wird bei der ersten Verwendung spezialisiert, daher das Verhalten beim Auskommentieren a.

Offenbar, die Typchecker verwalten an Modulgrenze zu verallgemeinern, ich werde nicht versuchen zu raten, warum, da es (Obj.) Magie beteiligt ist.

Es gibt keine offensichtliche schöne Lösung für dieses Problem, da ocaml nicht Sie die Zeilenvariable nicht lassen manipulieren und nicht spezialisieren, die Art Variable, wenn Sie einen Zweig eingeben, mit der Ausnahme, wenn gadt mit (das einer Feature-Anfrage verdienen könnte. Es bezieht sich auf).

Wenn Sie nur ein paar Fälle haben oder keine komplizierte Kombination, können Sie versuchen, dass:

module T : sig 
    type foo = FOO 
    type bar = BAR 

    type _ generic = 
    | Foo : int -> foo generic 
    | Bar : int -> bar generic 

    val map : (int -> int) -> 'a generic -> 'a generic 

    val a : foo generic 
    val b : bar generic 
end = struct 

    type foo = FOO 
    type bar = BAR 

    type _ generic = 
    | Foo : int -> foo generic 
    | Bar : int -> bar generic 

    let map (type a) fn (x : a generic) : a generic = match x with 
    | Foo x -> Foo (fn x) 
    | Bar x -> Bar (fn x) 

    let a = Foo 1 |> map succ 
    let b = Bar 1 |> map succ 
end 

Answer 2

Der einzige Weg, eine Art vielleicht geändert, wenn es schwach ist, und in der Tat, map in Ihrem Modul hat Geben Sie (int -> int) -> (_[< generic ] as 'a) -> 'a ein, beachten Sie diese _. Also, das bedeutet, dass vor Ihrer Karte verwenden, müssen Sie das T Modul verlassen:

let a = Foo 1 |> T.map succ 

arbeitet als Charme.

Was einen allgemeineren Ansatz betrifft, der keine Magie erfordert, dann würde ich folgendes verwenden. Ich werde explizit einen polymorphen Typ definieren. Der einzige Unterschied ist, dass map eine Zuordnung von 'a t zu 'a t Werte a und b eine generische Art 'a t haben wird.

module T : sig 
    type generic = 
    [ `Foo of int 
    | `Bar of int ] 

    type 'a t = 'a constraint 'a = generic 
    val a : 'a t 
    val b : 'a t 
    val map : (int -> int) -> 'a t -> 'a t 
end = struct 
    type generic = 
    [ `Foo of int 
    | `Bar of int ] 

    type 'a t = 'a constraint 'a = generic 

    let map fn = function 
    | `Foo x -> `Foo (fn x) 
    | `Bar x -> `Bar (fn x) 

    let a = `Foo 1 |> map succ 
    let b = `Bar 1 |> map succ 
end 

Aber man kann sagen, dass dies der springende Punkt verdirbt, das heißt, wollen Sie map Typ ihres Arguments zu bewahren, so dass, wenn Sie es mit Foo aufrufen sollte es Foo zurückzukehren. Das bedeutet nur, dass wir eine andere Einschränkung für unseren Typ wählen sollten, d. H. [< generic] anstelle von weniger allgemein [generic] zu verwenden. Mit anderen Worten sagen wir, dass unser 'a zu einer Untergruppe vom Typ generic polymorph ist, d. H. Dass es zu jedem Typ instanziieren kann, der eine Teilmenge von generic ist. Damit können wir auch unsere 'a t und zeigen verstecken nur generic Art in unserer Unterschrift, damit das ursprüngliche Ziel zu erreichen:

module T : sig 
    type generic = 
    [ `Foo of int 
    | `Bar of int ] 

    val map : (int -> int) -> generic -> generic 

    val a : [`Foo of int] 
    val b : [`Bar of int] 
end = struct 
    type generic = 
    [ `Foo of int 
    | `Bar of int ] 

    type 'a t = 'a constraint 'a = [< generic] 

    let map fn : 'a t -> 'a t = function 
    | `Foo x -> `Foo (fn x) 
    | `Bar x -> `Bar (fn x) 

    let a : [`Foo of int] = `Foo 1 |> map succ 
    let b : [`Bar of int] = `Bar 1 |> map succ 
end 

Answer 3

Warum benötigen Sie die Signatur der map Funktion

val map : (int -> int) -> ([< generic] as 'a) -> 'a 

Es werden macht wenig Sinn für mich, da Sie versuchen, die "Offenheit" der Variantentypen einzuschränken. Es scheint mir, dass es zwei natürliche Signaturen für die Kartenfunktion gibt. Die erste Möglichkeit ist

val map : (int -> int) -> [< generic] -> [> generic] 

so dass map f kann auf einem Subtyp von generic angewendet werden und erzeugt einen Wert, der auf natürliche Weise in jedem Supertyp von generic eingebettet ist. Die zweite Möglichkeit ist

val map : (int -> int) -> ([> generic] as 'a) -> 'a 

wo map f kann auf jedem übergeordneten Typ von generic angewandt werden, sondern nur Prozessvarianten in generic und vermutlich auch andere Werte unverändert lassen.

Die erste Signatur kann als

module T : sig 
    type generic = 
    [ `Foo of int 
    | `Bar of int ] 

    val map : (int -> int) -> [< generic ] -> [> generic ] 
end = struct 
    type generic = 
    [ `Foo of int 
    | `Bar of int ] 

    let map fn = function 
    | `Foo x -> `Foo (fn x) 
    | `Bar x -> `Bar (fn x) 
end 

Die zweite Signatur implementiert werden kann implementiert werden, wie

module T : sig 
    type generic = 
    [ `Foo of int 
    | `Bar of int ] 

    val map : (int -> int) -> ([> generic ] as 'a)-> 'a 
end = struct 
    type generic = 
    [ `Foo of int 
    | `Bar of int ] 

    let map fn = function 
    | `Foo x -> `Foo (fn x) 
    | `Bar x -> `Bar (fn x) 
    | x -> x 
end 

es wenig Sinn macht für mich eine Funktion, deren Bereich zu schreiben ist eine geschlossene Variante, ein sollte stattdessen eine klassische Summenart verwenden. Vielleicht ist es sogar unmöglich, eine solche Funktion zu schreiben, die Spezialisten bestätigen können.