Signature members

[nilern]

It should be possible to nest signature declarations inside structures and specifications inside signatures. The OCaml Map module is just one example where this is quite natural compared to the toplevel pollution in the SML/NJ library with ORD_KEY and ORD_MAP.

Abstract signatures make module type checking undecidable, so those should not be added.

[YawarRaza7349]

When you write "abstract signatures [...] should not be added", I think you mean to ban something like:

struct
  signature I = sig type t end
  structure T = struct type t = int end
end :> sig
  signature I (* abstract signature *)
  structure T : I
end

But what if I write:

struct
  signature I = sig type t end
  structure T = struct type t = int end
end :> sig
  signature I = sig end (* signature subtyping *)
  structure T : I
end

Which seems like the same thing to me. Maybe you want to mandate that signature declarations match specifications exactly, rather than allowing subtyping. Or maybe you want to ban structure specifications in a sig from having signatures declared in the same sig. Is there a specific framework you had in mind, like from a paper, that's already dealt with this stuff?

[rossberg]

Since signatures can be used in both co- and contra-variant position, allowing subtyping on signature equations would be unsound.

The closest you could do is bounded abstract signatures:

struct
  signature I = sig type t end
  structure T = struct type t = in end
end :>
sig
  signature I < sig end
  structure T : I
end

But when using this in functor parameters, that would give rise to something at least as expressive as bounded quantification as in F-omega-sub with full forall-subtyping, which we also know is undecidable.

[dmacqueen]

All these examples in this discussion seem to me to be trying to stretch the existing SML module system design beyond its breaking point. Better to start over from scratch with a well-thought-out and coherent underlying model (but not just F_omega!).

The other problem is “exceeding the conceptual complexity bound” for a reasonable pragmatic programming language, where the “pragmatic, programmer’s model or semantics” has to be kept fairly simple. It is all too easy to get into the weeds and make the type/module system complex beyond (average) programmer’s comprehension. It should be possible to teach the entire language in an introductory programming course based on the language. I have verified that this is certainly not the case for, e.g. Haskell (and I assume the same is true of C++). Dynamic languages (such as Python), avoid the issue by leaving their implicit type system out of the design! Sometimes someone comes along later and tries to fix that, e.g. typescript.

Sometime, probably later this year, I plan to launch a “heavy” project to reimplement (and probably partly redesign) the SML type + module system in SML/NJ (or a branch thereof). Kibitzers welcome. Watch for it in github.com/smlnj http://github.com/smlnj and standardml.zulipchat.com http://standardml.zulipchat.com/. I will take into account these Successor-ML discussions.

Dave

On Feb 16, 2024, at 4:07 AM, Andreas Rossberg @.***> wrote:

Since signatures can be used in both co- and contra-variant position, allowing subtyping on signature equations would be unsound.

The closest you could do is bounded abstract signatures:

struct signature I = sig type t end structure T = struct type t = in end end :> sig signature I < sig end structure T : I end But when using this in functor parameters, that would give rise to something at least as expressive as bounded quantification as in F-omega-sub with full forall-subtyping, which we also know is undecidable.

— Reply to this email directly, view it on GitHub https://github.com/SMLFamily/Successor-ML/issues/39#issuecomment-1948271432, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAGXNPMOJD6T35YRSFCMF4LYT5DW5AVCNFSM4H7MP662U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJUHAZDOMJUGMZA. You are receiving this because you are subscribed to this thread.

David MacQueen @.***