[idl] Simplify function subtyping to positional args

[rossberg]

As discussed on #465.

This doesn't change the surface syntax, just the subtyping rule.

[nomeata]

Main complaint: Don’t allude to records when they behave very differently now.

[nomeata]

Again, I think alluding to records is more confusing than helpful here. Better allude just to tuples, or to nothing at all.

[rossberg]

Simplified language. The alluding was to explain the rule as actually expressed.

[nomeata]

Thanks. But the rule is still not compositional, i.e. refers to record in the precedent without records being involved.

I was expecting something like this, with a rule to explain subtyping on argument lists:

-----------------------------------------
( ) <: ( <argtype>,* )

<argtype1> <: <argtype1'>
( <argtype2>,* ) <: ( <argtype2'>,* )
------------------------------------------------------------------------------------------------
( <argtype1>, <argtype2>,* ) <: ( <argtype1,>, <argtype2'>,* )

and then a simple rule for functions:

( <argtype1'>,* ) <: ( <argtype1>,* )
( <argtype2>,* ) <: ( <argtype2'>,* )
-------------------------------------------------------------------------------------------------------------------
func ( <argtype1>,* ) -> ( <argtype2>,* ) <funcann>* <: func ( <argtype1'>,* ) -> ( <argtype2'>,* ) <funcann>*

[rossberg]

The idea was to avoid rule duplication and emphasise the semantic equivalence with tuple records. In particular, once we have the unsoundness issue resolved, the solution will directly apply to functions as well in a natural way.

[nomeata]

The idea was to avoid rule duplication and emphasise the semantic equivalence with tuple records.

Guess it’s a matter of taste … in our AS typing rules you were usually arguing strongly for compositional rules. And the equivalence feels more like a derivable theorem to me than something that should be the definition.

Also, I think it is confusing to go via records here if names on tuples are irrelevant for subtyping, but names on records are not? (Yes, the former is a short-hand, and precise reading of the rules is fine, but there is still room for confusion).

Would it be cleaner to give upon “tuple records” as a non-first-class short-hand-induced concept and

• introduce tuples as a type separately from records
• tuples can name the fields, but it’s only for documentation,
• have prefix subtyping on tuples,
• functions take and return tuples (we can refer to their subtyping rules in the func rule)
• records are a separate thing, and must have names or numbers on fields

In particular, once we have the unsoundness issue resolved, the solution will directly apply to functions as well in a natural way.

Optimist :-). I’d like to see a solution first before drawing such conclusions.

[rossberg]

Well, that's the thing: I very much want to avoid introducing multiple notions of product type with multiple sets of subtyping and elaboration rules.

Not sure why you are saying that the rules aren't compositional. Do you mean inductive on syntax?

[nomeata]

very much want to avoid introducing multiple notions of product type with multiple sets of subtyping and elaboration rules.

But isn't that precisely what this PR will introduce: We’d have sequences with prefix subtyping (only in function arguments so far, but there is no strong reason for that restriction) and records (with different subtyping rules). Sure, the rules have some overlap, but they seem already pretty different notions to me.

Having the cake and eat it too would be to only have tuples (you mentioned that option during the last call, right?)

(Incidentally, we have bool, and opt and variant, which are multiple notions of sum types with multiple set of subtyping and elaboration rules…)

[rossberg]

Well, the current formulation reduces it to a (syntactic) special case of the more general mechanism, which in my mind means that at least semantically, there is only one mechanism.

[nomeata]

I still think it’s odd:

We have

record { foo : Int; bar : Text } <: record { bar : Text } 

but not

func () -> ( foo : Int, bar : Text ) <: func () ->( bar : Text )

and yet we explain the latter via the former (and yes, the reduction is correct, because field names get resolved/removed before the reduction, but it is confusing and misleading.)

I expect that the different treatment of names will confuse people, if we don't clearly distinguish records for tuples in our explanation. And we will face questions like “why can I have tuples only in function arguments”.

But as we agree on the semantics, and this document is mostly for internal consumption, I will not block you on this. If we ever write a paper about the IDL, I will fight this again :-)

[rossberg]

Thanks! :)