Introduction At the very least when it comes to types, something of type A \texttt{A} A can be used whenever something of type A \texttt{A} A is expected.
int a = 5 float b = 5.0 \texttt{int a = 5}\newline\texttt{float b = 5.0} int a = 5 float b = 5.0
Is there any leeway for flexibility? Specifically, does there exist a notion of type substitutability?
float b = 5 \texttt{float b = 5} float b = 5
This makes sense because an int \texttt{int} int is a subset of a float \texttt{float} float . In other words, a float \texttt{float} float can do anything an int \texttt{int} int can do.
int b = 5.0 \cancel{\texttt{int b = 5.0}} int b = 5.0
This wonβt work. An int \texttt{int} int cannot do everything a float \texttt{float} float can do (cannot represent all of its values). A quick way to break this is: int b = 5.5 \texttt{int b = 5.5} int b = 5.5
Definition S < : T S <: T S <: T means that S S S is a subtype of T T T .
This means that anything of type S S S can be used whenever type T T T is expected.
So in the above example:
int < : float \texttt{int}<:\texttt{float} int <: float
You can think of it as S S S is more restrictive (to typecheck) than T T T since if you want to do something with T T T , you should also be able to do it with S S S .
Structures Width Subtyping Class Hierarchy Suppose a class lineage has the following structures.
class Animal: string name int age void β void makeNoise class Mammal extends Animal: string furColor class Human extends Mammal: string occupation int netWorth void β int doTaxes
\begin{align*}
&\texttt{class Animal:}\newline
&\texttt{\qquad string name}\newline
&\texttt{\qquad int age}\newline
&\texttt{\qquad void}\rightarrow\texttt{void makeNoise}\newline
&\newline
&\texttt{class Mammal extends Animal:}\newline
&\texttt{\qquad string furColor}\newline
&\newline
&\texttt{class Human extends Mammal:}\newline
&\texttt{\qquad string occupation}\newline
&\texttt{\qquad int netWorth}\newline
&\texttt{\qquad void}\rightarrow\texttt{int doTaxes}
\end{align*}
β class Animal: string name int age void β void makeNoise class Mammal extends Animal: string furColor class Human extends Mammal: string occupation int netWorth void β int doTaxes β
By definition of class hierarchy, a child has every characteristic its parent has. For example, Human \texttt{Human} Human has a furColor \texttt{furColor} furColor , and transitively, since Mammal \texttt{Mammal} Mammal has a name \texttt{name} name (among other things), so does Human \texttt{Human} Human .
Since children have everything their parents have (and thus can do anything the parents can do):
Human < : Mammal \texttt{Human} <: \texttt{Mammal} Human <: Mammal
Mammal < : Animal \texttt{Mammal} <: \texttt{Animal} Mammal <: Animal
β and transitively β - \textit{and transitively } - β and transitively β
Human < : Animal \texttt{Human} <: \texttt{Animal} Human <: Animal
Generally:
Child < : Parent \texttt{Child} <: \texttt{Parent} Child <: Parent
This is called width subtyping since supertypes (opposite of subtypes) contain a subset of fields (along the width of the class definition).
The notion of width subtyping can be extended to datatypes without hierarchical relationships.
For example, suppose there are two unrelated datatypes with the following definitions.
struct Named: string name struct User: string name string age
\begin{align*}
&\texttt{struct Named:}\newline
&\texttt{\qquad string name}\newline
&\newline
&\texttt{struct User:}\newline
&\texttt{\qquad string name}\newline
&\texttt{\qquad string age}
\end{align*}
β struct Named: string name struct User: string name string age β
They have no explicit relationship. However, it sort of makes sense that whenever a program expects a Named \texttt{Named} Named entity that we can pass it a User \texttt{User} User (since anything a Named \texttt{Named} Named has, a User \texttt{User} User also has).
Example:
func rename(Named entity, string newName): entity.name = newName User user = { name: βgleeβ, age: 1000 } rename(user, βnot gleeβ)
\begin{align*}
&\texttt{func rename(Named entity, string newName):}\newline
&\texttt{\qquad entity.name = newName}\newline
&\text{}\newline
&\texttt{User user = }\lbrace\texttt{name: βgleeβ, age: 1000}\rbrace\newline
&\texttt{rename(user, βnot gleeβ)}
\end{align*}
β func rename(Named entity, string newName): entity.name = newName User user = { name: β glee β , age: 1000 } rename(user, β not glee β ) β
This can get fairly messy to type check in various type systems.
Depth Subtyping Definition Instead of subtyping at the top level, could we subtype at the field level (and thus, their fields recursively)?
class LivingSpace: Animal resident class Studio: Human resident
\begin{align*}
&\texttt{class LivingSpace:}\newline
&\texttt{\qquad Animal resident}\newline
&\newline
&\texttt{class Studio:}\newline
&\texttt{\qquad Human resident}
&\end{align*}
β class LivingSpace: Animal resident class Studio: Human resident β β
Does Studio < : LivingSpace \texttt{Studio} <: \texttt{LivingSpace} Studio <: LivingSpace ?
Notice that these cannot have hierarchical relationships.
It might make sense logically that if our program requires a LivingSpace \texttt{LivingSpace} LivingSpace that we may provide it with a Studio \texttt{Studio} Studio since the latter can do anything the former can do (in this case, provide resident.name \texttt{resident.name} resident.name ).
func owner(LivingSpace home) β string: return home.resident.name Studio studio = { resident: { β some human β } } print(owner(studio))
\begin{align*}
&\texttt{func owner(LivingSpace home)} \rightarrow \texttt{string:}\newline
&\texttt{\qquad return home.resident.name}\newline
&\text{}\newline
&\texttt{Studio studio = }\lbrace\texttt{resident: }\lbrace- \textit{some human} -\rbrace\rbrace\newline
&\texttt{print(owner(studio))}
\end{align*}
β func owner(LivingSpace home) β string: return home.resident.name Studio studio = { resident: { β some human β }} print(owner(studio)) β
Caveat func reassignResident(LivingSpace home, Animal newResident): home.resident = newResident Studio studio = { resident: { β some human β } } reassignResident(studio, { β some animal β } )
\begin{align*}
&\texttt{func reassignResident(LivingSpace home, Animal newResident):}\newline
&\texttt{\qquad home.resident = newResident}\newline
&\text{}\newline
&\texttt{Studio studio = }\lbrace\texttt{resident: }\lbrace- \textit{some human} -\rbrace\rbrace\newline
&\texttt{reassignResident(studio, }\lbrace- \textit{some animal } -\rbrace)
\end{align*}
β func reassignResident(LivingSpace home, Animal newResident): home.resident = newResident Studio studio = { resident: { β some human β }} reassignResident(studio, { β some animal β }) β
Ah, so hereβs where it breaks down. We want to assign our subtyped field. But the true underlying structure requires more!
reassignResident \texttt{reassignResident} reassignResident is under the impression that an Animal \texttt{Animal} Animal is enough to fill up a LivingSpace \texttt{LivingSpace} LivingSpace , which is logically true. But if we pass reassignResident \texttt{reassignResident} reassignResident a Studio \texttt{Studio} Studio , it should really expect a Human \texttt{Human} Human instead of an Animal \texttt{Animal} Animal .
It turns out that the breakdown occurs because of aliasing . Thus, depth subtyping works with immutable structures (records).
Functions Introduction Functions are values. So how do we typecheck function assignment? Weβll reuse some types from above.
Mammal β Mammal someFunction = β¦ Mammal input = { β¦ } Mammal output = someFunction(input)
\begin{align*}
&\texttt{Mammal} \rightarrow \texttt{Mammal someFunction}=\ldots\newline
&\texttt{Mammal input = }\lbrace\ldots\rbrace\newline
&\texttt{Mammal output = someFunction(input)}
\end{align*}
β Mammal β Mammal someFunction = β¦ Mammal input = { β¦ } Mammal output = someFunction(input) β
The question is: what types can we assign to someFunction \texttt{someFunction} someFunction ?
Outputs Letβs trial and error, and try to reason the solution out.
Mammal β Human functionValue = β¦ Mammal β Mammal someFunction = functionValue
\begin{align*}
&\texttt{Mammal} \rightarrow \texttt{Human functionValue}=\ldots\newline
&\texttt{Mammal} \rightarrow \texttt{Mammal someFunction = functionValue}
\end{align*}
β Mammal β Human functionValue = β¦ Mammal β Mammal someFunction = functionValue β
functionValue \texttt{functionValue} functionValue returns a Human \texttt{Human} Human . Executions of someFunction \texttt{someFunction} someFunction expect a return value that can do everything a Mammal \texttt{Mammal} Mammal can do, which a Human \texttt{Human} Human satisfies. This works.
actualOutput < : expectedOutput \texttt{actualOutput} <: \texttt{expectedOutput} actualOutput <: expectedOutput
For sake of clarity, letβs try it the other way.
Mammal β Animal functionValue = β¦ Mammal β Mammal someFunction = functionValue
\begin{align*}
&\texttt{Mammal} \rightarrow \texttt{Animal functionValue}=\ldots\newline
&\cancel{\texttt{Mammal} \rightarrow \texttt{Mammal someFunction = functionValue}}
\end{align*}
β Mammal β Animal functionValue = β¦ Mammal β Mammal someFunction = functionValue β
Clearly, an execution to someFunction \texttt{someFunction} someFunction which expects a Mammal \texttt{Mammal} Mammal return type will miss out on the furColor \texttt{furColor} furColor attribute.
Again, letβs trial and error.
Human β Mammal functionValue = β¦ Mammal β Mammal someFunction = functionValue
\begin{align*}
&\texttt{Human} \rightarrow \texttt{Mammal functionValue}=\ldots\newline
&\cancel{\texttt{Mammal} \rightarrow \texttt{Mammal someFunction = functionValue}}
\end{align*}
β Human β Mammal functionValue = β¦ Mammal β Mammal someFunction = functionValue β
Clearly, whatever we provide as input must be able to do whatever someFunction \texttt{someFunction} someFunction requires of it. If we provide Mammal \texttt{Mammal} Mammal , functionValue \texttt{functionValue} functionValue expects a Human \texttt{Human} Human which might use attributes like occupation \texttt{occupation} occupation which arenβt present in Mammal \texttt{Mammal} Mammal .
Animal β Mammal functionValue = β¦ Mammal β Mammal someFunction = functionValue
\begin{align*}
&\texttt{Animal} \rightarrow \texttt{Mammal functionValue}=\ldots\newline
&\texttt{Mammal} \rightarrow \texttt{Mammal someFunction = functionValue}
\end{align*}
β Animal β Mammal functionValue = β¦ Mammal β Mammal someFunction = functionValue β
Providing someFunction \texttt{someFunction} someFunction with an input that can do at least what Mammal \texttt{Mammal} Mammal can do will allow it to safely be used as input to its value, functionValue \texttt{functionValue} functionValue .
expectedInput < : actualInput \texttt{expectedInput} <: \texttt{actualInput} expectedInput <: actualInput
Putting it All Together Itβs a little counterintuitive, but the inputs and outputs of a function subtype have opposite directionality (as we saw above).
Animal β Human functionValue = β¦ Mammal β Mammal someFunction = functionValue
\begin{align*}
&\texttt{Animal} \rightarrow \texttt{Human functionValue}=\ldots\newline
&\texttt{Mammal} \rightarrow \texttt{Mammal someFunction = functionValue}
\end{align*}
β Animal β Human functionValue = β¦ Mammal β Mammal someFunction = functionValue β
I β < : I O < : Oβ β
ββΉ β
βI β β
O < : Iβ β Oβ \begin{align*}
\texttt{I}&\texttt{β} <:\texttt{I}\newline
&\texttt{O} <:\texttt{Oβ}\newline
&\implies\newline
\texttt{I}\rightarrow\medspace&\texttt{O} <: \texttt{Iβ}\rightarrow\texttt{Oβ}
\end{align*} I I β β β <: I O <: Oβ βΉ O <: Iβ β Oβ β