This chapter build TFAE that extends FAE with static typing to help detecting run-time error related to type.
Errors are classified into three groups: expressions that evaluate to a value, expressions that never terminates, and, expressions that terminate but fail to produce the desired result (run-time error).
Detecting error while running the program is called dynamic analysis. However this approach fails for program that doesn’t terminate, has infinite cases, or are nondeterministic.
Detecting run-time error without executing programs are called static analysis. However making such program to do the analysis is undecidable and in general is very hard. To help such analysis, we introduce type system so that we can classify run-time error into type error and non-type error.
A type is a set of values with the same ability and structure. In FAE the only possible run-time error are type errors but other languages might have nontype-error.
(skipped, talked about dynamically vs statically type languages)
$$ e::=n\mid e+e\mid e-e\mid x\mid \lambda x:\tau .e\mid e\;e $$
Here, we define the metavariable for type value $\tau$:
$$ \tau::= \text{num}\mid \tau \rightarrow \tau $$
$$ \sigma \vdash \lambda x:\tau.e \Rightarrow \lang \lambda x.e ,\sigma \rang \quad \text{[Fun]} $$
sealed trait Expr
...
case class Fun(x: String, t: Type, b: Expr) extends Expr
sealed trait Type
case object NumT extends Type
case object ArrowT(p: Type, r: Type) extends Type