Type identity and grouping operations for implicits

[JanBeh]

I have a remark on implicits, referring to the paper Syntactic Implicit Parameters with Static Overloading.

As I already said last year in thread #777, I love this approach. I do have a possible concern however.

Specifically I would like to have a look at "Grouping Operations" as discussed in Section 4.2 of your paper, and as also discussed in the other thread (777), and comparing it to some aspects of OCaml's module system, specifically signatures.

What I love both about Koka's implicits and also about OCaml's signatures is that they avoid "interface identities". In OCaml, two equally defined OCaml signatures are indistinguishable:

(* OCaml *)

module type Num = sig
  type t
  val add : t -> t -> t
  val mul : t -> t -> t
end
module type Num2 = sig
  type t
  val add : t -> t -> t
  val mul : t -> t -> t
end

Say Num and Num2 are defined by entirely different libraries. Then it's still possible to use these two interfaces interchangeably. Similiarly, using implicits in Koka, two different libraries could demand the same interface without needing to depend on each other or a common dependency. Consider:

// Library #1

fun fadd( x : a, y : a, z : a, ?(+) : ((a, a) -> a), ?(*) : ((a, a) -> a) ) : a
  x + (y * z)

// Library #2

fun foo( x : a, y : a, z : a, ?(+) : ((a, a) -> a), ?(*) : ((a, a) -> a) ) : a
  x + (y * y * z)

// Library #3

fun main ()
  println(fadd(1, 2, 3))
  println(foo(1, 2, 3))

Here Koka library 1 and Koka library 2 both provide functions (fadd and foo) that operate on numbers that have an addition and multiplication. These two libraries don't need to know about one another, and if they use the same nomenclature, they are automatically compatible.

But things change when we group operations:

// Library #1

struct num<a>
  (+): (a, a) -> a
  (*): (a, a) -> a

val int/num : num<int> = Num( (+), (*) )

fun fadd( x : a, y : a, z : a, .?num : num<a> ) : a
  x + (y * z)

// Library #2

// This library provides its own type, here "number":
struct number<a>
  (+): (a, a) -> a
  (*): (a, a) -> a

fun foo( x : a, y : a, z : a, .?number : number<a> ) : a
  x + (y * y * z)

// Library #3

// This does not work:
val int/number = int/num
// Instead we need:
// val int/number : number<int> = Number( int/num.(+), int/num.(*) )

fun main ()
  println(foo(1, 2, 3))

Even disregarding the different naming, int/num and int/number are not compatible, because they are different types. I see this as an unwanted property, arising from using (or abusing?) types to group implicits, because types have an identity.

Compare with OCaml, where this problem doesn't occur:

(* Library #1 *)

module type Num = sig
  type t
  val add : t -> t -> t
  val mul : t -> t -> t
end

module IntNum = struct
  type t = int
  let add x y = x + y
  let mul x y = x * y
end

module Fadd (Num : Num) = struct
  let fadd x y z = Num.add x (Num.mul y z)
end

(* Library #2 *)

module type Number = sig
  type t = int
  val add : t -> t -> t
  val mul : t -> t -> t
end

module Foo (Number : Number) = struct
  let foo x y z = Number.add x (Number.mul (Number.mul y y) z)
end

(* Library #3 *)

(* Note we can use "Foo" from library #2 and "IntNum" from library #1. *)
module M = Foo (IntNum)
let _ =
  print_endline (string_of_int (M.foo 1 2 3))

I wonder if it is worth considering adding a dedicated language construct to group implicits to avoid the issue in Koka, and I'm curious about your assessment of this issue.

[TimWhiting]

This really is about two different things:

• Structural and nominal typing: structural would treat similar / identical structured types as identical (this is completely separate from implicits and affects the rest of the type system. There are pros and cons, but it is a major change.
• Improving / understanding how to use implicits for this kind of use case.

I think it is pretty clear what the first issue is about, but I want to address the second.

Structures are easy to derive, you don't have to derive them manually for each implementation. This helps avoid the issue you mention entirely.

struct num<a>
  (+): (a, a) -> a
  (*): (a, a) -> a

fun any/num(?(+): (a, a) -> a, ?(*): (a, a) -> a): num<a>
  Num((+), (*))

fun fadd( x : a, y : a, z : a, .?num : num<a> ) : a
  x + (y * z)

// Library #2

// This library provides its own type, here "number":
struct number<a>
  (+): (a, a) -> a
  (*): (a, a) -> a

fun any/number(?(+): (a, a) -> a, ?(*): (a, a) -> a): number<a>
  Number((+), (*))

fun foo( x : a, y : a, z : a, .?number : number<a> ) : a
  x + (y * y * z)

// Library #3

fun main ()
  println(foo(1, 2, 3) + fadd(1, 2, 3)) // mix

Additionally you can even "abstract" over names / signatures that you don't even provide in your own module.

fun foo(x: a, y: a, z: a, ?fadd: (a, a, a) -> a): a
  fadd(x, y, z)

[TimWhiting]

Yes, this fits nicely into the loose grouping / naming aspect of implicits in Koka (and the fact that really for implicits we are using namespaces), and has been discussed. We definitely know there are still use cases that we need to improve for implicits. But also, I'm not saying that modules are incompatible with Koka, but just that they might be less needed, or maybe something else needs to fill in the gap.

[JanBeh]

Headsup: I'm not sure if I understand Koka well enough to not mix up some things here, but I hope I got everything right at this point. It wasn't as easy for me though to follow up on everything said.

Thanks for bringing the naming / compatibililty up. It is something that we failed to cover earlier, and only contains a small mention in the paper. In Koka just like OCaml the names of the operations matter. For something like include Stdlib.Float you can name a base: float-interface in a struct. This will automatically be unpacked when using the .? syntax - bringing the names from your struct and all recursive 'base' interfaces into scope.

Would you mind giving a short example on syntax? I am not following what you mean.

The only time you need to be explicit is if there is more than one implementation for a specific type. Koka will figure out long chains of implicits guided by both name and type.

Well yes, when writing this response, I almost forgot that multiple implementations are fine as long as they apply to different types.

[…], or use the newtype pattern. I think this is a useful requirement, and you might want to be explicit in some cases and to use newtypes for a different cases.

I am personally not too fond of the newtype pattern. I see some use-cases where I would like to use it (say turn an integer into a file-descriptor, for example), but I also believe (I may be wrong or change my opinion) that in many cases it is a work-around for a deficiency in the polymorphism implementation or function dispatch.

I would even go as far to say that the term "newtype" usually refers to exactly that workaround. Is wrapping an integer in a file-descriptor type really a newtype pattern? Maybe it is, but I usually use the term more for wrapping a type with the intent to have other typeclasses/traits apply.

In OCaml I can create a new type (or a new abstract type) when I want to make sure that type is on purpose incompatible with the inner type used for storing the data. I would never do that for changing dispatch, as OCaml simply doesn't dispatch based on the type (with a few exceptions regarding record fields and constructors, for example).

When in other languages a new wrapping type is used to dispatch operations instead of describing a different semantic for the stored data, I think it's not a good pattern in many cases. For example, when I simply want to use a "sort" function in reverse order, do I really want to wrap ints in a reverse-int type (which has a reversed ordering), sort a list of them, and then extract an integer from each newtype-wrapped datum? I don't think it's a good idea.

On the other hand, if I create a new wrapping type to distinguish file descriptors from semantic-less integers, I could be annoyed if sorting fails because the type has changed and my newtype isn't Ord anymore. I have seen so many "pass-through" implementations of traits in Rust. A lot of boilerplate.

However to differentiate between z/semi and zmod/semi I would probably use a newtype, since I never want to mix the two. I'm working in a different domain space. Though a naming change to modular-semigroup / mod-plus could also help here.

Yes, maybe that example is a case where newtype might make sense, but also because it effectively affects the meaning of each value (and the domain space as you say).

In that matter, OCaml has caught my attention because it seems to come with very powerful mechanics to provide abstraction without creating formal dependencies. Even the standard library in OCaml defines some signatures redundantly (see Stdlib.Set.OrderedType and Stdlib.Map.OrderedType, for example) edit: while maintaining interoperability.

I know this is a simple example, but this doesn't really require a grouping, and the naming and types still have to match in OCaml which makes this more of a convention like it is in Koka (unless you do the adaptor mentioned). So in both languages you have convention + adaptors.

Yes, but even if both Koka and OCaml have "convention + adaptors", I still believe there is a difference. When newtypes are involved (only relevant for Koka, as OCaml doesn't do dispatch based on types), you will have to wrap and unwrap values later when using the polymorphic code (unless you wrap every function and make the function wrappers perform the wrapping/unwrapping). When no newtypes are involved, OCaml and Koka are still different. In OCaml, if the convention doesn't match, I can create an adaptor (a module) that fits a certain interface (a module type or signature) without needing to add any dependency to where the interface is defined. In Koka, I can either create a wrapper module or also a wrapper struct, each with the limitations as previously discussed.

I'm not claiming that it doesn't come at a price. Just that the price in practice doesn't seem to be as large as it seems at first glance (I had the same worry as you did at first). In practice I found that I rarely have to do what I wrote there for semi - because in Koka I never create such ambiguous interfaces in the first place. […]

I think it would be interesting to formalize (or at least point out using natural language) what this "price" exactly is (compared to what OCaml can do). Not sure how easy or difficult that is.

At some point we will probably add the ability to control imports more - hiding definitions etc, which will help.

Yes, that avoids boilerplate. But I think in order to reach the same expressiveness as OCaml (in that particular matter) without having to name each item of the grouped operations (thus effectively not really grouping them), it would be necessary to do the import on a per-implicit-basis.

Say you have a function that requires two monoids (as two implicit arguments). Then you might want to import one module to be used for the first implicit argument, and the other module for the second implicit argument.

In OCaml that's easily possibe:

module M = SomeFunctor (Additive) (Multiplicative)
let _ = SomeFunctor.foo arg1 arg2 arg3

In Koka we might have some function:

fun foo( arg1 : list<a>, arg2 : a, arg3 : int, ?monoid1 : monoid1<a>, ?monoid2 : monoid2<a> )

But a locally scoped import wouldn't work unless we could do that on a per-argument basis, like:

foo ( arg1, arg2, arg3, import addidive, import multiplicative )

In particular I don't think that avoiding dependencies is an issue. Define a local grouping if you want (no dependencies) - and a default way to derive it from the "convention" / names / operations you expect.

Yes, and I think this makes Koka quite powerful already.

No one has to know about your grouping - they just have to have the right things in scope. You will only have to manually construct / distinguish when you have an interface that has truly ambiguous implementations in scope.

Yes, but to my understanding it hasn't been mentioned in the paper that this "grouping" is (or should be?) limited in exposure and perhaps only be a library-local syntax-aid?

In a way you can't have both: Interoperability of this grouping mechanism and avoiding creating a type identity (with resulting dependencies) at the same time.

But the manual construction / manual choice is what you have to do with OCaml for everything - including adaptors.

I don't understand what you mean? Could you elaborate what you mean about OCaml here?

[TimWhiting]

Would you mind giving a short example on syntax? I am not following what you mean.

See this example file in the test suite. Here is the definition, but you'll want to look at the full example to understand what base does.

koka/test/overload/monad3.kk

Line 9 in 338bf4f

base : monad<m> // field names starting with "base" get unpacked recursively in .?

Newtyping:

On the other hand, if I create a new wrapping type to distinguish file descriptors from semantic-less integers, I could be annoyed if sorting fails because the type has changed and my newtype isn't Ord anymore. I have seen so many "pass-through" implementations of traits in Rust. A lot of boilerplate.

I wholeheartedly agree with you on this. I would never use a newtype to do a reverse-sort. Two different approaches / patterns I would use in Koka: one primary advantage of Koka's implicits is the ability to manually pass in an implicit - which is one way I would do a reverse sort: sort(l, ?cmp=reverse-cmp) note the different name reverse-cmp. This version make it clear what is happening, not relying on type magic. The other approach is to provide reverse-sort(?reverse-cmp) or reverse-sort(?cmp) or both actually and implement it in terms of the regular sort. This makes it clear what the semantics is without type magic, and without accidentally forgetting to give the implicit manually. I also recently encountered several layers of pass-through reimplementation of traits in Rust due to a newtype pattern, which causes useless boilerplate and obscures where real implementation details differ or reside. I wonder what the criteria is for what makes a newtype useful versus a hindrance. I wonder if a more relaxed newtype would be useful: discriminating if ambiguous, falling back if not.

Convention:

Yes, but even if both Koka and OCaml have "convention + adaptors", I still believe there is a difference. When newtypes are involved (only relevant for Koka, as OCaml doesn't do dispatch based on types), you will have to wrap and unwrap values later when using the polymorphic code (unless you wrap every function and make the function wrappers perform the wrapping/unwrapping). When no newtypes are involved, OCaml and Koka are still different. In OCaml, if the convention doesn't match, I can create an adaptor (a module) that fits a certain interface (a module type or signature) without needing to add any dependency to where the interface is defined. In Koka, I can either create a wrapper module or also a wrapper struct, each with the limitations as previously discussed.

I guess what I still think is that what you term an adaptation to an interface without needing to add a dependency would be more related in Koka to adding additional top level functions with the right names. To me grouping via structs is just a syntactic convenience, not conforming to an interface. Conformance to interface to me is conventional naming. In other words, I would first start by adding static overloads. I can add flat-map to every type, and they don't have to conform to a functor interface or anything like in Haskell. Often I'll be using static overloads directly. Like I mentioned previously the only time ambiguity shows up is precisely the interface between polymorphic and static code, and even then not frequently. If convention doesn't match (e.g. fmap versus flat-map, I don't need necessarily a full adaptor from one kind of functor interface to another at the level of entire groupings, I just need to add fun default/fmap(a: a, f: a -> m, ?flat-map: ....): ... {flat-map(a, f)}`. This would likely get inlined.

I think it would be interesting to formalize (or at least point out using natural language) what this "price" exactly is (compared to what OCaml can do). Not sure how easy or difficult that is.

I think this is rather difficult as evidenced by this conversation. Whether it is just something that could be "fixed" by adding structural subtyping is one interesting avenue of answering this question more formally. But, the fact that this deals with several features in Koka (overloading + implicits) makes it more difficult.

fun foo( arg1 : list, arg2 : a, arg3 : int, ?monoid1 : monoid1, ?monoid2 : monoid2 )

I agree that imports can be tricky to understand or visualize what they bring into / out of scope (especially when working with a narrow aspect). However, I think there is a bit of a misunderstanding here. There is no need to locally scope imports here, because I assume monoid1 stands for additive-monoid and monoid2 stands for multiplicative-monoid. Since they have different names, Koka will be able to disambiguate even if both are in scope. In fact you can just use a single type monoid<a> for both: the implicit name is a primary mechanism for discovering implicit parameters. Koka first filters based on the names, and then finds if there is a single instance of the correct type in scope for that particular name. We never mix up additive / multiplicative monoids if they are named such. If the available "instances" do not use distinguished names and a function expects them to be named such, you can pass them in manually, or assign the instances to local variables using those names. Vice versa, if the instances have distinguished names and you want to pass them to a more general 'monoid', same solution -> local variable or pass in the implicit manually. You can always create a functional abstraction with a distinguished name to do the adaptation if used frequently. But the adaptation rarely has to be at the level of a full struct grouping.

Yes, but to my understanding it hasn't been mentioned in the paper that this "grouping" is (or should be?) limited in exposure and perhaps only be a library-local syntax-aid?

At the end of the section we explicitly state that we are still learning the limitations in practice: "This simple mechanism can work surprisingly well, but of course it is limited as well compared to more specialized mechanisms like type classes. We hope to gain more experience in practice to evaluate its limits."

In a way you can't have both: Interoperability of this grouping mechanism and avoiding creating a type identity (with resulting dependencies) at the same time.

I don't believe I said that you can avoid creating a type identity with grouping. You can avoid the type identity with static overloading and convention. Implicits and static overloading are two separate mechanisms, but tightly related, and surprisingly powerful together as the paper shows.

I don't understand what you mean? Could you elaborate what you mean about OCaml here?

I just mean that regular OCaml doesn't have implicits. Every disambiguation or adaptation is done manually rather than through implicits.

[JanBeh]

See this example file in the test suite. Here is the definition, […]

Ah thanks, I understand now.

one primary advantage of Koka's implicits is the ability to manually pass in an implicit - which is one way I would do a reverse sort: sort(l, ?cmp=reverse-cmp) note the different name reverse-cmp.

The manual passing I see in other languages too (minus the part that it's an implicit in Koka and can be omitted in the standard cases in Koka, which is better in Koka of course).

But this only works if it's a single operation (or a few operations that are all explicitly passed) or a struct. In the last case, we have the "type identity issue" again, as discussed (which is the main concern of my original post).

As a side note, we see an explicit passing of a sorting function even in OCaml, see Stdlib.List.sort. OCaml doesn't use something like OrderedType and Functors here, because those are syntactically and sometimes also runtime-wise associated with an overhead. So in practice, some constructs that I love about OCaml don't always play out well in practice. (I'll get back to that when summarizing below.)

The other approach is to provide reverse-sort(?reverse-cmp) or reverse-sort(?cmp) or both actually and implement it in terms of the regular sort. This makes it clear what the semantics is without type magic, and without accidentally forgetting to give the implicit manually.

I'm not sure if ?reverse-cmp would be a good idea. Maybe for sorting, reverse-sort(?cmp) makes most sense, not sure. Or sort(negate(cmp)) or something like that.

I wonder what the criteria is for what makes a newtype useful versus a hindrance.

My feeling (and I don't have any substantiated or formal arguments for this) is that types should not be used with the sole intent to discriminate different operations that work on the same underlying data. I believe newtypes should be used when we have the same representation for an entirely different datum from a semantic point of view (like "a file descriptor is an abstract entity, and not the same as an integer"). We then can select operations based on that newtype, of course, but I don't think we should motivate a newtype in order to do that selection of operations. But in some languages we are forced to do the latter.

I wonder if a more relaxed newtype would be useful: discriminating if ambiguous, falling back if not

Interesting thought. Like we could sort a file-descriptor by default in that case.

To me grouping via structs is just a syntactic convenience, not conforming to an interface. Conformance to interface to me is conventional naming.

I think I understood that part now and it's what I meant with: "that this 'grouping' is (or should be?) limited in exposure and perhaps only be a library-local syntax-aid?" The grouping mechanism outlined in the paper is not meant to be used as an interface. Interfaces are still done through conventional (ungrouped) naming. (Or only grouped using modules.) This is something I misunderstood for a while. Specifically, I didn't conclude this from the "limitations" mentioned in the paper.

But if interfaces are really given by conventional naming, then Koka's limitations on grouping operations and passing grouped operations aren't really limited by the .? syntax and the mechanism proposed in section 4.2. Then the limitations of Koka in this matter are actually dependent on how you can do selective imports, locally scoped imports, etc.

However, I think there is a bit of a misunderstanding here. There is no need to locally scope imports here, because I assume monoid1 stands for additive-monoid and monoid2 stands for multiplicative-monoid. Since they have different names, Koka will be able to disambiguate even if both are in scope.

Well, yes, you previously proposed two use different conventions for those:

I would actually probably say that these should be different operations -> prefer additive-monoid and multiplicative-monoid, since monoid is arguably too general for domains that have both -> and pass them explicitly to operations that work for general monoids -> since you know which one you want to use.

Maybe the monoid example is a bit unfortunate here. There could be an example where some code needs two "abstract numbers", e.g. numbers for weights and numbers for coordinates, and you would want to be able to pass different implementations. In some OCaml code I recently was writing a functor as follows:

module Make
    (WeightNum : Number.S)
    (CoordNum : Number.S)
    (VertexSet : Set.S with type elt = CoordNum.t Iarray.t) : … = …

Yes, but to my understanding it hasn't been mentioned in the paper that this "grouping" is (or should be?) limited in exposure and perhaps only be a library-local syntax-aid?

At the end of the section we explicitly state that we are still learning the limitations in practice: "This simple mechanism can work surprisingly well, but of course it is limited as well compared to more specialized mechanisms like type classes. We hope to gain more experience in practice to evaluate its limits."

In a way you can't have both: Interoperability of this grouping mechanism and avoiding creating a type identity (with resulting dependencies) at the same time.

I don't believe I said that you can avoid creating a type identity with grouping. You can avoid the type identity with static overloading and convention. Implicits and static overloading are two separate mechanisms, but tightly related, and surprisingly powerful together as the paper shows.

Yes, the paper doesn't say anything wrong. I just intepreted more into this "grouping" and assumed it could be used for interfaces (why shouldn't I assume it?). Now I learned it is likely not the canonical way to define interfaces. Maybe that point could be made more clear in the future. Like I said above, the practical limitations then will not just arise from this "grouping" (and what it cannot do), but also from what can or cannot be done when not using that grouping mechanism (while we still might want to handle a set of types and operations on them as a single unit).

I don't understand what you mean? Could you elaborate what you mean about OCaml here?

I just mean that regular OCaml doesn't have implicits. Every disambiguation or adaptation is done manually rather than through implicits.

Oh, yeah sure. Specifically, OCaml can be very verbose syntactically. And this is how I would like to draw a small résumé for myself:

I really like the way how OCaml (not Koka, sorry 😅) allows me to specify interfaces that group types and operations while avoding dependencies (due to the structural typing of signatures). It also allows me to pass implementations of those interfaces. I have not seen any other language so far, which gives me this expressiveness, and I really love it.

But OCaml does not have implicits at all. This makes syntax verbose and unhandy in practice. Moreover, every functor in OCaml is a lot of syntactical noise.

While I like OCaml's approach in theory (disregarding several inconsistencies and issues in OCaml, e.g. this one), I feel like Koka's approach may be much nicer in practice, but I still see limitations in theory. I would like to better understand what I'm really missing in Koka, coming from OCaml. Maybe all it needs is an easier way to import modules selectively in order to reach the same level of expressiveness? Or maybe the problem I see is only of theoretical value anyway and doesn't occur in practice? I'm not sure.

Either way, thanks again a lot for this discussion. When I hopefully have some more time to try Koka in practice, I might get a better feeling for the different options Koka offers (and maybe feel its limitations or learn that they are neglectible or even non-existent). Generally, I really like the dot-syntax and the idea of combining implicits with overloading. It might create very easy-to read and concise code (opposed to the clunky syntax in OCaml).

[TimWhiting]

I really like the way how OCaml (not Koka, sorry 😅) allows me to specify interfaces that group types and operations while avoding dependencies (due to the structural typing of signatures). It also allows me to pass implementations of those interfaces. I have not seen any other language so far, which gives me this expressiveness, and I really love it.

I think your opinion is totally valid. OCaml does not have the same theoretical issue as Koka due to its structural subtyping. Thanks as well for the discussion, especially since this is one of the parts of the paper that we could use the most feedback on what the limitations are in practice and theory.

I wonder if we can address the structural typing issue with only a slight change in grouping. Currently .?num: num<a> desugars to ?num: num<a> followed by a match destructuring the elements -> which has the issue of nominal typing. What if instead it desugared to: ?num: a, ?add: a -> ((b,b) -> b), ?mul: a -> ((b,b) -> b)). In other words the function is polymorphic over all structures that have the same interface as num. The primary issue I see with this is the performance, since the accessor functions are provided as separate parameters and have to be looked up on type a (polymorphic), not known ahead of time. It solves the syntactic issue, at the expense of dynamic issues. To be fair this is the same issue that structural subtyping might have -> the functions would have to be looked up dynamically (by name) or have some consistent global ordering on fields across subtypes. In both cases we can probably optimize such calls via normal specialization / inlining, as well as other techniques.

In other words, we can view "interfaces" / structural typing, as just another kind of constraint on a particular shape of polymorphic function.