Here’s a simple example of recursive types interacting badly with subtyping:

T={ foo: T -> A}

U={ foo: U -> B}

Consider `T <: U`

, therefore

(T -> A) <: (U -> B)

Which implies:

U <: T

So `T <: U`

but also `U <: T`

, which is true iff `A <: B `

and `B <: A`

.

In my case, the subtyping relation is polymorphic subsumption: `T`

is subsumed by `U`

iff `U`

is “more polymorphic”, intuitively, it can be instantiated to all types that `T`

can.

This situation arises in rather simple code, involving polymorphic vs. non-polymorphic row fields. For example, `A`

is a row with a polymorphic method, whereas `B`

is a row with a monomorphic (but compatible) method, such as:

A = { method: forall a. a -> () }

B = { method: String -> () }

In this case subsumption (the form of subtyping in play) fails.

One way around this is to avoid subsumption issues altogether by keeping things rank-1, and not using higher-rank row fields. Unfortunately, throwing away polymorphic methods is very bad: consider a non-polymorphic `array.map`

(in JS).

A slightly better workaround is to push the foralls all the way out, keeping all types (including row types) rank-1. Every time an object method is accessed via the property syntax `obj.method`

, we end up instantiating the object’s row type, and get a “fresh” type for the method. We get practically polymorphic methods. That’s the approach I’m investigating for **infernu**.

Just stumbled upon infernu. Interesting project!

I’m not sure I follow this post though. The two foo functions return types aren’t related so I would say that the function types aren’t related either. With proper variance (T => A) B) iff U <: T and A <: B

In the polymorphic example I would say that forall a. a is just a synonym for Number|String|… thus String <: forall a. a. Since () <: () we can say A.method <: B.method.

Btw. Have you seen the paper on pure subtype systems? Might provide som inspiration for getting polymorphisms involving string literals in place (not uncommon in js), might also be way to give o[“method”] the same type as o.method.

I’m not sure what you mean by the syntax “(T => A) B)” – did WordPress ruin your text? what did you mean by that?

I agree that A.method <: B.method – which then implies A <: B But in the case of recursive U, T we also expect B <: A which in this case doesn't hold. We end up not having any subtyping relation at all between (non-equal) recursive row types in the form of U and T.

Yeah, wordpress ate some of the brackets 😉

I meant T.foo <: U.foo iff U <: T and A <: B

However, I realize now that you really meant recursive (I read the asignments as object level variables, so didn’t account for the fact that var T was supposed to equal type T in your argument…)

But why do you say T <: U ?

I’m not entierly convinced that A.method <: B.method implies A <: B though. Is that from rowtypes or how do you get to that conclusion?

If i take A and B as functions

A = “method” -> (forall a. a -> ())

and

B = “method” -> (String -> ())

it kind of follows that A <: B, but can we generlize that to composed records?

In the paper I was talking about ( http://stuff.thedeemon.com/pure-subtype-systems-popl10-hutchins.pdf ) they apparently decide to avoid the issue by having invariant argument types. “The practical applications of System λC that we have explored thus far (i.e. modules) do not require contravariance, so we have not included it in the theory”