More convenient opaque ascription

[eduardoleon]

Opaque ascription is a very useful feature, but one of its downsides is that selectively making types abstract in a large structure is very verbose. For example:

functor MakeQux (FB : FOO_BAR) :> QUX
  where type FB.foo = FB.foo
    and type FB.bar = FB.bar =
struct
  structure FB = FB

  type 'a qux = 'a bar foo list

  (* operations go here *)
end

I wish I could do the following instead:

functor MakeQux (FB : FOO_BAR) : QUX =
struct
  structure FB = FB

  (* locally a synonym, externally an abstract type *)
  newtype 'a qux = 'a bar foo list

  (* operations go here, unchanged *)
end

I propose the keywords newtype and neweqtype, which define a type with the following properties:

• Inside the current structure, it's a type synonym.
• Outside of the current structure, it's an abstract type or eqtype.

[MatthewFluet]

I suppose I see what you are getting at, but I expect that "current structure" would be limiting. For example, what should happen with:

functor MakeFooBarQux (FB: FOO_BAR) : FOO_BAR_QUX =
struct
  structure Foo = FB.Foo
  structure Bar = FB.Bar
  structure Qux =
   struct
     newtype 'a qux = 'a Bar.bar Foo.foo list
   end
  (* operations go here *)
end

Do the operations outside of structure Qux see the definition?

[eduardoleon]

Do the operations outside of structure Qux see the definition?

Sadly, no. In this case, you'd have to use normal opaque ascription, unless my proposal were modified to allow the user to control the level of structure nesting at which the type synonym is made abstract.

In practice, I don't think I ever introduce new abstract types in nested modules, but of course I can't speak for anyone else.

[eduardoleon]

Here's a slight generalization. In most likelihood, it still doesn't cover every case, but it covers the particular example you gave:

functor MakeFooBarQux (FB: FOO_BAR) : FOO_BAR_QUX =
struct
  structure Foo = FB.Foo
  structure Bar = FB.Bar
  newstructure Qux : QUX =
   struct
     (* not a newtype! *)
     type 'a qux = 'a Bar.bar Foo.foo list
   end
  (* operations go here, 'a Qux.qux is a synonym here *)
end
structure FBQ = MakeFooBarQux (...)
(* 'a FBQ.Qux.qux is an abstract type here *)

The meaning of newstructure Struct : SIG = ... is as follows:

• Within the current structure, Struct is transparently ascribed the signature SIG.
• Outside of the current structure, Struct is opaquely ascribed the signature SIG.

[MatthewFluet]

I think that this is approaching the problem in the wrong direction (and, to be honest, I don't actually think there is a significant problem). It seems to me a better solution would be to adjust the signature language with a mechanism to indicate that, when used in a transparent ascription, a particular type should not be revealed:

functor MakeQux (FB : FOO_BAR) : QUX hiding type qux =
struct
  structure FB = FB

  type 'a qux = 'a bar foo list

  (* operations go here *)
end

But, I'm not really sure if something like this fits well with elaboration of the signature language, because one wants to elaborate QUX hiding type qux independently of its use in an ascription and then it isn't clear to me what the elaborated representation would be.

And, there are mechanisms in SML that get you nearly there:

functor MakeQux (FB : FOO_BAR) : QUX =
struct
  structure FB = FB

  datatype 'a qux = Qux of 'a bar foo list

  (* operations go here *)
end

Note that by not exporting the Qux data constructor, the type 'a qux is effectively opaque -- although clients may "know" the definition, they cannot exploit it in any way to create or destruct an 'a qux.

[eduardoleon]

This isn't completely satisfactory. Here's a(n admittedly contrived) example:

signature QUX =
sig
  structure FB : FOO_BAR
  type 'a qux
  val unwrap : 'a qux list -> 'a FB.bar FB.foo list list
end

functor MakeQux (FB : FOO_BAR) : QUX =
struct
  structure FB = FB
  newtype 'a qux = 'a FB.bar FB.foo list
  fun unwrap x = x  (* no-op! *)
end

functor MakeQux' (FB : FOO_BAR) : QUX =
struct
  structure FB = FB
  datatype 'a qux = Qux of 'a FB.bar FB.foo list
  fun unwrap xs = map (fn Qux x => x) xs  (* O(n) *)
end

Using your datatype trick would require unwrap to be an O(n) operation.

[JohnReppy]

I don't understand why there would be a difference in performance between new type and hiding in this example? Are they not both essentially syntactic sugar for opaque signature matching?

[eduardoleon]

You are right, but in my last example I was comparing new type (or hiding, whichever syntax is deemed better) against wrapping “moral synonyms” in datatype constructors.

[RobertHarper]

“hiding” would be handy, as would be other operations on signatures previously proposed.

“newtype” is to me pointless, a carryover of a mistake in haskell. either use ascription, perhaps with hiding to make it more convenient, or use a datatype, which provides an abstract type.

btw, my proposal regarding data types and modules really should be fleshed out and adopted, it’s the right idea. to refresh your memories, one would have the concept of a data signature, which is more or less a datatype spec with a nicer syntax that fits better with modules, and the concept of a default implementation of a data signature, written “data structure S : SIG”, where SIG is a data signature. (don’t you just love that syntax? and it avoids the stupid replication problem we’ve had forever.)

bob

(c) Robert Harper All Rights Reserved.

On May 3, 2017, at 17:09, eduardoleon notifications@github.com wrote:

You are right, but in my last example I was comparing new type (or hiding, whichever syntax is deemed better) against wrapping “moral synonyms” in datatype constructors.

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

[eduardoleon]

@RobertHarper Please note that while my proposal is called new type, its semantics is completely different from Haskell's newtype. (I agree that the latter is a bad idea.) My new type proposal is syntactic sugar for selective opaque ascription.

[RobertHarper]

But then I would say that information does not belong on the structure, but the signature. The “hiding” proposal seems more reasonable to me.

Bob

(c) Robert Harper All Rights Reserved.

On May 4, 2017, at 00:27, eduardoleon notifications@github.com wrote:

@RobertHarper https://github.com/RobertHarper Please note that while my proposal is called new type, its semantics is completely different from Haskell's newtype. (I agree that the latter is a bad idea.) My new type proposal is syntactic sugar for selective opaque ascription.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/SMLFamily/Successor-ML/issues/27#issuecomment-299094609, or mute the thread https://github.com/notifications/unsubscribe-auth/ABdsdY1T0QYOE2hEWHa4tSgb2uZV70_Uks5r2VPBgaJpZM4J9jg8.

[YawarRaza7349]

But, I'm not really sure if something like this fits well with elaboration of the signature language, because one wants to elaborate QUX hiding type qux independently of its use in an ascription and then it isn't clear to me what the elaborated representation would be.

That's because we think of type specs as having two "states": unrefined (type t) and refined (type t = int). But here, we should think of them as having three states, with a separate "abstract" state. We then see that opaque ascription implicitly converts all unrefined types into the abstract state before applying the signature to the structure, while transparent ascription implicitly refines all unrefined types to whatever type is bound to them in the structure. In this formulation, we can think of hiding as converting a particular (unrefined) type spec into the abstract state. Note that currently in SML, a type spec can only be in the abstract state as it is being ascribed to a structure, while hiding adds the ability for a type spec to be in the abstract state while it is bound to a signature variable.

This all brings up something that's always bugged me: Why do we assume that a programmer will want the unrefined types in a signature to be all abstract or all concrete? What connection do different types in a signature have with each other? Shouldn't they all be independent?

If hiding is added to the language, there should also be a way to put a type in the abstract state directly in a signature, something like type t = abstract or abstract type t (I'd personally prefer to pull a C++ auto and repurpose abstype since it's already reserved, but IDK if the 1±2 people who still used abstype would find that "confusing"; then we wouldn't need the hiding keyword either since we could just use this repurposed abstype with where).

The above paragraphs are the real point I'm trying to make. This section just talks about an unrelated unpopular opinion I have related to something else mentioned in this discussion. [click to expand]

FWIW, @eduardoleon's `newtype` proposal is actually pretty close to fitting in with one of my favorite underrated SML features: `local`. I've always kinda wished `type` decls in a `local` block were made abstract outside the `local`, but I understand that its actual behavior is more consistent. Still, one could imagine something like `localtype t = int in (* t = int here *) end (* t abstract here *)`, which is close to the proposed `newtype`, except that the scope of the exposed type equality is more explicit. The reason I've wanted this functionality is that, with something like `localtype`, all functionality of signatures (that I can think of) each has another feature that provides it: name hiding has `local`, type abstraction has `localtype`, and type narrowing (monomorphization) has type annotations directly on the `val`. Which is great because I hate the redundancy of signatures (not saying I would never use them, but I want the option to use less verbose options in smaller contexts).