감명 깊었던 programming language principles 6- 값 중심의 언어 - 정적 타입 시스템

오류 검증 문제

M3는 유용하지만 실행되서는 안되는 프로그램들이 있습니다. 실행중에 타입이 맞이 않아서 실행을 멈추게 되는 경우를 가진 프로그램들입니다.

타입

 - 프로그램을 기획하는 한 방법

 - 프로그래밍 언어가 그러한 기획을 물샐틈 없이 할 수 있도록 구성되어야 

  "너무 빡빡하지 않게" (PASCAL, PL/1, Algol68, Ada)

프로그램이 기획한 대로 실행된다는 것을 보장해야

프로그램 기획이 제대로 됬는지를 실행전에 검증 될 수 있어야 

검증이 자동으로 된다면...

M3 프로그램은 다섯종류의 값들이 있고 각각 분별력있게 흘러다녀야 합니다. 함수, 정수, 참/거짓, 쌍, 메모리 주소 입니다.

1. 함수 적용식  E1 E2  에서 식 E1은 함수여야 합니다. 

2. 덧셈식 E1 + E2 의 부품식들의 결과는 정수여야 합니다.

3. 조건식 if E1 E2 E3 에서 E1의 결과값은 참/거짓 이어야 합니다.

4. 쌍에서 첫번째 값을 뜻하는 식 E.1 에서 E의 결가값은 쌍이어야 합니다.

5. 메모리에 쓰는 식 E1:=E2 에서 E1의 결과 값은 메모리 주소여야 합니다.

M3 프로그램이 위와 같은 타입의 조건을 실행중에 항상 만족하는지를 미리 자동으로 검증하는 것이 가능했으면 하는 것입니다.

미리 static 안전하게 sound 검증하는 그러한 타입 시스템이 M3에 대해서는 가능합니다.

정적 타입 시스템 static type system

정적 타입 시스템은 말이 되는 프로그램인지를 프로그램 텍스트만으로 판단하는 한 방법입니다. 실행전에 말이죠.

이는 정적 의미 구조 static semantics 라고 부르기도 합니다. 이전까지의 의미구조들은 모두 동적 의미구조 dynamic semantics 였습니다.

일차적으로 문법 검증이 수행되는데, 

대부분 문법 구문은 아주 간단하기 때문에 문법 자체를 검증 하는 것은 쉽습니다.

그러나 프로그램은 문법 검증만으로 안전하다는 보장은 할 수 없습니다.

예를 들면, 아래와 같은 간략한 문법규칙이 있다고 합시다.

                          

문법 규칙이 간단하다는 것은 문맥을 생각하지 않는 규칙들이기 때문입니다.

+ 식은 두개의 부품식들이 정수식이어야 한다는 이런 문맥에 대한 조건은 "문법 규칙"에 표현하지 않습니다.

그래서  1+'a'는 문법상으로 정상이 되는 것입니다.

만약 이런 문맥에 대한 조건들을 표현한다면, 문법 규칙에서 "정적 타입 시스템"으로 은근 슬적 넘어가는 것입니다.

정적 타입 시스템 은 결국 일종의 정적 프로그램 분석(static program analysis)입니다.

대부분의 프로그램 분석이 그렇듯 정적 타입 시스템 역시 완전하지 못합니다.(incomplete)

그러나 안전하기는 합니다.(sound) 안전하도록 타입 시스템을 고안 해야 합니다.(우리 언어인 M3안에...)

정적타입 시스템은 형식 논리 시스템(formal logic)입니다. 논리식의 생김새, 논리식의 의미, 참인 논리식을 기계적으로 추론하는 규칙들 proof rules 또는 inference rules라고 불리는 것들 을 이용하여, 안전성과 완전성을 증명하는 논리 식들로 구성하는 것입니다.

그렇게 디자인이 끝나면, 구현합니다. 

구현된 타입시스템은 대상 프로그래밍 언어로 작성된 임의의 프로그램을 입력으로 받아 타입 오류가 있을지 없을지를 검증합니다.

구현되는 알고리즘이 디자인 한 타입 시스템을 제대로구현한 것이라는 사실도 확인하게 됩니다. 디자인에서 구현까지 단단한 과정을 밟는 것입니다.

형식 논리 시스템(formal logic) 리뷰

형식 논리 시스템은 논리식 집합의 정의, 논리식 의미의 정의,  참논리식 집합의 정의, 참논리식 추론의 방법, 추론방법 평가하기

로 구성됩니다.

선언 논리 (propositional logic) 시스템을 보자. 논리식 집합은 다음과 같은 귀납 규칙으로 정의됩니다.

                                    

논리식의 정의는 다음과 같고,

                    

 

참인 논리식들의 집합을 정의합니다 

: 즉, 쌍 ({f1,...,fn},f)    (표기 : )들의 집합입니다.

참인식 

들의 집합들.

        

                          

        

                       

                                

이 규칙들은 참인 식을 만드는 규칙이고, 이것을 논리 시스템에서는 추론규칙 inference rules 혹은 증명규칙 proof rules 라고 합니다.

여기서 살짝 다른 관점에서 보자면, 참인 논리식 집합을 만드는 과정은 곧 참 논리식을 유추한 증명을 만드는 과정이기도 합니다. 증명들의 집합을 만드는 귀납규칙으로보는 것입니다. 

증명규칙으로 만들어지는 증명을 증명 나무 (proof tree)라고 합니다.

이제 이렇게 "기계적인" 증명규칙 혹은 추론 규칙이 정말 좋은가를 따져봐야 합니다.

추론 규칙의 안전성 soundness

추론 규칙의 완전성 completeness

단순 타입 시스템 simple type system

M0 로 모든 것을 프로그래밍 할수 있겠으나, 값은 오직 함수 밖에 없었습니다. 값의 타입으로 함수와 정수만 있는 M1 코어만 생각합시다.

                                

위의 의미 규칙

                                

를 사용할 수도 있으나, 타입 시스템의 안정성 증명에서 편리한 방식을 위해서 프로그램 텍스트를 다시 써가는 방식의 의미에서, 

의미는 같지만, 실행 문맥 evaluation context을 이용하여 다음과 같이 정의 합니다.

실행 문맥은 적극적 실행 Eager evaluation 순서에 준해서 다음에 실행해야 할 부분을 결정됩니다.

프로그램 실행 규칙은 다음과 같습니다.

                             

                          

                                  

프로그램 E의 의미는 위의 규칙에 따라

            

                                     

단순 타입 추론 규칙

타입시스템을 정의합시다.

다시 한번 강조 하지만, 프로그램 텍스트만을 가지고 타입 오류 없이 실행되는 프로그램인지를 검증하는 논리 시스템입니다.

-프로그램 텍스트에 타입이 명시된것은 없습니다.

 하지만 논리시스템은 프로그램 구석구석의 타입이 어떻게 기계적으로 유추될 수 있는지를 정의합니다.

                  

논리식의 생김새는 

                             

입니다.

Γ(gamma)는 타입 환경 type environment 으로 변수들의 알려진 타입을 가지고 있습니다.

                    

타입환경 Γ에 대해서 Γ{x⟼τ} 대신 Γ+x:τ로도 씁니다.

x⟼τ ∈ Γ 대신에 x:τ ∈ Γ 로도 쓸 것입니다.

논리식의 의미는

                  [[ Γ⊢E:τ]]= true

                              iff

    

                 : ∀σ ⊨ Γ.E 이 영원히 돌든가, 값을 계산 E→*υ 하면 ⊢υ:τ

입니다.

이제 참인 논리식을 유추하는 규칙을 정의합니다.

타입 추론 규칙 type inference rules

                                          

                                         

                                

                     

이 식을 이용해서 실제 타입들에 대해서 증명과정에 대해서는 생략...

1. 식 E의 생김새마다 오직 하나의 규칙이 있다.

 이 사실은 증명규칙의 성질을 증명할 때 우리를 편하게 합니다.

예를 들어

이런 식이 유추 되었다면, 반드시 한 경우밖에 없습니다. : 

의 타입 유추 규칙이 하나 밖에 없으므로, 그 규칙에 있는 조건이 만족한 경우 밖에 없습니다.

즉, 

이면   

           이면 

                                             :

2. 어떤 식 E에 대해서, Γ⊢E:τ 인 τ값이 여럿 가능하다.

3. 문제 없이 실행되는 프로그램이 타입 유추가 불가능한 경우가 있다. 완전 complete 하지는 못한 것이다.

추론 규칙의 안전성

우리는 추론 규칙의 안전성 soundness은 증명할 수 있습니다.

즉, 타입 추론이 성공하면 그 프로그램은 타입 오류 없이 실행된다는 것이 보장됩니다.

즉, 프로그램(자유변수가 없는 식) E에 대해서

                                   

이 추론될 수 있다면, 프로그램 E는 문제 없이 실행되고 , 끝난다면 결과값 τ 타입이라는 것입니다.

두가지 증명법

1. 안정성을 증명하는 한가지 방법.

- Progress Lemma: 값이 나올 때 까지 문제 없이 진행한다.

               ⊢e:τ 이고 e가 값이 아니면 반드시 e → e'

- Subject Reduction Lemma : 진행은 타입을 보존한다.

               ⊢e:τ 이고  e → e' 이면  ⊢e':τ

2. 안정성 증명하는 두번째 방법.

- E → error 를 정의합니다.

- Subject Reduction Lemma : "진행은 타입을 유지한다", 를 증명합니다.

      ⊢E:τ 이고 E→ E' 이면 ⊢E':r 이다.

- 안정성이란, 값이 아닌 식 E가 타입이 있으면, E는 문제없이 진행하며 끝난다면 그 타입은 값이어야 한다.

- 값이 아닌 식 E가 타입이었다고 하자. 잘 진행하는가?

   그렇다, E→error로 진행할 수 없다. 왜냐하면, 그렇게 진행한다면 "Subject Reduction Lemma"에 의해서 모순이기 때문이다. error가 타입이 있어야 하는데 error의 타입을 결정하는 규칙은 없기 때문이다.

- 그리고 진행이 타입을 항상 보존하므로, 값으로 진행이 끝나게 되면 그 값도 같은 타입을 가진다.

이 단순 타입 시스템은 논리시스템으로 우리가 바라는 바를 가지고 있음을 증명할 수 있었습니다. 

다음 단계는 구현입니다. 하지만 간단해 보이지 않습니다. 다음 규칙을 보면 말이죠.

                                        

함수 몸통 E를 타입 유추하려면 인자의 타입 τ1을 알고 있어야 합니다. 그러나, τ1은 우리가 최종적으로 유추해야 할 함수 타입의 일부입니다.

어디서 본듯한 패턴입니다. 유추해야 할것을 미리 알고 있어야 한다.!!! 유추를 포기한다? 프로그래머에게 함수마다 타입을 기입하라고 해야 할까?

이번에는 놀라운 방식이 있습니다. 타입에 대한 연립방정식을 세우고 풀어가는 과정입니다.

그 과정이 놀라운 이유는 ,우선 타입을 자동으로 유추해 주는 알고리즘 때문입니다. 프로그램 텍스트에 타입에 대해서 프로그래머가 아무것도 명시할 필요가 없습니다. 자동으로 유추되기 때문입니다.

또다른 이유는, 타입 시스템을 충실히 구현한 알고리즘이기 때문입니다. 충실히?? 타입 시스템이 유추할 수 있는 것을 그 알고리즘은 똑 같이 유추해줍니다. 그 반대도 성립합니다. 알고리즘이 유추해 내었으면 타입 시스템도 같은 것을 유추해 낼 수 있습니다. 서로 iff관계로 논리시스템과 구현 시스템이 물려 있습니다.

예를 들면,

   1+(λx.x 1)0

이런 식이 있다고 합시다.

 각 부품(파트) 별로 번호를 붙여봅시다.

부품식 i 가 가져야 하는 타입 αi 와 변수 x가 가져야 하는 타입 αx에 대한 방정식 "lhs ≐ rhs" 는 다음과 같습니다.

위의 방정식의 해는 없다.  αx 는 ι(iota 요타)이기도 해야 하고 ( α≐ αx 로부터) ι →ι이기도 해야 하므로 ( α6≐ αx 로부터)

타입 연립 방적식 u는 다음과 같은 모습입니다.

타입 방정식

연립

타입변수

타입 연립 방정식의 해 S를 치환으로 표현하면 편합니다. TyVar을 Type으로 바꾸는 것입니다.

                                      :A->fin B  = A에서 B로 가는 치환들의 집합입니다. 

따라서 TyVar에서 Type으로 가는 집합을 의미합니다.

온라인 알고리즘들

타입 방정식을 도출하면서 그때 그때 풀어가는 알고리즘도 가능합니다.

안전한 그러나 경직된

단순 타입 시스템은 안전하긴 하지만 아쉬움이 많습니다.

완전하지 못하다. 타입 오류 없이 잘 실행될 수 있는 모든 프로그램이 단순 타입시스템을 통과 할 수는 없습니다.

인자 타입에 상관없이 실행되는 함수들이 많이 있습니다.

안전하지만 빠뜨리는 프로그램들이 있는 것입니다.

재귀 함수

재귀 함수는  Y 컴비네이터  (Y combinator)를 통해서 표현할 수 있습니다.

                              :Y 컴비네이터

이 핵심 부분은 자신을 인자로 받는 함수의 적용  "x x"입니다.

단순 타입 시스템에서는 함수가 자신을 인자로 받는 식은 타입 유추가 될 수 없습니다.

                             

각 부품식 i가 가져야 하는 타입 αi를 따져보면,

이 되는데, 결국 α→β≐α를 만족하는 타입을 Type에서는 찾을 수 없습니다.

unification  알고리즘은 위의 양변을 같게 만드는 α와 β를 찾는 것에 실패한다.

단순 타입시스템이 갖추어진 언어에서는 재귀함수를 Y 컴비네이터로 표현해서는 타입 시스템을 통과할 수 없습니다.

때문에 재귀함수인

                                      

은 필수가 됩니다. (더이상 설탕이 아닙니다.)

메모리 주소 값

메모리 주소를 값으로 사용하는 경우는 타입 시스템을 어떻게 확장할 수 있을까?

                                   

우선 타입의 종류가 하나 늘어납니다.

1. 타입 τ loc 는 메모리 주소타입인데, 그 주소에는 τ 타입의 값이 저장되는 타입입니다.

그리고, 타입 규칙들은 자연스럽게 확장됩니다.

다형 타입 시스템

단순 타입시스템을 정교하게 확장하자.. 안정성을 유지하면서 "잘 모르겠다"고 하는 경우를 줄입니다.

안전하면서 유연한 타입시스템이 필요합니다.

다형 타입 시스템(polymorphic  type system)이 바로 그러한 타입시스템입니다.

타입 유추가 가능하고 실제 언어에 실용적으로 구현될 수 있는 다형 타입 시스템이 let-다형 타입 시스템입니다.

타입 시스템에서 

"잘 모르겠다" = "타입방정식의 해가 없다" 즉,

이런경우 ⊢p 는 ⊢를 포섭하면서 확장한 경우라고 합니다.

다형 타입 시스템에서 "잘 모르겠다"고 하는 경우가 단순 타입 시스템 보다는 적습니다.