Is the code snippet given below legal Standard ML according to the Definition? It type-checks with Poly/ML, but not with Moscow 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
The error Moscow ML gives is:
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
I tried using an explicit type signature for uncons:
fun 'a uncons (xs : 'a tail) = Option.map (rebuild o extract) (List.getItem xs)
But it merely makes the error message more localized:
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
If anyone's interested, here's where the snippet originally came from.
The problem is the use of #1 in line 57. It involves a locally unresolved record type. The SML definition says that "the program context must uniquely determine" how to resolve such a type and that a type annotation may be required. Unfortunately, the definition doesn't say how large the relevant program context may be. No implementation accepts an arbitrary large context, and no complete efficient algorithm has been published that could handle that, short of introducing record polymorphism (and thus being too general). So not being more specific is considered a (known) bug in the definition.
A good rule of thumb for what works across all implementations is the smallest surrounding declaration, i.e., in this case the definition of ++. The type of #1 cannot be determined from that definition alone, so many implementations will reject it even though some are more lenient.