language-lawyer - 根据定义，这个片段是否合法标准 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

如果有人感兴趣，这里是where the snippet originally came from .

Answer 1

问题出在第57行中#1的使用。它涉及到一个本地未解析的记录类型。 SML 定义说“程序上下文必须唯一地确定”如何解析这样的类型并且可能需要类型注释。不幸的是，该定义并未说明相关程序上下文可能有多大。没有实现接受任意大上下文，并且没有发布可以处理该问题的完整有效算法，除非引入记录多态性(因此过于笼统)。因此，不更具体被认为是定义中的(已知)错误。

适用于所有实现的一个好的经验法则是最小的周围声明，即在本例中为 ++ 的定义。 #1 的类型不能仅根据该定义来确定，因此许多实现将拒绝它，即使有些更宽松。