. General discussion of types
. What is a type?
. compile-time vs run-time checking
. conservative program analysis
(조금만 이상하면 그냥 틀렸다고 한다.)
compile time에 모든 것을 알 수는 없다.
(halting problem과 동치?)
. Type inference
. Good example of static analysis algorithm
. Will study algorithm and examples
. Polymorphism
. Polymorphism vs overloading
. Uniform vs non-uniform impl of polymorphism
. Type
. Semantic analysis에서 가장 먼저하는 것
. 최근 PL의 가장 큰 break through
. A type is a collection of computable values that share some structural property.
. well-define되는 것만 type이고 well defined 안되면 type이 아니다.
. type : well define된 value의 set과 그것들에 가능한 operation을 모은 것.
. 어떤 언어든 manual 처음은 각 언어의 primitive type을 설명함.
(그만큼 type이 중요하다는 뜻.)
. Uses for types (type check)
. Program organization and documentation
. seperate types for separate concepts
. represent concepts from problem domain
. Indicate intended use of declared identifiers
. Types can be checked, unlike program comments
. Identify and prevent errors
. Compile-time or run-time checking can prevent
meaningless computations such as 3 + true
. support optimization
. ex : short integers require fewer bits
. access record component by known offset
. type이 틀렸다면 아마 error일 것이다.
. type이 정해지면 field(layout)이 정해져서 structure에서 offset을 정할 수 있다.
. bit-pattern(binary representation)이 type이 있어야 의미가 결정된다.
. Type erros
. Hardware error
. Fuction call x() where x is not a function
(x가 적절한 address가 아니고 엉뚱한 instruction이다.)
. May cause jump to instruction that does not contain a legal op code
. Unintended semantics
. int_add(3, 4.5) - 다른 representation을 연산하면 당연히 이상한 값이 나온다.
. Not a hardware error, since bit pattern of float 4.5
can be interpreted as an integer
. Just as much a program erros as x() above
. General definition of type error
. A type error occurs when execution of program
is not faithful(충실하지 않음) to the intended(의도한) semantics
. Do you like this definition?
. Store 4.5 in memory as a floating-point number
location contains a particular bit pattern
. to interpret bit pattern, we need to know the type
. If we pass bit pattern to integer addition function,
the pattern will be interpreted as an integer pattern
. type error if the pattern was intended to represent 4.5
. Type system : type check를 하는 systme
. Type system을 통과했다. = type error가 없다.
= 우리가 원하는 semantic대로 움직인다.
물론 logic이 틀렸으면 다른 값이 나올 것이다.
. Compile-time(static check)
. run-time checkcing(dynamic check)
. Lisp uses run-time type checking
. (car x) make sure x is list before taking car of x
. ML uses compile-time type checking
. f(x) must have f:A->B and x:A
. Basic tradeoff
. Both prevent type errors
. Runtime checking slows down execution
. Compile-time checking restricts program flexibility
. Lisp list : elements can have different types
. ML list : all elements must have same type
. variable이 runtime에 type이 바귈까? 언어에 따라 다르다.
. Expressiveness(표현력)
. In Lisp, ew can write function like
(lambda(x) (cond ((less x 10) x) (T (car x))))
=> x가 10보다 크거나 같으면 9car 10)이 안되므로 type error
. some uses will produce type error, some will not
. dynamic하면 run-time check이면 expressiveness는 커지지만
어떻게 될지 모른다.
. Static typing always conservative(soundness)
. Cannot decide at compile time if run-time error will occur
(halting problem의 undecidability와 관련있다.)
. sound < A < completeness < U
. A : 우리가 check하는 성질
. sound and complete = A
. type check를 통과한 program
1. 내가 원하는 결과가 나오거나(옳은 결과)
2. 영원히 끝나지 않음.
. soundness : yes라고 말하면 반드시 yes
. completeness : yes인 것은 항상 yes라고 대답, no인 것도 가끔 yes로 대답할 수 있음.
. relative type-safety of languages
(type-safe language = sound = strongly typed)
. Not safe : BCPL family, including C and C++
. BCPL : 거의 type이 없다.
. Cast, pointer arithmetic(가장 악명높다.)
. Almost safe : Algol family, pascal, Ada.
. Dangling pointers (allocate는 문제 없으나 free가 문제)
. Allocate a pointer p to an interger, deallocate the memory
referenced by p, then later use the value pointed to by p
. No language with explicit deallocation of memory is fully type-safe
. Safe : Lisp, ML, Samlltalk, and Java
. Lisp, Smalltalk : dynamiclly typed(run-time)
. ML, Java : statically typed(compile-time)
. ML, Java는 pointer가 없고 reference만 있다.
. Type checking and type inference
. Standard type checking
. Look at body of each function and use declared types of identifies to check aggrement.
. Type inference
. Type을 안 적어도 알아냄.
. Look at code without type information and figure out what types could have been declared.
. ML is designed to make type inference tractable.
. Motivation
. Types and type checking
. Type systems have improved steadily since algol 60
. Important for modularity, compilation, reliability
. Type inference
. Cool algorithm
. widely regarded as important language innovation
. ML type inference gives you some idea of how many
other static analysis algorithms work
. Application
f(x)
@(f(x)) : r (parent)
f : s (left-child)
x : t (right-child)
s = t -> r
t : domain
r : range(codomain)
. Abstraction
lx.e
l : s->t (parent)
x : s (left-child)
e : t (right-child)
. Types with type variables
. Assign tpes to leaves
. Propagate to internal nods and generate constraints
(위로 propagete한다.)
. solve by substitution
. Use of Polymorphic function
. argument type에 따라 return type이 결정됨, 여러 종류를 넣을 수 있다.
. most general form - 더 general하게 적을 수 없다.
ex)
(int -> t) -> t : general form: 가장 simple하고 모든 것을 나타냄.
: (int -> int) -> int
: (int -> (s->t->r)) -> (s->t->r)
. Main points about type inference
. Compute type of expression
. Does not require type declarations for variables
. Find most general type by solving constraints
. leads to polymorphism
. Static type chcking without type specifications
. May lead to better error detection than ordinary type checking
. Type may indicate a programming error even if there is no type error
. ML에서는 type inference가 잘 되게 type system이 define되있다.
(C는 그렇지 않다.)
. Polymorphism vs overloading
. Parametric polymorphism(같은 algorithm)
. single algorithm may be given may types
. Type variable may be replaced by any type
. Overloading (다른 algorithm)
. A single symbol may refer to more than one algorithm
. Each algorithm may have different type
. Choice of algorithm determined by type context
. Types of symbol may be arbitrarily different
. Parametric Polymorphism : ML vs C++
. ML polymorphic function (implicit polymorphism)
. Declaration has no type information
. Type inference : type xpression with variables
. Type inference : substitute for variables as needed
. C++ function template(explicit polymorphism)
. Declaration gives type of function arg, result(type parameter의 name을 줌)
. Place inside template to define type variables
. Function application : type checker does instantiation
. ML also has module system with explicit type parameters
. Example : swap two values(polymorphism)
. ML : 모든 변수는 pointer임. (function이 1 copy면 됨.)
. swap is compiled into one function
. typechecker determines how function can be used
. C++ : stack에 들어가는 변수가 있기 때문에 swap function의 size가 달라짐.
. 그래서 type에 따라 function이 여러 copy가 필요함.
. swap is compiled into linkable format
. linker duplicates code for each type of use
. Why the difference
. ML ref cell is passed by reference(pointer), but
local x is on stack, size depends on type
. Another example
. C++ polymorphic sort function
. What parts of implementation depend on type?
. Indexing into array(type의 size가 다름)
. Meaning and implementation of <
. Swap
. ML Overloading
. Some predefined operators are overloaded
. User-defined functions must have unique type
(User defined는 polymorphic일 수는 있으나, overloading은 안됨)
. Why is a unique type needed?
. Need to compile code => need to know which +
. Efficiency of type inference
. Aside : general overloading is NP-complete
. Summary
. Types are important in modern languages
. Program organization and documentation
. Prevent program errors
. Provide important information to compiler
. Type inference
. Determine best type for an expression, based on
known information about symbols in the expression
. Polymorphism
. Single algorithm (function) can have many types
. Overloading
. Smbol with multiple meanings, resolved at compile time
. type
. a collection of computational entities that share some common property
. naming and organizing concepts
. making sure that bit sequences in computer memory are interpreted consistently.
. providing information to the compiler about data manipulated by the program
. type inference하는 법
. 일단 lambda calculus로 바꾼다.
. lambda lx.y
l이 parent가 됨 : s
left child는 bound variable(x) : t - node를 그리는 것이 아니라 leaf node와 잇는 다.
right child는 function body(y) : u
s = t -> u
. function : f(x) => f = x -> f(x) => lx.(f x)
@이 parent가 됨 f(x) : s
left child는 f : t
right child는 x : u
t = u -> s
. + : int -> int -> int
. recursive function의 경우 argument가 여러번 쓰이는 경우 lambda에서 여러개 잇고 각 node들을 같은 type variable로 적는 다.