SubTyping | Exercise 7

In type theory, sub typing denoted by (<:) is a relation that describes when one type can be used in place of another type. It's more like flexible version of type equality.

Y -> XY -> X <: XY -> X -> XY

The notation we are seeing is about function types and record types:

1. X, Y, XY are record types
2. -> represents function types
3. <: means is a sub type

For example:

1. X = {X:Nat} means a record/object with just an x field of type Nat (Natural Number)
2. Y = {y:Nat} means a record with just a y field of type Nat
3. XY = {x:Nat, y:Nat} means a record with both x & y fields.

A function type A -> B means a function that takes an input of type A and returns a type B.

So when we are seeing something like:

XY -> X <: Y -> XY 

it's asking Can a function that takes Xy and returns X be considered a subtype of a function that takes a Y and return XY?

The rules for determining this involves:

1. Contra variance of input types (domains)

1. This refers to how function input types (the domain) are compared when checking sub typing.
2. The sub typing rule is: If S1 <: S2, then a function accepting s1 is a subtype of a function accepting S2. (S1 -> T <: S2 -> T)
3. Example:
4. If Nat :< Int, then Nat -> X is a subtype of Int -> X
5. Covariance of output types (ranges)
6. Structural compatibility of types