8. Type Systems Flashcards
Type systems are most widely used form of static analysis. T/F
True
Motivation for type system (basic example of what it is/does)
required a boolean but you gave it a float.
Tried to return an array when the function expected to return an int.
What is a type?
A type is a set of values
int is a set of all integers between -2^31 and the opposite of that
Example of an abstract value. Represents a set of concrete values
More types
Foo is the set of all objects of class Foo List is set of all Lists of Integer objects
Abstraction
represents sets of concrete values as abstract values
In type systems, every concrete value is an element of some abstract value.
every concrete value has a type
english to inference rule for
if e1 has type int and e2 has type int, then e1+e2 has type int
(e1:int ^ e2:int)=> e1+e2 : int
Notation for inference rules
|-Conclusion
Inference rule axiom
|-e:t
something with no hypotheses but we know is true
Type judgement
Hypotheses and conclusions are type judgments that take the form:
|-e:t
|-
it is provable that
Schema
something very basic and template like.
|- i : int
i is integers
Rules for integers: inference rule for e1+e2
|-e1:int |-e2:int
————————- [Add] (name)
|-e1+e2 :int
Hypotheses state facts about ______
Conclusions state facts about ______
sub-expressions
entire expression
Bound variable
a variable in an expression that is defined within the expression
