Discussion for proposal 2020-001 (Addition of the Universal module)

[JohnReppy]

No description provided.

[JohnReppy]

This issue is for discussion of proposal 2020-001 (Addition of the Universal module).

[MatthewFluet]

In addition to a structure Universal : UNIVERSAL, perhaps it would be useful to have a functor MkUniversal() :> UNIVERSAL.

Just as it can be awkward to use the single exn type for all of one's universal type needs, it could be awkward to use the single Universal.universal type.

Also, as noted in the proposal, native compiler support might enable more efficient implementations. This might extend to more efficiently supporting separate universal types.

In any case, functor MkUniversal() :> UNIVERSAL = Universal would suffice as a default implementation.

[RobertHarper]

I am not sure I agree with this proposal. It does, after all, describe exactly what the exn type provides, bearing in mind that “exn” means “extensible”. I don’t really understand the worry about “us[ing] the single exn type for all one’s universal type needs.” The language supports data abstraction, so of course anyone can define their own interface and seal it, implementing it as exn, but programming against their own interface. Given that, I am not sure why we would want to pick the “standard” interface to it, but we could do that if we’d like, simply because it hides the need to use the misnamed “exception” declaration (should be “extension” declaration). Also, I don’t see the need for a functor, could someone explain that to me? There is only one extensible type, and I can use that one type “at the same time” as the implementation of several abstract types. The “generative” nature of extensions means that they cannot be confused; there is only one shared state underlying the generation. I would suggest not to call it “universal”, but instead, say, Extensible. (In Java it’s called Object, but I’d prefer we not use that terminology!) Bob

…

On Apr 23, 2020, at 18:37, Matthew Fluet ***@***.***> wrote: In addition to a structure Universal : UNIVERSAL, perhaps it would be useful to have a functor MkUniversal() :> UNIVERSAL. Just as it can be awkward to use the single exn type for all of one's universal type needs, it could be awkward to use the single Universal.universal type. Also, as noted in the proposal, native compiler support might enable more efficient implementations. This might extend to more efficiently supporting separate universal types. In any case, functor MkUniversal() :> UNIVERSAL = Universal would suffice as a default implementation. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#27 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AALWY5M542UMFSQDRCLNVDDROC7KLANCNFSM4MORGLYA>.

[JohnReppy]

The arguments in favor of the Universal module are that it is more convenient to program with than using dynamic exceptions and that an implementation could provide a more efficient implementation than one gets from exceptions.

The name was chosen because "Universal" is what Poly/ML calls it. Since a subgoal is to make it easier to port code across implementations, so preserving the existing name is beneficial.

[dmacqueen]

I, and various other people I assume, have contemplated the idea of generalizing the exn primitive type by allowing new such “open” datatypes to be declared. Each of these exn-like types would be nullary primitive types and in the scope of their declaration there could be associated data constructor declarations, analogous to the “exception” declarations. I don’t remember how far I worked out the implementation details, but it seems obvious that they should be able to share the existing machinery (or techniques, at least) for the exn type and its constructors. This would provide another alternative to the Universal structure. My way of thinking of these is as “open tagged unions”, a limited and tamer variant on dynamic types where the component/variant type serves as the tag. Dave

On Apr 23, 2020, at 4:28 PM, John Reppy ***@***.***> wrote: The arguments in favor of the Universal module are that it is more convenient to program with than using dynamic exceptions and that an implementation could provide a more efficient implementation than one gets from exceptions. The name was chosen because "Universal" is what Poly/ML calls it. Since a subgoal is to make it easier to port code across implementations, so preserving the existing name is beneficial. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#27 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAGXNPKLDRG4QQIEHHMSE4DRODFJZANCNFSM4MORGLYA>.

David MacQueen [email protected]

[ratmice]

Something always bothers me about these sorts of structures, which is the completeness of it,
If one can call tagProject, one can also call tagInject, Similar in a way to exception in that currently there isn't a mechanism for having a destructurable/handled execption which cannot then be rethrown again.

Any opinions on adding another subTag or equivalent type to the module which allows projection but not injection?

type 'a subTag

val derive_subtag: 'a tag -> 'a subTag;
val subtagIs: 'a subTag -> universal -> bool
val subtagProject: 'a subTag -> universal -> 'a 

Such that then given a subtag, one only has the right types to project out of a universal, without necessarily being able to project into them.

Edit: Not that i'm smitten with the name subTag, perhaps a better name might be weak_tag?
Edit: I'm not sure it's obvious what I intend 'a subTag to be here, essentially an opaque alias for 'a tag.

so we'd have

sig
type 'a tag;
type 'a subTag;
...
end

and

struct
type 'a tag = ...
type 'a subTag = 'a tag;
...

So derive_subtag is the identity function, and subtagIs and subtagProject are just their tag* variations with on a type with no inject.

[dmacqueen]

Why not just provide/use a signature-coerced version of the module that omits the tagInject function? Dave

On Apr 23, 2020, at 4:48 PM, matt rice ***@***.***> wrote: Something always bothers me about these sorts of structures, which is the completeness of it, If one can call tagProject, one can also call tagInject, Similar in a way to exception in that currently there isn't a mechanism for having a destructurable/handled execption which cannot then be rethrown again. Any opinions on adding another subTag or equivalent type to the module which allows projection but not injection? type 'a subTag val derive_subtag: 'a tag -> 'a subTag; val subtagIs: 'a subTag -> universal -> bool val subtagProject: 'a subTag -> universal -> 'a Such that then given a subtag, one only has the right types to project out of a universal, without necessarily being able to project into them. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#27 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAGXNPL72XCTZNEDJBVKAMTRODHTRANCNFSM4MORGLYA>.

David MacQueen [email protected]

[ratmice]

@dmacqueen that would work too, is there any interest/objections in including a signature as such?

Or is it something one is expected to know can be done and declare the signature separately in their own program using via structural subtyping?

The only real reason I did it in addition rather than as a structural subtype, is because reading the types, one gets implication that both are available and one is weaker than the other. I wouldn't think there is another difference.

So, to try that mechanism instead it'd be something like:
signature WEAK_UNIVERSAL

type universal

type 'a tag

val tag : unit -> 'a tag
val tagIs : 'a tag -> universal -> bool
val tagProject : 'a tag -> universal -> 'a

we could then perhaps add a function to UNIVERSAL, and Weak structure?

structure WeakUniversal: WEAK_UNIVERSAL
val weaken: universal -> WeakUniversal.universal
val weaken_tag: 'a tag -> 'a WeakUniversal.tag

That would preserve the discoverability aspect of it?
Edit: I guess rather than theabove what you were thinking was more like functor WeakenUniversal(it:UNIVERSAL) : WEAK_UNIVERSAL?

[YawarRaza7349]

@ratmice, in your second comment, you created a type WeakUniversal.universe distinct from universe. But in your first comment, subTags are used on the original universe type instead, which is the correct approach. So this is what the functor you mention in your last edit should look like:

functor ViewTags (U : UNIVERSAL) :> sig
  type 'a tag
  val viewTagOf : 'a U.tag -> 'a tag
  val tagIs : 'a tag -> U.universal -> bool
  val tagProject : 'a tag -> U.universal -> 'a
end

And why not also provide the dual notion?:

functor CreationTags (U : UNIVERSAL) :> sig
  type 'a tag
  val creationTagOf : 'a U.tag -> 'a tag
  val tagInject : 'a tag -> 'a -> U.universal
end