Type Synonyms

[AshleyYakeley]

Option 1 type T = type Pinafore infers the maybe-polarity of T

Option 2 type T = type -- T is ambipolar type + T = type -- T is positive type - T = type -- T is negative

Prefer option 2, possibly syntax could change.

[AshleyYakeley]

If we allow recursive types (#2), then we should allow recursive type synonym definitions, e.g. type T = [T].

[AshleyYakeley]

Easiest way to do this, with parameters and recursion:

• only permit ambipolar types
• only permit grounded types
• create new type containing body, with bidirectional subtype relationships to body

[AshleyYakeley]

Equivalents of storable types won't be storable, which would be surprising for synonyms.

[AshleyYakeley]

Type synonyms with both parameters and recursion probably makes no sense, for example:

type T a = Maybe (T (List a))

This doesn't correspond to a Pinafore type.

So let's drop recursion.

[AshleyYakeley]

Simplest way is to take a very template-like approach. Types have parameters, but they are not checked for variance and {-p,+q} is not allowed. They simply substitute in, so you could do, e.g. type Endo a = a -> a, even though that "parameter" is neither covariant nor contravariant.

[AshleyYakeley]

Slightly nicer (maybe?) would be to enforce parameter variance, and allow rangevariance, but otherwise treat it as a template.

[AshleyYakeley]

One possibility, that would dovetail with #172:

• type creates a new ground type constructor with no other special properties
• type storable creates a new ground type constructor that is storable

Note that greatest dynamic supertype would not be preserved. But subtype relations would be, since the new type would be equivalent to its source.