# Row polymorphism extended to modules

One common observation in type systems is that having subtyping makes type inference hard [1]. Consequently, for records, many modern functional languages shun subtyping (OO style) in favor of row polymorphism. Some examples include:

• Ur/Web - duplicate labels are disallowed, the programmer uses first class disjointedness proofs to combine records.
• Koka - duplicate labels are allowed and are used to encode effects [2].
• Purescript - duplicate labels are allowed and are used to encode effects [3].

ML-style module systems may be thought of as extending records by allowing type definitions and abstraction as well, along with all the complications those entail, such as recursive definition, preservation/loss of type equalities etc.

SML and OCaml's (and probably many other MLs') module systems allow subtyping. Also, OCaml doesn't offer much in terms of type inference for module signatures (I'm assuming SML is similar here).

Q: Is there an equivalent of row polymorphism at the module level? (I mean something documented in the literature or used in some existing language). Something that would make the following type-check:

module type S1 R = { type t; val f1 : t -> int; | R }
module type S2 R = { type t; val f2 : t -> int; | R }
functor F (M : S1 R) : S2 R = { type t = M.t; let f2 x = f1 x * 2 | R }

module M : S1 { type u; } = {
type t = char;
let f1 = atoi;
type u = Traveller;
}

(* Arrived! *)
type traveller = (F M).u


It seems plausible that something like Ur/Web's system would work as you'd want to enforce uniqueness of type definitions and not have the order of definition matter.

If such a system does exist, please provide citations :). If not, please try to provide an explanation at the level of an introductory type theory book (e.g. Pierce's Types and Programming Languages) of why this wouldn't work [4].

Note: While this question specifically asks about ML-style modules, answers related to mixin modules are also welcome (although I'm only very vaguely familiar with them).

[1] Yes, I know about the Algebraic Subtyping paper which shows an alternate approach, but that is relatively recent work.

[2] Leijen, Daan. "Koka: Programming with row polymorphic effect types." arXiv preprint arXiv:1406.2061 (2014).

[4] I had a quick look at the 8th chapter in Pierce's Advanced Topics in Types and Programming Languages which goes over ML modules in quite some detail. It seems to take subtyping as a given, for understandable reasons.

• hmm, completely off-topic, but this is not type theory, but type system. they are confusing and tightly related but I do not find type system necessarily involves type theory too much. interesting that there is no type-system tag. – Jason Hu Aug 19 '18 at 18:07
• Several related questions have the type-theory tag so I chose to stick to instead of creating a new one. – cutculus Aug 19 '18 at 18:38
• I don't have references for you. But, as someone who's implemented row polymorphism, I'd like to say that it is not a recipe for 'easy' type inference. In fact, there's quite a bit of literature out there on various restrictions to avoid exponential blowup. A better reason to have row polymorphism is that quantifiers and variables can express things that subtyping can't. For instance, the type of the polymorphic identity function forall a. a -> a has no obvious translation to subtyping. And of course, you have a row type example in your functor. – Dan Doel Sep 2 '18 at 1:02
• @DanDoel MLSub integrates subtyping with parametric polymorphism, so a type of forall a. a -> a can still be assigned. I agree that the "motivation section", so to speak, is a bit weak; I've deliberately kept it short to avoid focusing on it too much. – cutculus Sep 2 '18 at 1:21