Questions about Simple[r]-sub

[devdtc]

Thanks for the paper and discussion here--Algebraic Subtyping is very exciting and I'm looking forward to implementing it in my toy language!

I had a few more follow-up questions to that discussion specific to Simple-sub:

1. I have a vague idea that Simple-sub does some extra work that Cubiml skips in order to simplify types for presentation, but could you elaborate on the other practical differences (advantages and weaknesses) of the two approaches?
2. One limitation of Cubiml is the inability to specify polymorphic type annotations. Is this feasible in either Simple-sub or Simpler-sub? Seems important for things like the FFI.
3. Regarding the simplifications made for Simpler-sub:
   1. I understand the example given for simplification 3, but I'm not sure I fully understand the implications. What else should I know about this other than that it forces the arms of conditionals to match? Does it still allow width subtyping of function arguments? E.g. let f x = { x with name = "f" } : 'a -> 'a <: {name: string}. Actually, what would the constraint on 'a look like in this case to ensure it's a record of some kind?
   2. Starting from Simple-sub, in broad strokes, what changes would give you simplification 3 without 1 and 2? Is the algorithm that much different, or are you merely removing a few parts?
   3. Can you provide some examples of where simplification 3 would reject well-typed terms?
4. Would implementing an alternative record type (let's call it a "struct") that supports record update but not width subtyping, in addition to the standard record that does support width subtyping, be feasible in Simple-sub or Simpler-sub?
5. My intuition from reading the paper suggests that implementing abstract/existential types in module signatures shouldn't be too bad if type annotations are reasonably expressive. Does this sound right?

Sorry for all the questions and my ignorance (feel free to just point me at the paper or somewhere else), and thanks for your time!

[LPTK]

Hi Dan!

Sorry for the late reply, I've been really busy these days. Let me try to answer your questions point by point:

1. I am not that familiar with Cubiml, as I only looked into it superficially. But as far as my understand, both are mutable graph-based implementations of MLsub constraint solving, and I expect that both should be fairly similar algorithmically. But as you say, Simple-sub additionally performs some simplification, which in particular normalizes type representations. For instance, it aligns unions and intersections of recursive types, "zipping" them together by unrolling them until they match – I call this canonicalization.
   This can have some uses beyond simplification, such as ensuring that certain forms of types are never merged into the same union or intersection, like for instance int & string. You need canonicalization to reject types like ((int -> 'a) as 'a) | ((string -> string -> 'b) as 'b), which will be canonicalized to (int & string -> int & string -> 'a) as 'a.

2. You can specify polymorphic type annotations for external functions, no problem. On the other hand, the act of checking if a given term satisfies a given polymorphic type annotations is a little tricky, but still doable (though it's not implemented in the Simple-sub code base). If you're interested in this I can go into some detail.

3. Regarding the simplifications made for Simpler-sub:

   i. Yes of course, you still get width subtyping – though you may get some unification which removes a little precision in some cases. Trying to simplify your example (let me know if that's too simplified): the term let f x = strLen x.name would be given type 'a -> int where 'a would have an upper bound 'a <: { name: 'b } and where 'b <: string. Now, in this simple case the type would be simplified to { name: string } -> int (the type variables are not useful).

   ii. Simplification (3) is the most significant of Simpler-sub's simplifications, as it fundamentally changes the way constraints are handled – instead of arbitrary graphs of type variables, we now deal with type variables that have simple, concrete upper and lower bounds, computed through LUB and GLB functions. I think this makes subtype inference much easier to reason about and to handle in a practical compiler.

   iii. Yes, here is an example: let f x y = (x, if ... then x else y) in strLen (f "a" false)._1. Here, f is assigned type 'a -> 'a -> ('a, 'a) because we have merged the types of x and y due to the if-then-else. Thus, call (f "a" false) results in type (?X, ?X) where type variable ?X :> string and ?X :> boolean (equivalently, ?X :> LUB(string, boolean) =:= top), on which you can't perform strLen. On the other hand, in simple-sub, for f you'd have obtained the type 'a -> 'b -> ('a, 'a | 'b), and you could have type checked its later use.

4. Sure, but you'd need to disambiguate fields one way or the other, so that it's always clear what type of x the expression x.field requires. This has been a sticking point of global type inference and languages like OCaml, Haskell, and PureScript have all come to different solutions. Like PureScript, you could use row polymorphism or like Haskell some sort of type class resolution – indeed, to type check x.field, what constraint should be inferred on the type of x? Row polymorphism would say that this type should be a subtype of { x: ?A | ?R } where ?A is a type variable and ?R is a row variable representing the other fields in the record. Note that this latter approach still does not allow for efficient field access implementation unless you perform some specialization/monomorphization of the code

5. Could you be a little more specific about what you have in mind with this? I think an example would help :^)

Hope that helps!

[devdtc]

This is fantastic, thanks Lionel!

2. Got it. Is the situation the same with Simpler-sub? I don't want to take too much of your time, but roughly how difficult would it be to check polymorphic type annotations? The main use I have for this I think is for module signatures (see 5).
3. 1. I think I asked two questions here in a confusing way. You answered the main one, but my other question was something like: what does the constraint look like for record extension? Is this where row polymorphism would come in?
4. Gotcha, I suppose then the disabling of subtyping on "structs" would just have the benefit of making monomorphization easier, or possibly a guarantee depending on use.
5. I want to be able to write something like:

   module Map with
     type T k v = abstract,
     type StringMap v = T String v,
   
     empty : T k v,
     insert : k -> v -> T k v -> T k v,
     ...
   where
     type T k v = [Empty | Node k v (T k v) (T k v)]
   
     empty = Empty
     init k v t = ...
   end

   Here, users of the Map module would be able to use Map.T to pass to functions within the module, but the structure of Map.T would not be visible outside the module. Does that make sense?

[LPTK]

Sorry for the delay. As you can imagine, this end of the semester was very busy!

how difficult would it be to check polymorphic type annotations?

Not very difficult I expect. In fact I think it'll even be a bit simpler than for Simple-sub/MLsub, as you would have less normalization of types to do, since they will already be reduced to simple LUBs or GLBs.

what does the constraint look like for record extension? Is this where row polymorphism would come in?

Well it depends how you design your type system and what static and dynamic semantics you want. The trickier question is what type the updated value would have. You could either make records invariant, and then infer constraints like ?a <: { x: ?b } where ?b :> string. Or, again, you could use row polymorphism with shadowing semantics, which may not need to constrain the type of the receiver at all, and could yield a type like { x: string | ?a } meaning "add an x: string field on top of ?a, shadowing what ?a may already define as x".

As a small digression, in my new MLscript language prototype (which removes the restrictions on the polarity or unions and intersections), the type given to fun x -> x with { name = "f" } is 'a -> ('a\name & {name: "f"}) where 'a\name is the type of 'a from which field name has been removed. You can try it out here: https://hkust-taco.github.io/mlscript/

I suppose then the disabling of subtyping on "structs" would just have the benefit of making monomorphization easier

I don't see how it would make monomorphization easier. It's just that, if you design your system well, you could simply compile field accesses to reads at an offset from the object's base pointer. This is just not possible when the object could have many possible shapes, in which case you need some sort of dictionary or fields implemented as virtual getter methods.

I want to be able to write something like:

Sure, you basically want ML modules. There is nothing in MLsub/Simple-sub that would prevent you from just implementing ML modules in the classical way.

[devdtc]

Thanks again Lionel! I think I have enough to go on now--appreciate all the help. :)