[PL]Ch.6 - Types

. 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로 적는 다.