Является ли этот фрагмент законным стандартом ML в соответствии с определением?

Question

Является ли приведенный ниже фрагмент кода законным стандартом ML в соответствии с определением? Проверяет тип с Poly/ML, но не с 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

Ошибка Moscow ML дает:

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

Я пытался использовать явную подпись типа для uncons:

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

Но это просто делает сообщение об ошибке более локализованным:

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

Если кому-то интересно, вот откуда взялся этот фрагмент.

Answer 1

Проблема заключается в использовании #1 в строке 57. Он включает локально неразрешенный тип записи. Определение SML говорит, что "программный контекст должен однозначно определять", как разрешить такой тип, и что может потребоваться аннотация типа. К сожалению, определение не говорит о том, насколько большим может быть соответствующий контекст программы. Ни одна реализация не принимает произвольно большой контекст, и не было опубликовано ни одного полного эффективного алгоритма, который мог бы справиться с этим, за исключением введения полиморфизма записей (и, следовательно, слишком общего). Таким образом, отсутствие уточнения считается (известной) ошибкой в ​​определении.

Хорошее практическое правило для того, что работает во всех реализациях, - это наименьшее окружающее объявление, т. Е. В этом случае определение ++, Тип #1 не может быть определено только из этого определения, поэтому многие реализации отклонят его, хотя некоторые из них более снисходительны.