Add test showing that finite hashes are subtypes of generic hashes of the right shape

[ptarjan]

I was exploring the subtype relationships between finite hashes and generic hashes and was surprised by the two commented out results here. Should they be true? Or can you please explain to me why they aren't.

[jeffrey-s-foster]

The first one, tt("{a: Integer, b: String}") <= tt("Hash"), fails because there's no rule that allows a parameterized type to be a subtype of a non-paramterized type with the same base. In other words, right now it's not the case that Hash<Symbol, Integer or String> <= Hash. Is this an important case to allow? I don't see a major problem with letting it typecheck it but it might warrant a warning that could be switched off with a configuration option.

The second one, tt("{a: Integer, b: String}") <= tt("Hash<Symbol,%any>"), is not allowed because of mutation. It should be that {a: Integer, b: String} <= Hash<Symbol, Integer or String>. But it's not the case that Hash<Symbol, Integer or String> <= Hash<Symbol, %any> because that would be unsound. For example, simplifying slightly, if x has type Hash<Symbol, Integer> and we let y = x where y has type Hash<Symbol, %any>, then we could set y[:a] = "foo", and now x's type does not match its actual value.

Because of this unsoundness I don't want to generally allow the second case, but this is one of those rules that can be annoying in practice. For example, I believe DART does allow this unsound subtyping, on the theory that it is mostly sound in practice and doing the sound thing gets in the way too much. So if this case is common, I wouldn't be adverse to optionally allowing the unsoundness.

[ptarjan]

The first one, tt("{a: Integer, b: String}") <= tt("Hash"), fails because there's no rule that allows a parameterized type to be a subtype of a non-paramterized type with the same base. In other words, right now it's not the case that Hash<Symbol, Integer or String> <= Hash. Is this an important case to allow? I don't see a major problem with letting it typecheck it but it might warrant a warning that could be switched off with a configuration option.

I'm not sure how important it is since right now I'm doing a pre-transform step from our runtime type system into RDL's string language so I can apply whatever transform at that point. It was pretty surprising to me that it didn't work that way, so to work with the principal of least surprise I'd probably suggest to make that work. Is it unsound? What would the warning be? Do you already have a warning framework?

The second one, tt("{a: Integer, b: String}") <= tt("Hash<Symbol,%any>"), is not allowed because of mutation. It should be that {a: Integer, b: String} <= Hash<Symbol, Integer or String>. But it's not the case that Hash<Symbol, Integer or String> <= Hash<Symbol, %any> because that would be unsound. For example, simplifying slightly, if x has type Hash<Symbol, Integer> and we let y = x where y has type Hash<Symbol, %any>, then we could set y[:a] = "foo", and now x's type does not match its actual value.

Because of this unsoundness I don't want to generally allow the second case, but this is one of those rules that can be annoying in practice. For example, I believe DART does allow this unsound subtyping, on the theory that it is mostly sound in practice and doing the sound thing gets in the way too much. So if this case is common, I wouldn't be adverse to optionally allowing the unsoundness.

Yeah, in the face of untyped code we think that we might have to make this unsoundness compromise. We're struggling with what happens when you do:

type 'Array<Integer> -> Array<Integer>'
def my_function(an_array)
  an_array.map {|element| some_untyped_function(element)}
end

We're unsure if the right way is to make the sub typing unsound or to introduce a %dynamic which can have anything done to it. I think the dynamic approach is what Hack, Flow and mypy do but it does introduce unsoundness in presence of gererics.