Lecture 10: Exceptions, Type Checking ---- :::warning Announcements - **Please sit in the first 2 rows of the room**. - `A4: Static Types` due tonight (shorter than usual, extendable to Sunday) - `A5: Type Checking` out tomorrow - Quiz 1 grades back soon ::: :::success Agenda for today - Exceptions - Type checking (A5) - Dynamic vs. Static type checking - Type representations ::: # Exceptions Across many different programming languages _exceptions_ are used for handling "exceptional cases": almost always errors or other unexpected conditions. For example, in Java, null pointer exception indicate the exceptional case of trying to call a function on the `null` pointer instead of an actual object. Exceptions allow you to exit from a computation early and directly. Rather than proceeding with normal control flow, exceptions propagate errors back up the call stack. In OCaml, exception bindings declare new kinds of exceptions: ```ocaml (* New exception without any carried data *) exception NewException (* New exception that carries an int *) exception BadNum of int ``` Under the hood, there is one exception type, `exn`. Conceptually, defining an exception adds it as a variant of the `exn` type. ## Raising exceptions `raise` expressions throw an exception: ```ocaml raise NewException raise (BadNum -1) ``` `try...with...` expressions can catch exceptions (similar to `try/catch` blocks in Java). ```ocaml try e with NewException -> 0 try e with BadNum n -> n ``` ## Examples of using exceptions To walk through an example: ```ocaml exception NewException (* Want data passed along with my exception *) exception BadNum of int let divide x y = match y with | 0 -> raise (BadNum 0) (* _ is a wildcard: it matches anything, but creates no binding *) (* like "else" in Racket/plait: fallback case *) | _ -> x / y ``` Running this code gives: ```ocaml (* Normal, non-exception case *) utop # divide 4 2 ;; - : int = 2 (* Exception case *) utop # divide 4 0 ;; Exception: BadNum 0. (* Catch the exception with try/with *) utop # try (divide 4 0) with | BadNum n -> 0 ;; - : int = 0 (* Catching a different exception still raises *) utop # try (divide 4 0) with | NewException -> 0 ;; Exception: BadNum 0. (* But a non-exceptional case is still fine with the "wrong" one *) utop # try (divide 4 2) with | NewException -> 0 ;; - : int = 2 utop # try (divide 4 0) with | NewException -> 999999 ;; Exception: BadNum 0. (* We can use a wildcase if we don't care about the value *) utop # try (divide 4 0) with | BadNum _ -> 999999 ;; - : int = 999999 ``` :::danger Note: the exception name on its own (e.g., `BadNum`) produces *a value*, the exception itself, but *does not interrupt control flow*. To actually interupt control from, we need to `raise` the value (e.g., `raise BadNum`). ::: We need to `raise` to actually take the exceptional path: ```ocaml utop # NewException ;; - : exn = NewException utop # raise NewException ;; Exception: NewException. ``` :::success Why is it useful to have a distinction between the exception as a value, and raising the exception? ::: :::spoiler Think, then click! We might want to operate over exceptions, for example, having a match statement that produces different exceptions in difference cases to be raised later. ::: ## Evaluation and typing rules for `raise` :::info We raise (throw) exceptions with `raise e`. **Type-checking:** - `e` must have type `exn` - Result type is any type you want (!) **Evaluation rules:** - Do not produce a result (!) - Stop with normal control flow - Pass the exception produced by `e` to the nearest try expression on the call stack... (sort of like dynamic scope) ::: ## Evaluation and typing rules for `try/with` :::info `try... with ...` expressions can catch exceptions. **Evaluation rules:** - Evaluate `e1` - But if `e1` raises an exception and that exception matches the pattern, then evaluate `e2` and that is the result - Otherwise, `e1`'s value is the result **Type-checking:** `e1` and `e2` must have the same type and that is the overall type. ::: This brings up some interesting questions for whether code with exceptions type checks. We saw the following type checks: ```ocaml let divide x y = match y with | 0 -> raise (BadNum 0) | _ -> x / y ``` :::success What if we change the code to not use `raise` in the first branch? Does it still type check? ```ocaml= let divide x y = match y with | 0 -> (BadNum 0) | _ -> x / y ``` ::: :::spoiler Think, then click! No, this does not type check! It fails with the error: ```ocaml utop # let divide x y = match y with | 0 -> (BadNum 0) | _ -> x / y ;; Error: This expression has type int but an expression was expected of type exn ``` This is because while `raise`ing an exception has any type (because the code does not actually produce a *value* at all!), the exception itself has type `exn`. All branches of `match` must have the same type; but `exn` and `int` are different types. Thus, this code fails to type check. OCaml doesn't know the mistake is with the first arm of the `match`, so instead of reports the error on the `x /y` having type `int`. ::: Next, we'll think about type checking more broadly to lead into our next assignment. We'll use the OCaml exception syntax we just saw in our type checker, to give specific errors to the user based on what sort of type errors their code contains. # Type checking (Assignment 5!) :::success Recall from the start of our OCaml unit: what is the purpose of having static types? ::: :::spoiler Think, then click! Answers: - Self-documenting - Primary answer: prevent certain errors without even running the code. This can be especially useful when shipping code: static type checking covers all possible paths through the code (for all possible inputs). Dynamic checking only considers the paths that are actually taken. This means static types can help prevent customers seeing crashes "in the wild". - Potentially optimized interpretation/compilation. ::: ## Dynamic vs. Static type checking ### Dynamic type-checking - Examples: Racket, Python - Little/no static checking (only basic parsing/syntax checking) - If the program does something bad, like trying to treat a number as a function during evaluation, report error only then. - Check for type issues (e.g., invalid operator use) at runtime, report dynamic errors. E.g.: trying to add incompatible types, calling a function with the wrong number of arguments. - Halt actual program execution for most type issues :::danger - Cons: - Runtime checks can slow program execution - coverage: only catches errors on paths executed => could expose more crashes to customers ::: :::success - Pros: - Easier to implement (don't need a separate type checker) - Flexibility: programs that don't crash on the paths actually run are allowed to run successfully ::: ### Static type checking - Examples: Java, Rust, OCaml, Assignment 5 `MiniLangT` - Reject a program before it runs to prevent possibility of some classes of errors. - Part of the language definition :::success - Pros: - Reliability: considers all possible program paths. Does not crash already-running programs for many kinds of errors - Can speed up program execution: no need for runtime checks ::: :::danger - Cons: - Harder to implement - Overly conservative: restricts flexibility ::: ## Static vs. dynamic, conceptually When we say that static type checking is *conservative*, we mean that it might reject more programs than it actually needs to. Assignment 5 asks you to consider this for `MiniLangT` specifically. In general, for almost all interesting languages, we can think of the world of programs like this: ``` +--------------------------------------------------+ | all programs | | +------------------------------------------+ | | | programs that can run without | | | | dynamic errors | | | | +----------------------------------+ | | | | | statically type-checkable | | | | | | programs | | | | | +----------------------------------+ | | | +------------------------------------------+ | +--------------------------------------------------+ ``` That is, the set of all statically type-checkable programs is a subset of the set of programs that can run without dynamic errors. For most languages, that means there are programs that would run perfectly fine, but that are rejected by a static type checker. Assignment 5 asks you to write some of these for `MiniLangT`. ## Type checking analysis To type check a expression, we can think of it as the following: :::success 1. Either the expression has a type, in which case it "type checks". ::: :::danger 2. Otherwise, the expression does not have a type, in which case it "does not type checking" or equivalently, "has a type error". ::: ### Let's consider some examples Do the following OCaml expressions *type check*? `1 + 2` :::success This one is easy, yes! ::: `1.0 + 2` :::danger No, not in OCaml, we cannot `+` a float and an int. ::: `(fun x -> x + 1) true` :::danger This one is a bit harder: it does not type check. How did we know that? ::: We needed a *type environment* to know that `x` in the function body must have type bool. The type environment, also called a static environment, maps from variables to their type. Our conclusion is that types let us sanity check code, *without* actually running the code. In the logical extreme, this makes type checking *much* more efficient than running code. For example, code with an infinite loop takes an infinite amount of time when run under an interpreter: you never get an final value. But code with an infinite loop *can* be type checked, typically in linear time. Type checking only needs to look at each function (really, each expression) once, rather than every time it is dynamically executed. # Assignment 5: simple type checking For assignment 5, we'll focus on type checking a simple, statically typed language. We'll use the following *typed* version of `MiniLang`: `MiniLangT`! There are a few changes compared to the original MiniLang: - Static types! - No more `string` type/operations, no more `and`/`or` - Multi-argument `lambda` functions and `let` For simplicity, we will not have polymorphic types in MiniLangT. How, then, do we assign a type to the following? ``` (lam (x) x) ``` We can't! Thus, we do need _type annotations_ on function arguments, for example: ``` (lam (x : Int) x) ``` # Group exercise :::success Part 1: Design an OCaml recursive variant type to represent the types of values in MiniLangT: numbers, booleans, lists, or functions. Lists should be homogeneous. ::: :::success Part 2: Design an OCaml recursive variant type to represent the following cases of the grammar to an OCaml ``` <expr> ::= <num> | true | false | <var> | (+ <expr> <expr>) | (let ((<id> <expr>)+) <expr>) ``` ::: ## Solution :::spoiler Think, then click! The full solution to these two problems will be given to you in the stencil code for Assignment 5 (but it's good practice to derive them yourself!) For types, we'll add a `T` at the end to make it clear these are types. `BoolT` and `NumT` are the base cases. `ListT` and `FunT` need to be recursively defined, for their element types and argument/return types, respectively. ```ocaml type typ = | NumT | BoolT (* Element type *) | ListT of typ (* Type of the argument, then return type *) | FunT of typ list * typ (* Note: longer version provided in stencil code *) type expr = | BoolE of bool | VarE of string (* OpE defined in the stencil code *) | OpE of operator * expr * expr (* variable, then expression, then body *) | LetE of string list * expr list * expr ``` ::: Next class, we'll cover how OCaml handles more powerful type checking with the concept of *type inference*.