Ist dieses Snippet legaler Standard ML gemäß der Definition?

Question

Ist das Code-Snippet unter dem rechtlichen Standard ML gemäß der Definition angegeben? Es Typprüfungen mit Poly/ML, aber nicht mit Moskau ML:

infixr 5 ::: ++ 

signature HEAP_ENTRY = 
sig 
    type key 
    type 'a entry = key * 'a 

    val reorder : ('a -> key) -> 'a * 'a -> 'a * 'a 
end 

signature HEAP_TAIL = 
sig 
    structure Entry : HEAP_ENTRY 

    type 'a tail 

    val empty : 'a tail 
    val cons : 'a Entry.entry * 'a tail -> 'a tail 
    val uncons : 'a tail -> ('a Entry.entry * 'a tail) option 
    val ++ : 'a tail * 'a tail -> 'a tail 
end 

signature SIMPLE_FOREST = 
sig 
    structure Entry : HEAP_ENTRY 

    type 'a tree 
    type 'a tail = (int * 'a tree) list 

    val head : 'a tree -> 'a Entry.entry 
    val tail : int * 'a tree -> 'a tail 
    val cons : 'a Entry.entry * 'a tail -> 'a tail 
    val link : (int * 'a tree) * 'a tail -> 'a tail 
end 

structure IntRank = 
struct 
    fun reorder f (x, y) = if f x <= f y then (x, y) else (y, x) 

    fun relabel' (_, nil, ys) = ys 
    | relabel' (r, x :: xs, ys) = 
     let val r = r - 1 in relabel' (r, xs, (r, x) :: ys) end 

    fun relabel (r, xs) = relabel' (r, xs, nil) 
end 

functor SimpleForestTail (F : SIMPLE_FOREST) :> HEAP_TAIL 
    where type Entry.key = F.Entry.key = 
struct 
    open F 

    val empty = nil 

    fun link ((x, xs), ys) = F.link (x, xs ++ op:: ys) 
    and xs ++ nil = xs 
    | nil ++ ys = ys 
    | (op:: xs) ++ (op:: ys) = link (IntRank.reorder (#1 o #1) (xs, ys)) 

    fun pick args = #1 (Entry.reorder (#1 o head o #2 o #1) args) 
    fun attach (x, (y, xs)) = (y, x :: xs) 
    fun extract (xs as (x, op:: ys)) = pick (xs, attach (x, extract ys)) 
    | extract xs = xs 

    fun rebuild (x, xs) = (head (#2 x), tail x ++ xs) 
    fun uncons xs = Option.map (rebuild o extract) (List.getItem xs) 
end 

Der Fehler Moskau ML gibt, ist:

File "test.sml", line 47-66, characters 45-631: 
! .............................................:> HEAP_TAIL 
! where type Entry.key = F.Entry.key = 
! struct 
! open F 
! .......... 
! 
! fun rebuild (x, xs) = (head (#2 x), tail x ++ xs) 
! fun uncons xs = Option.map (rebuild o extract) (List.getItem xs) 
! end 
! Signature mismatch: the module does not match the signature ... 
! Scheme mismatch: value identifier uncons 
! is specified with type scheme 
! val 'a' uncons : 
    (int * 'a' tree) list -> ((key * 'a') * (int * 'a' tree) list) option 
! in the signature 
! but its declaration has the unrelated type scheme 
! val uncons : 
    (int * 'a tree) list -> ((key * 'a) * (int * 'a tree) list) option 
! in the module 
! The declared type scheme should be at least as general as the specified type scheme 

ich für uncons mit einer expliziten Typ Unterschrift versucht:

fun 'a uncons (xs : 'a tail) = Option.map (rebuild o extract) (List.getItem xs) 

Aber es macht nur die Fehlermeldung mehr lokalisiert:

File "test.sml", line 65, characters 78-80: 
! fun 'a uncons (xs : 'a tail) = Option.map (rebuild o extract) (List.getItem xs) 
!                    ^^ 
! Type clash: expression of type 
! (int * 'a tree) list 
! cannot have type 
! (int * 'b tree) list 
! because of a scope violation: 
! the type variable 'a is a parameter 
! that is declared within the scope of 'b 

Wenn jemand interessiert ist, hier ist where the snippet originally came from.

Answer 1

Das Problem ist die Verwendung von #1 in Zeile 57. Es handelt sich um einen lokal nicht aufgelösten Datensatztyp. Die SML-Definition besagt, dass "der Programmkontext eindeutig bestimmen muss", wie ein solcher Typ aufgelöst werden soll und ob möglicherweise eine Typannotation erforderlich ist. Leider sagt die Definition nicht aus, wie groß der relevante Programmkontext sein könnte. Keine Implementierung akzeptiert einen willkürlichen großen Kontext, und es wurde kein vollständiger effizienter Algorithmus veröffentlicht, der damit fertig werden könnte, ohne einen Aufzeichnungspolymorphismus einzuführen (und somit zu allgemein zu sein). Nicht spezifisch zu sein wird als (bekannter) Fehler in der Definition betrachtet.

Eine gute Faustregel für was funktioniert über alle Implementierungen ist die kleinste umgebende Deklaration, d. H. In diesem Fall die Definition von ++. Der Typ von #1 kann nicht aus dieser Definition allein bestimmt werden, so dass viele Implementierungen ihn zurückweisen werden, obwohl einige nachsichtiger sind.