CS 421 – Spring 2007Lecture Notes Set 12:User Defined Recursive TypesElsa L. Gunter1Transcribed by: Pooja MathurCorresponding to Slides: 07 - typederiv-1 (slides start - 40)Made available: February 16, 2007Revision 1.01 Change Log1.0 Initial Release.2 Types Systems (slide 2)Previously, we discussed creating types yourself. Infinitely recursive types, trees, etc. In this lecture, we will discusshow types can be used (data abstraction) and how they are interpretted (type checking)2.1 Terminology (slides 3-4)When we refer to a type t we are defining a set of possible data values that t can hold. So, for example, in C, a shortis an value in the set -215,...,215- 1. Booleans have a value in the set true, false. The values in this set are said to havetype t. So type systems are the rules in a language that assign types to expressions.We use these types to describe properties. For example, types can be used to define if data is read-write or read-only. We can use a type to decided if some operation has the authority to access the data. We can also check to seeif data came from the right place or that see if some operation might raise an exception. Like in Java, you can throwan input/output exception, as the signature of a method and that can be thought of as part of the type for that method.Most languages have the types describe the layout of the data and how they can be accessed.2.2 Sound Type Systems (slide 5)Types can guarentee us some amount of safety within a program. What this safey is, is a sound type system. It iswhere if an expression has some type t and then the expression evaluates to some value v, then we know that v is inthe set of values defined by the type t. OCaml has a sound type system, but languaages like C and C++ generally donot.2.3 Strongly Typed Languages (slides 6-7)If we are writing in a language, where when you apply an operator to some arguments, and there can be no run-timetype errors, the language is considered strongly typed. For example, 1 + 2.3 in OCaml will complain at compile time.It will tell you that you are using a float where there should be an integer.However, this is also a vague term and depends on the definition of type error. That is, C++ claims to be stronglytyped, but with Unions allowing types to be used in other places, type coercion causing undesirable effects, etc, somecall the claim to be false.OCaml is strongly typed, but still makes sure it does array bound checking, runtime type case analysis, etc.1c 2007, Share and Enjoy13 Type Checking3.1 Static vs. Dynamic Types (slide 8)A static type is a type that is assigned to an expression at compile time, where a dynamic type is a type assigned to astorage location at run time.So, statically typed languages (also known as typed languages) are those where every expression is staticallytype assigned at compile time. Dynamically typed languages (also known as untyped languages) where types of anexpression are determined at run time.3.2 What and when (slides 9-10)If we have an operation, applied to some arguments, type checking makes sure that we apply the operation to the rightnumber of arguments of the right types. Right type means that the argument has the same type as what was specifiedearlier or it means that the type used was a predefined implicit coercion. This is used to resolve overloaded operations.So, type checking may be done at two different times. It can be done statically at compile time, or dynamicallyat run time. Dynamically typed languages (like LISP and Prolog) do only dynamic type checking. Where staticallytyped languages (like C, C++, and Java) can do most of its type checking statically.3.3 Closer look at Dynamic Type Checking (slides 11-12)Here, there is no type checking at compile time. During run time, before an operation is performed, the type ofthe operation and the arguments are checked. The types of the variables and operations are all left unspecified untilruntime. There is an advantage to this, and that is the same variable can be used as different types. So for example,you started out using a variable as an integer, but later on, you wanted to redeclare it as a string. Dynamically typedlanguages will allow this.The disadvantages are that, the data object that you are using must hold the type information needed, since yourenvironment doesn’t have it. Also, since everything is done at runtime, some errors may not be detected until theerroneous part of the code is executed, which may not until years after the code was written.3.4 Closer look at Static Type Checking (slides 13-14)Static type checking is performed after parsing, but before running the program. So we parse the program and get it’ssyntax tree, and then we check to see if it’s type safe. Then if we find that it is type safe then we can throw out all thetype information because we already know that it is type safe and then start running the program.So an advantage is that once static type checking finds that a program is type safe, the information does not need tobe kept, because we know the program makes sense. So we get rid of the need to store that information like dynamictype checking needs. Static type checking also catches many program errors at early points. However, a problemarises because we can’t check types that depend on dynamically computed values, like array bound checking. Thathas to be done at runtime.This all depends on the idea that for every variable, every expression, every operator, their types have to be knownat compile time. This can either be done by type inference or by declaring variables. OCaml mainly does typeinference.3.5 Type Declarations and Inference (slide 16-17)A type declaration is the explicit assingment of types to variables or functions. But if you have type inference, typedeclarations are not needed. Type inference is a program analysis that infers the types for you. OCaml uses this, buttypes like Records cause problems for this.So, when you use the addtion operator, the +, OCaml sees it and says this operator works on two integers, so thatis what we are going to look for. Then OCaml also knows that after performing that operation, an integer should bereturned.24 Mathematics of Type Checking4.1 Type Judgements (slides 18-19)A type judgement looks like:Γ | - exp: τΓ is the typing environment, which supplies the types of variables and functions. It is a list in the form [x: σ,...].So, it has a list of variable names and associated types.The ’exp’
View Full Document
Unlocking...