[TYPES] Has anyone seen a language with sub-typing and recursive parametric type aliases?
Isaac
Isaac.Oscar.Gariano at ecs.vuw.ac.nz
Mon Feb 24 03:16:21 EST 2020
Dear Stefan,
Thanks for the reply!
>> Note that partially-applied type aliases are not allowed, e.g. "List" is not a valid type.
> I'm not completely sure what you mean by "valid type" here.
> Clearly, `List` is not a proper type, so do you mean that `list` cannot
> appear un-applied within a type expression? Can arguments to your type
> aliases be something else than proper types?
No they cannot.
Any mention of a type-alias name must be supplied with the appropriate number of type arguments or it is an error.
(alternatively, the missing ones might be inferred).
In particular, higher-order type aliases are not allowed:
type Foo[C] = C[Int] // error, only type-aliases can be supplied with paramaters
type Bar[X] = { head -> X }
type Baz = Foo[Bar] // error, Bar needs 1 type argument
Thus all type-aliases are of kind * -> * -> ... -> * (for some finite number of arrows).
Although I believe languages like Haskell or Scala can support such constructs.
> AFAICT here you need to use the property:
> ∀X,Y. X <: Y implies Exploding-List[X] <: Exploding-List[Y]
> in order to prove the subtyping without hitting the inf-loop.
> If all your arguments are proper types, than you can probably get
>a working algorithm that keeps track of the polarity of arguments and
> uses this kind of reasoning (instead of expanding the definition)
> whenever faced with
> Exploding-List[...] <: Exploding-List[...]
> Now I don't think it's going to help you very much with
This looks like inferring the variance of the type-paramaters? (which Typescript appears to be doing). I'll look into literature on this, thanks.
> Exploding1-List[...] <: Exploding2-List[...]
> and other fun stuff.
Sadly not, but perhaps that is an unlikely case?
Although I feel rejecting such code kind of defeats the spirit of a structural type system.
More information about the Types-list
mailing list