Lavender Type System Higher Rank Types - kvverti/rusty-lavender GitHub Wiki

Higher rank types have been a goal for Lavender's type system since the beginning. Being able to express and check against higher rank types allows many useful constructs to be expressed, including:

• Enforcing independence between two type variables
• Certain forms of existential type usage
• Greater flexibility in users of functions such as callCC.

However, higher rank types pose several implementation concerns. Lavender chooses to answer some of these concerns with the following design

• Lavender shall have at least forall quantification at any level, and possibly exists quantification at any level.
• The scope of a quantifier is always implicitly reduced to the smallest possible scope. The scope of a quantifier should not be widened if explicitly given.
• Internally, the type checker will perform skolemization and instantiation of higher rank types at the latest possible time of application.
  • The dependencies of existential variables will be only the in-scope universal variables.
    • The above point forbids hiding escaping existentials behind another existential, which may be undesirable.
  • As a corollary, a universal quantifier cannot be moved below an existential-equivalent quantifier in a nested scope.
  • The type checker will check type variable dependencies and reject cyclic dependencies.

Examples:

def one: for a. a -> (for b. b -> a)

A rank-1 type. Equivalent to for a b. a -> b -> a, which is implicitly reduced.

def two: for a. (for b. b -> a) -> a
# equivalent to
def two: for a. some b. (b -> a) -> a

A rank-2 type. b is in an existential position, and is dependent on a.

def three: for b. some a. b -> a

An existential type. In this case, a is dependent on b. Attempting to type check two three should result in a type error.

def four: (some a. a) -> _

A rank-1 type. Almost equivalent to for a. a -> _, but the return type of four cannot depend on the variable a. This rule prevents scope escape from hiding behind an additional existential variable, but this may be undesirable.

def five: (some a. a) -> (some b. b)

Equivalent to some b. for a. a -> b rather than for a. some b. a -> b.