functor syntax

[RobertHarper]

Personally I find the syntax for functors disheartening, especially when "sharing" and "where" are used. I never know how to indent, and I never find a way to make it look nice.

I think there is general agreement that the parameter of a functor should be a specification, so that it's a kind of keyword style. SML97 admits that and a positional style, but I think we should just delete the latter entirely. Yes, it rules out F(G(X)), but how often does that come up in practice?

When the realization syntax is so heavy ("where type" instead of "where", and perhaps with "and"), it's all-but-impossible to write things neatly. Lightening the syntax would help, but not solve the problem. Maybe it's not solvable, but it sure would be nice to figure out something cleaner in the common case.

A related point is that I was once an advocate for the :> ascription (well, not that notation, but that concept), but in teaching and in practice I find it to be far more trouble than it's worth. It's easier to confine abstraction to the data types, and use that. (We could even adopt the "newtype" syntax from Haskell for the single-constructor case, but I'm not sure it's a good idea.) Are there any remaining advocates for :>?

[MatthewFluet]

With regards to dropping :> opaque ascription, I'm guessing that you mean for both structures and functors. (Actually, I guess in the language of SML97, functor ascription is just a derived form.) And by "confine abstraction to the data types", I think that you are referring to the fact that if the constructors of a datatype are not exposed by the signature, then the representation is effectively abstract.

One place where opaque ascription is useful is for a compile-time selection from among a number of modules matching the same (large) signature. For example, consider implementing the "default" Int.int type in the Basis Library. I'd like to be able to simply write:

structure Int :> INTEGER = Int32

and know that all clients cannot exploit the equality of Int.int and Int32.int and, therefore, could change the implementation to use Int64 and not break any client code (at least in terms of type checking).

Yes, I could accomplish this with something like:

structure Int : INTEGER =
struct
   structure I = Int32
   datatype int = Int of I.int
   val toString = fn (I i) => I.toString i
   ...
end

but I would actually need to lift every operation one by one.

Another, less compelling, example is with signatures that implement view-like abstractions:

signature TREE =
sig
  type 'a t
  datatype 'a view = Leaf | Node of 'a t * 'a * 'a t
  ...
end

For many trees, the 'a t and 'a view types will be distinct (e.g., a red-black tree, where the color isn't exposed in the view) and not exposing the constructors of 'a t suffice to keep it abstract. But, for the unrestricted binary tree, it is convenient to have:

structure Tree : TREE =
struct
  datatype 'a tree = Leaf | Node of 'a t * 'a * 'a t
  type 'a view = 'a tree
  ...
end

rather than

structure Tree : TREE =
struct
  datatype 'a tree = Tree of 'a view
  and 'a view = Leaf | Node of 'a t * 'a * 'a t
  ...
end

and need to write all of the Tree wrapping/unwrapping.

[JohnReppy]

I would argue in favor of getting rid of translucent ascription and just make ":" mean opaque signature matching. I think that opaque signature matching is much more intuitive (and useful). Translucent matching seems like a hack to make type equalities visible, but you can only understand these by peeking inside the implementation. I think that it is better programming style to make the equalities explicit in the interfaces.

I would also advocate getting rid of "sharing" and adding "where" for structures.

[alleystoughton]

On Apr 7, 2016, at 10:44 AM, John Reppy [email protected] wrote:

I would argue in favor of getting rid of translucent ascription and just make ":" mean opaque signature matching. I think that opaque signature matching is much more intuitive (and useful). Translucent matching seems like a hack to make type equalities visible, but you can only understand these by peeking inside the implementation. I think that it is better programming style to make the equalities explicit in the interfaces.

I wholeheartedly agree. We often don’t want concrete equality to be exported, as in:

signature IS = sig
type t
val empty : t
val sing : int -> t
val union : t * t -> t
val rep : t -> int list
end;

structure IS :> IS = struct
type t = int list

val empty = []

fun sing x = [x]

fun union(xs, ys) = xs @ ys

fun insert(x, nil) = [x]
| insert(x, y_ys as y :: ys) =
case Int.compare(x, y) of
LESS => x :: y_ys
| EQUAL => y_ys
| GREATER => y :: insert(x, ys)

fun rep nil = nil
| rep (x :: xs) = insert(x, rep xs)
end;

val xs = IS.union(IS.union(IS.sing 3, IS.sing 4), IS.sing 3);
val ys = IS.union(IS.sing 4, IS.union(IS.sing 4, IS.sing 3));
val us = IS.rep xs;
val vs = IS.rep ys;

In teaching, I find opaque ascription much easier to explain and motivate: “just look at the signature, that’s exactly what you’ll get”.

[RobertHarper]

Doing so causes you to need way too many sharing specifications or where type’s. I changed my mind on this issue exactly because of teaching (and practicality).

On Apr 7, 2016, at 11:13, Alley Stoughton [email protected] wrote:

On Apr 7, 2016, at 10:44 AM, John Reppy [email protected] wrote:

I would argue in favor of getting rid of translucent ascription and just make ":" mean opaque signature matching. I think that opaque signature matching is much more intuitive (and useful). Translucent matching seems like a hack to make type equalities visible, but you can only understand these by peeking inside the implementation. I think that it is better programming style to make the equalities explicit in the interfaces.

I wholeheartedly agree. We often don’t want concrete equality to be exported, as in:

signature IS = sig
type t
val empty : t
val sing : int -> t
val union : t * t -> t
val rep : t -> int list
end;

structure IS :> IS = struct
type t = int list

val empty = []

fun sing x = [x]

fun union(xs, ys) = xs @ ys

fun insert(x, nil) = [x]
| insert(x, y_ys as y :: ys) =
case Int.compare(x, y) of
LESS => x :: y_ys
| EQUAL => y_ys
| GREATER => y :: insert(x, ys)

fun rep nil = nil
| rep (x :: xs) = insert(x, rep xs)
end;

val xs = IS.union(IS.union(IS.sing 3, IS.sing 4), IS.sing 3);
val ys = IS.union(IS.sing 4, IS.union(IS.sing 4, IS.sing 3));
val us = IS.rep xs;
val vs = IS.rep ys;

In teaching, I find opaque ascription much easier to explain and motivate: “just look at the signature, that’s exactly what you’ll get”.

—
You are receiving this because you authored the thread.
Reply to this email directly or view it on GitHub #8 (comment)

[JohnReppy]

It may depend on programming style. I have not found the where types to be a particular burden in my code or my teaching, but I may not be as strict about using ":>" as I should be. It is somewhat more annoying with MLton than SML/NJ, since SML/NJ has the where-structure feature. Can you point at some example code that illustrates your point?

[RobertHarper]

part of it is that we limit ourselves to where type for compatibility, but more generally it is convenient to have sharing by construction as well as by specification. it’s just too finicky to demand that everything be an abstract type when in fact what you want is a type class. transparent ascriptions implement type classes; opaque ascriptions implement abstract types; you want both. because datatype’s are abstract, i can get away with only type classes, and that is easy to teach. matthew’s remarks are well-taken, so maybe we need to retain opaque ascription, but it would be a disaster to get rid of type classes (rather, to require them to be simulated using abstract types and where type by hand).

bob

On Apr 7, 2016, at 12:32, John Reppy [email protected] wrote:

It may depend on programming style. I have not found the where types to be a particular burden in my code or my teaching, but I may not be as strict about using ":>" as I should be. It is somewhat more annoying with MLton than SML/NJ, since SML/NJ has the where-structure feature. Can you point at some example code that illustrates your point?

—
You are receiving this because you authored the thread.
Reply to this email directly or view it on GitHub #8 (comment)

[alleystoughton]

Hi Bob,

Perhaps I’m being dense, but it didn’t seem like you addressed my point (and example) about how datatypes aren’t abstract enough — often we don’t want to export any kind of equality, or the equality we want isn’t concrete equality. I can see the argument for having both kinds of ascription (even if I almost never use transparent ascription), but can’t see how doing away with opaque ascription can be fully compensated for.

Alley

On Apr 7, 2016, at 3:47 PM, Robert Harper [email protected] wrote:

part of it is that we limit ourselves to where type for compatibility, but more generally it is convenient to have sharing by construction as well as by specification. it’s just too finicky to demand that everything be an abstract type when in fact what you want is a type class. transparent ascriptions implement type classes; opaque ascriptions implement abstract types; you want both. because datatype’s are abstract, i can get away with only type classes, and that is easy to teach. matthew’s remarks are well-taken, so maybe we need to retain opaque ascription, but it would be a disaster to get rid of type classes (rather, to require them to be simulated using abstract types and where type by hand).

bob

On Apr 7, 2016, at 12:32, John Reppy [email protected] wrote:

It may depend on programming style. I have not found the where types to be a particular burden in my code or my teaching, but I may not be as strict about using ":>" as I should be. It is somewhat more annoying with MLton than SML/NJ, since SML/NJ has the where-structure feature. Can you point at some example code that illustrates your point?

—
You are receiving this because you authored the thread.
Reply to this email directly or view it on GitHub #8 (comment)

—
You are receiving this because you commented.
Reply to this email directly or view it on GitHub

[RobertHarper]

My mistake. Yes, you’re right. I wasn’t thinking of it because when we teach ML to freshmen we PROHIBIT any use of equality testing, and any use of Booleans, so equality never comes up at all. The whole business about equality in SML is a mess; it should be replaced by uses of modular type classes.

Bob

On Apr 7, 2016, at 15:55, Alley Stoughton [email protected] wrote:

Hi Bob,

Perhaps I’m being dense, but it didn’t seem like you addressed my point (and example) about how datatypes aren’t abstract enough — often we don’t want to export any kind of equality, or the equality we want isn’t concrete equality. I can see the argument for having both kinds of ascription (even if I almost never use transparent ascription), but can’t see how doing away with opaque ascription can be fully compensated for.

Alley

On Apr 7, 2016, at 3:47 PM, Robert Harper [email protected] wrote:

part of it is that we limit ourselves to where type for compatibility, but more generally it is convenient to have sharing by construction as well as by specification. it’s just too finicky to demand that everything be an abstract type when in fact what you want is a type class. transparent ascriptions implement type classes; opaque ascriptions implement abstract types; you want both. because datatype’s are abstract, i can get away with only type classes, and that is easy to teach. matthew’s remarks are well-taken, so maybe we need to retain opaque ascription, but it would be a disaster to get rid of type classes (rather, to require them to be simulated using abstract types and where type by hand).

bob

On Apr 7, 2016, at 12:32, John Reppy [email protected] wrote:

It may depend on programming style. I have not found the where types to be a particular burden in my code or my teaching, but I may not be as strict about using ":>" as I should be. It is somewhat more annoying with MLton than SML/NJ, since SML/NJ has the where-structure feature. Can you point at some example code that illustrates your point?

—
You are receiving this because you authored the thread.
Reply to this email directly or view it on GitHub #8 (comment)

—
You are receiving this because you commented.
Reply to this email directly or view it on GitHub

—
You are receiving this because you authored the thread.
Reply to this email directly or view it on GitHub #8 (comment)

[rossberg-old]

I also think that :> is preferable to : for its clarity. Moreover, I think that the fact that this often leads to cumbersome where constraints is not a failure of :> itself, but a consequence of the overuse of fibration that is imposed by the language, due to the lack of parameterised signatures.

Let me explain. In practice -- especially in signatures used with :> -- there typically is a rather clear distinction between types that are exports from a module, and those that describe imports. Fibration is the right tool for the former, but not well-suited for the latter.

Take the unavoidable Map functor as an example:

signature MAP = sig type key; type 'a map; ... end
functor Map(Key : ORD) :> MAP where type key = Key.t = ...

Here, the type key clearly will always come from outside the (any) module that implements the signature MAP. It makes no sense to ever pretend that it is an abstract type provided by the module, and you never will want to keep it abstract. In cases like that, fibration is a pointless distraction (and the exponential parameter growth argument from Harper/Pierce moot). Instead of the above, it would be far more natural to write:

signature MAP(type key) = sig type 'a map; ... end
functor Map(Key : ORD) :> MAP(type key = Key.t) = ...

And even that is yet too verbose, I'd want to be able to shorten the clumsy MAP(type key = Key.t) to just MAP(Key.t).

Under such an approach, no normal use of :> would require where annotations; instead, something like MAP(t) is simple and obvious.

[RobertHarper]

In any form of dependent typing a family is a fibration. You are just talking about another syntax for the same thing. The psychology of what it means to be a component is not part of the concept. Any component can function, a posteriori, as an argument, and any argument is implicitly a component. It's very simple and flexible.

Bob

On Apr 9, 2016, at 02:17, Andreas Rossberg [email protected] wrote:

I also think that :> is preferable to : for its clarity. Moreover, I think that the fact that this often leads to cumbersome where constraints is not a failure of :> itself, but a consequence of the overuse of fibration that is imposed by the language, due to the lack of parameterised signatures.

Let me explain. In practice -- especially in signatures used with :> -- there typically is a rather clear distinction between types that are exports from a module, and those that describe imports. Fibration is the right tool for the former, but not well-suited for the latter.

Take the unavoidable Map functor as an example:

signature MAP = sig type key; type 'a map; ... end
functor Map(Key : ORD) :> MAP where type key = Key.t = ...
Here, the type key clearly will always come from outside the (any) module that implements the signature MAP. It makes no sense to ever pretend that it is an abstract type provided by the module, and you never will want to keep it abstract. In cases like that, fibration is a pointless distraction (and the exponential parameter growth argument from Harper/Pierce moot). Instead of the above, it would be far more natural to write:

signature MAP(type key) = sig type 'a map; ... end
functor Map(Key : ORD) :> MAP(type key = Key.t) = ...
And even that is yet too verbose, I'd want to be able to shorten the clumsy MAP(type key = Key.t) to just MAP(Key.t).

Under such an approach, no normal use of :> would require where annotations; instead, something like MAP(t) is simple and obvious.

—
You are receiving this because you authored the thread.
Reply to this email directly or view it on GitHub #8 (comment)

[rossberg-old]

Sure, but as always, syntax matters, and it's the very subject of this issue :). The abstract conceptual equivalence simply isn't accessible in the concrete language right now.

[RobertHarper]

But it’s a positive disadvantage to commit in advance to what is a “paremeter” and what is a “result”. The whole beauty of the pullback notation is that it avoids pre-commitment.

I think it’s a matter of psychology, really. People are trained to expect some sort of function-style parameterization mechanism. That’s not what we have. So what? They also expect “methods” and “classes” and “instances” and whatnot. We don’t give them that either.

Bob

On Apr 10, 2016, at 04:32, Andreas Rossberg [email protected] wrote:

Sure, but as always, syntax matters. This abstract conceptual equivalence simply isn't accessible in the concrete language right now.

—
You are receiving this because you authored the thread.
Reply to this email directly or view it on GitHub #8 (comment)

[rossberg-old]

But it’s a positive disadvantage to commit in advance to what is a “paremeter” and what is a “result”. The whole beauty of the pullback notation is that it avoids pre-commitment.

I am with you regarding the theoretical beauty, but in the vast majority of practical cases, the advantage is purely hypothetical, and diminished by the disadvantage of a cumbersome notation. Adequate sugar would be a remedy.

I think it’s a matter of psychology, really. People are trained to expect some sort of function-style parameterization mechanism. That’s not what we have. So what? They also expect “methods” and “classes” and “instances” and whatnot. We don’t give them that either.

Well, in a language where every other abstraction mechanism is via function-style parameterisation they are kind of right to expect this, wouldn’t you agree? Either way, we can’t deny that it increases the barrier to entry.

The argument for more conceptual generality would be more compelling if we applied it to other cases as well. The irony is that if you carry that through (like MixML did, for example), then you end up with something that is much closer to an object-oriented language. And indeed, the mechanism fits the expectations from that world more naturally, where it is close to the notion of refinement through mixin composition.

[RobertHarper]

yep, except that dave's formulation predated that stuff by decades. i would say that his setup inspired the (bad imo) mixin ideas.

On Apr 16, 2016, at 13:47, Andreas Rossberg [email protected] wrote:

But it’s a positive disadvantage to commit in advance to what is a “paremeter” and what is a “result”. The whole beauty of the pullback notation is that it avoids pre-commitment.

I am with you regarding the theoretical beauty, but in the vast majority of practical cases, the advantage is purely hypothetical, and diminished by the disadvantage of a cumbersome notation. Adequate sugar would be a remedy.

I think it’s a matter of psychology, really. People are trained to expect some sort of function-style parameterization mechanism. That’s not what we have. So what? They also expect “methods” and “classes” and “instances” and whatnot. We don’t give them that either.

Well, in a language where every other abstraction mechanism is via function-style parameterisation they are kind of right to expect this, wouldn’t you agree? Either way, we can’t deny that it increases the barrier to entry.

The argument for more conceptual generality would be more compelling if we applied it to other cases as well. The irony is that if you carry that through (like MixML did, for example), then you end up with something that is much closer to an object-oriented language. And indeed, the mechanism fits the expectations from that world more naturally, where it is close to the notion of refinement through mixin composition.

—
You are receiving this because you authored the thread.
Reply to this email directly or view it on GitHub

[YawarRaza7349]

I like the parameterized signatures thing due to the UX principle of affordances and constraints. But it seems like @rossberg wants the shorter syntax, while @RobertHarper doesn't want to restrict the functionality of signatures. So why not just make parentheses syntactic sugar for where to satisfy both concerns?

signature MAP = sig
  type key
  (* ... *)
end

functor Map(Key : ORD) :> Map(type key = Key.t) = (* ... *)

I don't really know Rust, so this stuff might be wrong [click to expand].

FWIW, Rust uses the syntax Map<K = Key::T> for its version of where type (for "associated types"). Interestingly, though, it also has a version of parameterized signatures ("generic traits", which accept types rather than general modules), also using angle brackets. The former is for associated types for typeclasses (as in Modular Type Class's Section 2.5), while the latter is used to produce typeclasses (so Into<bool> would be like overload into from (INTO where type target = bool)).

But it’s a positive disadvantage to commit in advance to what is a “paremeter” and what is a “result”. The whole beauty of the pullback notation is that it avoids pre-commitment.

I think you could do something like:

sig
  type k
  include MAP(type key = k)
end

In order to recover the "result" interpretation.

I would argue in favor of getting rid of translucent [sic] ascription and just make ":" mean opaque signature matching.

I'm not a fan of transparent ascription, but one elegant thing about : meaning transparent ascription is that functor parameter annotations (which also use :) behave like transparent ascription, not opaque ascription:

functor Map (Key : ORD) = (* Map body *)
structure IntMap = Map (IntOrd)

The IntMap above is equivalent to:

structure IntMap = let
  structure Key : ORD = IntOrd (* transparent ascription *)
  in (* Map body *)
end

Since newtype was mentioned in the opening message, I'd like to point out that the entire reason Haskell has the newtype keyword is due to its non-strict semantics: case DataCtor undefined of { DataCtor _ -> 2024 } needs to evaluate to 2024, so DataCtor can't be optimized out. newtype exists so the programmer can opt in to the optimization, accepting the different semantics that cases like the example I gave above have. Since SML is strict, said optimization doesn't change the semantics anyway, so newtype doesn't serve any purpose for SML. Doesn't mean it was a mistake for Haskell (any more than non-strictness was, anyway).