교토대에서 프로그래밍 언어 수업을 들으면서 이가라시 교수님 수업을 들으며 관련 책을 좀 보았는데, 인상적이었서서 소개해볼까 한다. 프로그래밍 언어 입문서로 국내에 이광근 교수님이 저술한 책이 있지만, 그 책 말고는 입문서가 사실상 전무한 수준이라고 감히 생각한다.(한국어로 된 좋은 책이 있으면 소개좀…) 옆 문화권의 좋은 입문서가 있다면 조금이라도 살펴보면 도움이 되지 않을까 싶다.
영어가 편하면 Types and Programming Languages (a.k.a. TaPL) 을 읽으면 되지 않을까. 나도 아직 안봤지만.

들어가며

프로그래밍 언어는 계산기 소프트웨어를 기술하기 위한 인공 언어이며, 계산기의 발전과 함께 다수의 프로그래밍 언어가 개발되어 왔다. 프로그래밍언어는, 영어같은 외국어와 비교해보면, 같은 ‘언어’라고는 말할 수 없고, 그 성립과 목적도 크게 다르다. 그렇지만, 습득하는 프로세스에는 공통된 부분도 실제로는 많다. 외국어를 습득하는 방법인, 실제로 문장을 써보거나 회화를 해보고, 네이티브의 문장을 읽고하는 훈련은, 프로그래밍을 적어서 돌려보고, 다른 사람이 적은 좋은 프로그램을 읽어보고하는 것과 대응하고 있는 것일 것이다. (지금까지의 프로그래밍 교육에서는, 다른 사람의 프로그램을 읽는 것은 그렇게 중시되지 않던 것 같다.) 그리고, 복수의 외국어를 효율적으로 배우기위해서는, 각 언어의 문법만이 아니라, ‘동사의 활용’, ‘명사의 성의 유무’, ‘조수사’라는 많은 언어에 적용할 수 있는 개념을 이해하는 것이 매우 중요한 것 처럼, 복수의 프로그래밍 언어를 효율적으로 배우기 위해서는 ‘프로그래밍 언어를 말하기 위한 개념’을 아는 것이 중요하다.

이 책의 목적은, 프로그래밍의 동작을 수학적으로 엄밀하게 기술하기 위한 의미론, 프로그래밍의 오류를 프로그래밍을 실행하기 전에 탐지하기 위한 틀인 타입 시스템, 그리고, 그것과 관련된 프로그래밍 언어의 기초개념을 습득하여, 그 개념 간의 수학적인 관련을 배우는 것이다. 다만, 구문해석등의 이른바 구문론(신텍스), 가비지 컬렉션에 의한 메모리 관리 등의 언어처리계의 실제적인 기술 등은, 모두 중요한 개념이지만, 이 책에서는 다루지 않는다.

구체적인 프로그리밍언어로서는, ML(의 방언인 OCaml) 을 중심 부분으로 하였다. ML은, 프로그래밍 언어 중에서도 함수형 언어라고 불리는 종류의 것으로,

• 계산 절차의 한 묶음인 함수를 데이터로 하여 교환하는 고차함수
• 구조를 가지는 데이터의 내부를 단순한 기술로 엑세스하는 패턴 매치
• 프로그램 속의 오류를 프로그래밍 실행 이전에 탐지하기 위한 타입 시스템
• 프로그램이 사용하는 변수의 종류(타입 정보)의 기술을 생략해도, 타입 시스템에 의한 오류 탐지를 하는 타입 추론
• 하나의 절차를 다목적으로 사용해, 프로그램의 재이용성을 향상시키기 위한 폴리모픽 타입 시스템

이라는 선진적인 특징이 있는 언어이다. OCaml을 재제로서 다룬 것은, 저자의 기호에도 따르고 있지만,

• 처리계가 존재하고, 스스로 프로그램을 동작시키는 것이 가능하다
• 프로그램의 의미를 비교적 단순하게 기술할 수 있다
• 타입 시스템을 구비하고 있다
• 타입 시스템의 의미론의 관계가 수학적으로 엄밀하게 논의될 수 있다

라는 이유에서이다. 그러나, 외국어의 문법서만을 읽어도 읽기 쓰기가 되지 않는 것과 마찬가지로, 이 책만으로는, ML 프로그램을 작성할 수 있게 되지는 않는 것이다. 차라리 이 책이 ML 이외의 이미 알고있는, 알지 못하는 프로그래밍 언어에 대한 새로운 관점을 제공하는 것이 된다면, 이 책의 목적은 달성된다고 생각할 수 있다. (OCaml에 대해 자세하게 알고싶은 분은 이 책 말미의 ‘더 공부하고 싶은 사람에게’에도 참고서적을 소개하고 있기에 그쪽을 참고하면 좋겠다)

이 책의 특색은, 내용을 깊게 이해하기위한 온라인 연습 시스템이 준비되어 있다는 것이다. 연습으로는, 예를 들면, 주어진 프로그램의 실행 결과가 무엇인가라는 것의 ‘증명’을 주는 것이 요구되지만, 이 연습 시스템은, 해답인 ‘증명’의 정오를 자동으로 판정해준다. 온라인 연습 시스템인 연습문제의 일부는 본 책의 속에도 게재되어있지만, 문제는 그 외에도 120문 이상 준비되어 있다. 반드시, 도전해 주었으면 좋겟다. 온라인 연습 시스템을 포함해 보 낵의 보조자료는

http://www.saiensu.co.jp/

에 있는 본 책 서포트 페이지에서 링크를 보내주시던가, 직접

http://member.acm.org/~aigarashi

에 엑세스해 주시면 이용 가능하다.

본 책은 크게 나누어 세 부분으로 구성되어 있다. 제 1부(제 1~2장)에서는, ML의 의미론, 타입 시스템을 정의하기 위한 공통의 틀인 도출 시스템, 그리고, 도출 시스템에 대해 정리(메타 정리라고 불리는)와 그 증명 기법인 귀납법에 대해서 논의한다. 제 2부(제 3~7장)에서는 ML의 의미론에 대해, 그리고 제 3부(제 8~10장)에서는 ML의 타입 시스템과 의미론과의 관계에 대해, 제 1부에서 도입했던 도출 시스템을 사용하여 논의한다. 메타 정리의 증명에 대해서는, 조금은 고도의 내용도 포함되어있기 때문에, 처음에 읽는 때에는 적당히 넘어가도 상관없지만, 언젠가는 이해하였으면 좋겠다.

본책은 … (감사의 말씀)

2011년 7월

교토에서
저자