Re: [TYPES] Has anyone seen a language with sub-typing and recursive parametric type aliases?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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.