Types
- What are types?
- Types are properties of program values and the operations performed on those values.
- Types are a less-general and more succint form of logical predicates? Type-checking is similar to proving as in proof-carrying code.
- Type systems vary in expressiveness. More expressive --> more compile-time checks possible --> safer.
think Perl/Python vs. C/C++ vs. Java vs. Ocaml.
- Types in C? type ::= int | char | float | type * | type x type x ... x type (product) | union {type, type, type} (sum) | type(type) (function) | enum
- Other examples? type ::= string | Constructor of type | class (allows encapsulation)
- Polymorphic types (e.g., Ocaml, C++ templates): e.g., 'a -> 'a list ; 'a list -> int ; 'a * 'b -> 'a ; etc. e.g., list_length
- Implementation of polymorphic types may differ. e.g.,
- C++ generates multiple versions of a polymorphic function/data, one for each
type-level instantiation.
- OCaml uses runtime techniques, e.g., wrapping the polymorphic type through a layer of indirection.
- Many
languages also use just-in-time compilation to specialize polymorphic code at runtime. tradeoff: performance vs. program-size.
- Typed Assembly Language?
- Trickle down the type system from the higher-level language to the assembly language
- Type-checking the assembly program should prove the same properties as type-checking in the higher-level language
- The generation of types in the assembly program should be completely automatic --- using the "type compiler"
- Comparison with Proof-Carrying Code (PCC)?
- Automatic generation of types vs Manual instrumentation of logical predicates
- Actually, types are also manually annotated, albeit in the higher-level language
- Type annotations in high-level languages seem more natural/easier to humans, than predicate annotations. This is partly
because the programming language and the associated type system were carefully designed for ease-of-use.
- Some types are implicit in the grammar of the language. e.g., scoping.
- Much smaller annotations, less space requirement than PCC.
- Type-checking is usually much faster than proving
- Types are strictly less expressive than logic predicates. For example, PCC allows us to prove that a program
computes the factorial of its input. To achieve the same effect with types, one would need to design a rich type-system
that allows reasoning of relations between program values.
- Typed Assembly Language Example
- Use the sum example in TALx86 paper, which checks that argument and return values are integers.
- Motivate why types need to be associated with code locations. e.g., captures scope.
- Type checking involves checking that control flow can reach a code location, only if the corresponding type is satisfied
- Type checking also involves checking that opcodes operate on operands of correct types. e.g., integer type cannot be dereferenced.