3

根据定义，下面给出的代码片段是否合法标准 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

莫斯科 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

如果有人感兴趣，这里是片段最初来自的地方。

4

1 回答 1

4

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

一个适用于所有实现的好的经验法则是最小的周围声明，即在这种情况下是++. 的类型#1不能仅从该定义中确定，因此许多实现会拒绝它，即使有些更宽松。

于 2016-06-25T16:32:10.677 回答