Type Safety에 대한 정의에 대해 완전한 이해를 위해 포스팅을 준비하던 중, PL Enthusiast 블로그에서 너무 좋은 글을 찾게 되었다. 따로 정리할 필요없이 본 포스팅에서는 해당 글에 대한 이해와 번역을 한글로 정리한다.
Type Safety는 잘 이해되는 개념이지만, 쉽게 고정되는 개념은 아니다. 특히 누군가 "JAVA는 Type-safe한 언어다."라고 하면 이는 정확히 무엇을 의미하는가? 모든 종류의 Type-safe한 언어들은 어떤 면에서 "같다"고 볼 수 있는가? Type-safe의 개념은 특정 언어에서, 그리고 일반적으로 어떻게 받아들여지는가?
사실, Type Safety의 개념은 해당 언어의 타입 시스템의 정의에 따라 달라진다. 가장 간단한 예시로, Type Safety는 프로그램의 행동이 잘 정의된 것을 보장한다. 보다 일반적으로, Type Safety는 해당 프로그램의 correctness와 security를 추론하는 데 강력한 도구가 된다.
기본적인 Type Safety
Type Safety의 개념을 직관적으로 풀어써보면 "Well-typed 프로그램은 잘못되어질 수 없다."는 것이다. 이 표현은 1978년 Robin Miller의 논문 'A Theory of Type Polymorphism in Programming'에서 만들어진 것이다. 이제 그 의미를 본격적으로 파헤쳐보도록 하자.
잘못되어지는 것
프로그램 언어는 개발자가 작성하도록 허용된 Syntax와 작성된 프로그램이 가지는 의미인 Semantics로 정의된다. 모든 프로그램 언어는 Syntatic하게는 옳지만, Semantics가 옳지 않은 문제를 겪는다. Chomsky 고전의 문장인 “Colorless green ideals sleep furiously”는 문법적으로는 아무런 문제가 없지만, 이는 아무런 의미가 없다. OCaml 언어로 예를 들어, 1 + "foo"; 는 프로그램의 Semantic를 따져보았을 때 아무런 의미가 없다. 다른 예시는 C 언어의 { char buf[4]; buf[4] = ‘x’ } 이다. 이것 또한 버퍼의 범위 밖의 인덱스 4에 쓰기 접근을 하기 때문에 언어의 정의는 이러한 행동을 undefined behavior: 의미없는 것으로 분류한다. 이러한 의미없는 프로그램을 우리가 실행하게 된다면, 프로그램은 잘못된 행동을 야기할 것이다.
Well-typed ⟹ 잘못되어질 수 없는
Type-safe한 언어의 세계에서는, 언어의 타입 시스템이 특정 방법으로 "옳은"(잘못되어지지 않는) 프로그램만을 받아들인다. 특히, 우리는 타입 시스템이 받아들인 프로그램을 Well-typed라고 하고, Type-safety는 이러한 프로그램이 절대로 잘못되어지지 않음을 보장한다(그 프로그램들은 Well-defined된 프로그램 행동을 가진다). 이를 시각화하면 아래와 같다.
Type-safe한 언어의 세계에서, Well-typed 프로그램은 Well-defined 프로그램의 부분 집합이 된다.
어떤 프로그램 언어가 Type-safe할까?
이제 본격적으로 대중적인 프로그램 언어들이 Type-safe한지 아닌지를 다루어본다. 이 파트에서는 서로 다른 언어를 다루는데, 그들 간 Type-safety의 의미는 서로 달라질 수 있다.
C/C++ : Type-safe하지 않음
C의 표준 타입 시스템은 코딩 스탠다드나 개발자의 일반적인 상식에서 의미없다고 판단하는 프로그램을 배제시키지 않는다.(e.g. 버퍼의 인덱스를 벗어난 프로그램) 그러므로, C언어에서는 Well-typed된 프로그램도 잘못되어질 수 있다. 그리고 사실상 C의 상위 집합인 C++은 이러한 C의 타입 불완전성을 상속받는다.
JAVA/C# : Type-safe(아마도)
계속 발달한 언어의 구현이 Type-safe한지 확신하는 것은 꽤 어렵지만,(e.g. 초기버전 자바의 Generic은 buggy했다.) 좀 더 형식화된 대표격 언어들은(Featherweight JAVA) Type-safe하다고 할 수 있다. 재미있는 점은, Type Safety의 개념은 C의 Semantics에서는 정의되지 않았던 것들이 이들 언어에서는 의미가 주어진 점에 착안한다. 예를 들어, C 프로그램에서 배열의 범위 바깥에 접근하는 행동은 정의되지 않은 것이지만, JAVA나 C#에서는 정의되어 있다.(이 경우, 프로그램이 ArrayBoundsException을 던질 것이다.)
Python/Ruby : Type-safe(틀림없이)
파이썬이나 루비는 종종 Dynamically-typed된 언어로 구분된다. 이들은 타입 에러를 알리기 위해 실행시간에 발생하는 타입 에러에 대해 예외를 던진다. 자바가 배열 오버플로우에 대해 ArrayBoundsException를 던지는 것처럼, 루비는 스트링 타입과 정수 타입에 더하는 연산을 할 때, 예외를 던질 것이다. 두 경우 모두, 이러한 프로그램 행동은 언어의 Semantics에 의해 규정되어있기 때문에 Well-defined라고 할 수 있다. 사실상 언어의 Semantics가 거의 모든 프로그램의 행동을 잘 정의하기 때문에 이 경우의 밴다이어그램의 원들은 모두 일치한다고 볼 수 있다. 따라서 이러한 언어를 null 타입 시스템에 따라 Type-safe하다고 할 수 있다.(받아들이는 모든 프로그램이 잘못되어지지 않는: 밴다이어그램의 원 세개가 일치하는). 그러므로 Type-safe하다.
이 결론은 이상해보일 수도 있다. 자바언어에서, 프로그램 o.m()이 Well-typed라면, Type Safety는 o가 메서드 m에 대해 인자를 받지 않는 오브젝트라는 것을 보장하고, 함수의 호출은 성공할 것이다. 루비언어에서, 루비의 타입 시스템에 Well-typed된 프로그램 o.m()를 실행한다면, o가 메서드 m을 정의한다는 것을 보장할 수 없으며 호출이 성공할 수도, 예외가 발생할 수도 있을 것이다.
간단히 말해, Type Safety는 단순히 한가지를 의미하지 않는다는 것이다. 그것이 보장하는 것은 언어의 Semantics에 따라 달라지며, 잘못된 행동을 내포할 수도 있다. 자바언어에서, 존재하지 않는 메서드를 호출하는 것은 잘못된 행동이다.(컴파일에 실패할 것이다.) 루비언어에서는 그렇지 않다.(단순히 예외를 발생시키고 말 것이다.)
좀 더 심화적으로
일반적인 개념의 Type Safety는 유용하다. 그게 없다면 우리는 프로그램이 정의된 행동대로 정상적으로 동작할지 알 수 없고, 어떤 경우에서는 아무런 종류의 행동도 가능해질 수 있다. C/C++의 정의되지 않은 행동(Undefined behavior) 허용은 무수한 보안 취약점의 원천이 된다.(Stack smashing부터 Format string attack같은) 이러한 취약점은 Type-safe한 언어에서는 불가능한 것이다.
반면에, 자바와 루비의 비교가 보여주듯이, 모든 타입 시스템이 동일하게 만들어진 것은 아니다. 몇몇은 몇가지 행동을 보장할 수 있고, 없다. 이와 같이, 우리는 언어가 Type-safe한 지만을 볼 것이 아니라, 해당 언어의 Type Safety의 의미에 대해 생각해보아야 할 것이다.
간극 좁히기
밴 다이어그램 안 Well-defined와 Well-typed 원은 일치하지 않는다. 두 원의 사이에는 Well-defined되었지만 타입 시스템에 의해 거부되는 프로그램들이 존재한다. 예시를 하나 들자면, 대부분의 타입 시스템은 해당 프로그램을 받아들이지 않을 것이다.
https://gist.github.com/Bloofer/102392761416f25c080e8b541f474d67
위 프로그램은 항상 정수를 내놓지만, 타입시스템은 이를 거부한다. 왜냐하면 변수 x가 문자열 타입과 정수 타입으로 모두 사용되었기 때문이다. 정적분석을 빗대어 설명하자면, 타입 시스템은 Sound하지만 Incomplete하기 때문이다. 이러한 Incompleteness가 개발자에게 혼선을 준다.(그리고 아마 이러한 점이 루비나 파이썬같은 Dynamic 언어로 그들을 이끌 것이다.) 해결책은, 이러한 간극을 좁히고, 더 많은 프로그램을 타입 시스템이 받아들이도록 하는 것이다.
현실의 예시를 들어보자면, 자바의 타입 시스템은 1.5버전에서 generics의 개념과 함께 확장되었다. 자바 1.4 버전에서는 1.5 버전에 반하여 타입 시스템을 통과하기 위해 타입 캐스팅이 필요한 경우가 몇몇 생길 수 있다. 또 다른 예시로 함수형 프로그래밍 언어의 근간인 Lambda Calculus를 생각해보자. Lambda Calculus는 Milner의 polymorphic 타입 시스템보다 적은 수의 프로그램을 받아들일 것이고, Milner의 타입 시스템은 Rank-2(혹은 보다 높은) polymorphism보다 더 적은 수의 프로그램을 받아들일 것이다. 표현력이 강하고(Complete하고) 사용성이 좋은 타입 시스템의 디자인에 대해 많은 연구자들이 고민한다.
Invariant 활용하기
보편적인 언어들은 int나 string같은 타입들을 가진다. Type Safety는 int의 표현식들이 실제 실행시간에 -1, 2, 47과 같은 값으로 평가됨을 보장한다. 이 뿐만 아니라 타입 시스템은 더 많은 종류의 타입을 지원하여 프로그램의 표현을 더 풍부하게 만들 수 있다.
예를 들어, 최근 Refinement Type에 대한 연구 커뮤니티에서의 관심이 증가하였는데, 이는 논리식을 사용하여 타입의 가능한 값 집합을 구체화하는 것이다. 타입 {v: int | 0 <= v}는 int 타입을 논리식 0 <= v로 구체화하고, 결과로는 음수가 아닌 정수 타입을 정의한다. Refinement Type을 사용하면 프로그래머는 해당 자료구조 유형의 자료구조 Invariant를 표현할 수 있으며, 이러한 Type Invariant들로 항상 불변의 값들을 알 수 있다. Refinement 타입 시스템은 Haskell과 F#에서 개발되었다.
또 다른 예시로, 우리는 타입 시스템을 변수보호 락을 소유한 쓰레드가 공유 변수에만 접근한다는 불변성을 이용하여 Data race 문제를 해결할 수 있다. 공유 변수의 타입은 이를 보호하는 락을 표현한다. 안전한 락을 위한 타입은 Abadi와 Flanagan에 의해 처음 제안되었으며 Java 및 C 용 구현이 개발되었다.
타입 추상화와 정보 숨기기
많은 프로그래밍 언어는 프로그래머가 데이터 추상화를 할 수 있도록 지원한다. 이러한 언어는 클래스, 모듈 또는 함수의 추상화로 내부 코드를 사용하는 클라이언트 코드에서 숨겨지도록 한다. 이렇게하면 내부 코드가 클라이언트 코드에 영향을 미치지 않고 변경될 수 있어 보다 강력하고 유지보수가 쉬운 프로그램이 될 수 있다.
타입 시스템은 추상화에 중요한 역할을 할 수 있다. 예를 들어, 잘 설계된 타입 시스템의 도움으로 Representation Independence를 증명할 수 있다. 프로그램은 구현 방식이 아닌 추상화 동작에만 의존한다. 이는 John Reynolds의 1983년 논문에서 가장 잘 설명되었다. 논문에서 그는 "Type Structure는 추상화 수준을 유지하기위한 구문적 규칙"이라 말하면서 타입이 유지보수 가능한 시스템을 구축하는 주춧돌이 된다고 말한다.
출처 : PL-Enthusiast 블로그
