Lecture 11: Type Checking

목차

Learning Objectives

- Explain the difference between a type system and a type checker

- Analyze programs as being well-typed or ill-typed

- Explain and motivate "type safety"

- Implement a simple type checker for a language with let expressions

 

 

Why Type Check?

Type checking helps rule out errors

Example: 

 

 

Type System vs Type Checker

A type system is a specification of a set of syntactic restrictions on well-formed programs

A type checker is an implementation of a type system

E.g. the program on the right is syntactically well-formed according to the grammar, but may not be well-typed.

 

Type system: syntactic restrictions: they characterize what programs are well-typed based on the syntax of the program

 

 

Well-Typed?

 

1. Well-typed (Type checked)

2. Won't type check because we are using integer where boolean is expected

3. Depends on what x is. (If x is defined and is integer, it is well-typed) String is also fine → concatenation

 

Well-Typed?

1. Scala can't decide if it knows what x should be. Cannot infer the type of x (Need more information)

2. Type checked (well-typed). 만약에 return type 없으면: Doesn't type check: fac needs return type

3. Not well-typed: could not infer the type of self. 

 

Typing is subtle (미묘한) 

How do we specify what it means for a program to be well-typed? 

→ Type system

 

 

 

 

Γ: type context 

1. n is well typed and has the type Num

2. Plus expressions: (+ e1 e2) is well typed and has the type Number if e1 has type number and e2 has type number

3. Let expression is well-bound if it has t2 whenever e1 has type t1 under the same type context as the original let expression 

Once I know that e1 has type t1 then I know the e2 has type t2 under the type context where I extend the type context by adding x with type t1. 

4. If we encounter a variable x has some type t if I look in the type context and find x has type t 

 

Not well-typed according to the type context as Num is required

 

 

Type Safety

Type safety is a formal statement that characterizes what behaviors a type system is supposed to rule out

For example, the two typing rules below for arithmetic expressions rule out a runtime type error

 

nv: well typed and correspond to the type context

 

 

여기를 보면 다음과 같은 것들을 알 수 있다.

1. nil의 타입은 List t이다

2. (cons e1 e2)의 타입은 List t이다.

3. (cons e1 e2)에서 e1의 타입은 t여야하고 e2의 타입은 List t이어야 한다 (nil도 가능).

따라서, (cons 1 2)는 not well-typed이고 (cons  1  (cons  2  nil))은 well-typed.

4. e가 List t일 때, (head e)의 타입은 t가 된다.

5. e가 List t일 때, (tail e)의 타입은 Lsit t이다.

 

 

For Scala:

Any well-typed program either:

- returns a value of the expected type

- throws a programmer-raised exception

- crashes with a pattern match failure

- crashes with an invalid cast exception

- non-terminates

 

 

Casting in Scala

→ In Scala, we can cast any value of any type to anything else  (C는 B와 아무 관련이 없어도 Cast는 가능)

 

D.b 하면 error (crashes with an invalid cast exception)

 

 

 

Casting in Java

 

 

Type Safety for Java

Any well-typed program either:

- returns a value of the expected type

- throws an unchecked exception

- crashes with an invalid upcast exception

- non-terminates

 

 

 

Type Checking vs Type Inference

Specifying types can be automated

Type inference lets us infer the type of programs, without having to provide type hints up-front

 

 

Type Inference in Scala

 

 

 

Type Inference in Haskell

 

 

 

Typing Concerns

Type safety = the guarantee we get from a type system

A type checker is:

- Sound if it only accepts programs that are well-typed according to the type system it implements

- Complete if any program that is well-typed according to the type system is also accepted by the implementation

Type checking is undecidable if we cannot write a type checker that is both sound, complete, and guaranteed to terminate

 

 

Code

tnv: TEnv (Type Environment)

Purpose of function tc: Given an expression e and type environment tnv, should return a type or runtime exception.

 

sealed abstract class Expr
case class Num(i: Int) extends Expr
case class Plus(e1: Expr, e2: Expr) extends Expr
case class Let(x: String, e: Expr, body: Expr) extends Expr
case class Id(x: String) extends Expr
case class True() extends Expr
case class False() extends Expr
case class If(c: Expr, t: Expr, e: Expr) extends Expr

// NEW
case class Fd(x: String, t: Type, e: Expr) extends Expr
case class App(e1: Expr, e2: Expr) extends Expr


sealed abstract class Type
case class NumT() extends Type
case class BoolT() extends Type

// NEW
case class FunT(params: List[Type], ret: Type) extends Type

def tc(e: Expr, tnv: List[(String, Type)]): Type = e match {
  case Num(i) => NumT()
  case Plus(e1, e2) => (tc(e1, tnv), tc(e2, tnv)) match {
    case (NumT(), NumT()) => NumT()
    case p =>
      throw RuntimeException("plus expression expects two numbers, but type checking found: " + p)
  }
  case Let(x, e, body) => {
    val t1 = tc(e, tnv)
    tc(body, (x, t1) :: tnv)
  }
  case Id(x) => lookup(x, tnv)
  case True() => BoolT()
  case False() => BoolT()
  case If(c, t, e) => tc(c, tnv) match {
    case BoolT() => (tc(t, tnv), tc(e, tnv)) match {
      case (t1, t2) if t1 == t2 => t1
      case p => throw RuntimeException("expected branches of if-expression to have the same type, but type checking found: " + p)
    }
    case t => throw RuntimeException("expected condition of if-expression to be boolean typed, but type checking found: " + t)
  }
  case Fd(pxs, e) =>
    val t1 = tc(e, (x, t) :: tnv)
    FunT(t, t1)
  case App(e1, e2) =>
    // check that e1 has type t1 -> t2
    // check that e2 has type t1
    // return t2

}

def lookup(x: String, tnv: List[(String, Type)]): Type = tnv match {
  case Nil => throw RuntimeException("error - free variable: " + x)
  case (y, t) :: tnv if (x == y) => t
  case _ :: tnv => lookup(x, tnv)
}

 

 

1. case Num(i) → just return NumT()

2. case Plus(e1, e2) → if type of e1 is NumT() and e2 is NumT(), return NumT(). Otherwise, exception

3. case True(), False() → they are both boolean so return BoolT()

4. case If(c, t, e) → first type check c and if it's boolean, check if t and e have the same type. If they do, return that type. Otherwise, exception.