하스켈 프로그래밍(Haskell) 커뮤니티를 시작하며.


1994년 대학원에 들어가서 처음 함수형 프로그래밍 언어 하스켈(Haskell, www.haskell.org)을 접하고 여러 잡다한 프로그래밍을 통해 그 이상한 매력에 끌리게 되었다. 마치 결벽증 환자처럼 "순수함"을 유지하려고 애쓰는 모습도 희한했고, 그러면서도 남들이 하는 일을, 똑같이, 조금 과장해서 말하자면, 더 잘 할 수 있는 것도 멋있었다. 그 매력에 끌려 한때는 모든 다른 프로그래밍 언어는 삼류고, 다 필요없고, 오직 하스켈만 절대 지존이고 유일한 프로그래밍 언어라고 생각했던 적도 있었다. 물론 착각이고. 


20년이 지난 오늘 주변에서 하스켈에 대해 관심있는 사람들이 몇몇 있다. 아직은 학교에 있는 학생들이 대부분인 것 같고 L모 회사에 근무하는 사람도 관심을 가지고 있더라. 그리고 몇 주 전에 참가한 어느 세미나에서 "모나드(Monad)"에 대한 설명을 듣는데 개인적으로 너무 마음에 들지 않았다. 하스켈의 악명 높은 주제이긴 하지만 다른 식으로 얘기할 수 있지 않았을까 생각했다. 하스켈이 유일 무이한 프로그래밍 언어는 아니라는 것을 잘 알고 있지만, "순수함"을 잃지 않으려는 이 대범한 노력을 누가 또 할 수 있을까 생각할 때마다 하스켈 프로그래밍을 하던 학생 시절에 그랬던 것 처럼 가슴이 뛰기도 한다. 그리고 "순수함"을 유지하는 하스켈에 "순수함"을 잃어버린 다른 프로그래밍 언어들이 지향해야하는 모습이 담겨 있다는 생각까지 하게 되면, 하스켈 프로그래밍을 배우는 것은 단지 하스켈 언어만을 배우는 것이 아니라는 생각이 강하게 든다.


이러한 생각을 하다보니 하스켈 프로그래밍 커뮤니티가 하나쯤은 있어도 되겠다는 생각이 문득 들었다. 먼저, 하스켈에서 배운대로, 특별한 개발 목적이 있어서가 아니라 그냥 재미삼아 하스켈 언어를 배우는 스터디 모임을 가지고 커뮤니티를 시작해보려 한다. 이 커뮤니티가 활성화되면 하스켈에 적용된 최신 프로그래밍언어 기술에 대해서 논의하고, 나아가서 상용 목적으로 하스켈을 응용하는 사례에 대해 살펴보는 장으로 발전하기를 기대해본다.


2015/8/31


K. Choi


저작자 표시 비영리 변경 금지
신고

아담 칠리파라(Adam Chlipala)의 책 9.2절 Heterogeneous Lists 참고. 


ML이나 Haskell에서 리스트는 매우 빈번하게 사용한다. [1,2,3,4,5]는 1부터 5까지 정수를 포함하는 리스트로 그 타입은 Haskell에서 [Int]이다. ML이나 Haskell에서의 리스트는 타입이 동일한 원소들의 리스트를 얘기한다. 따라서, [1, true]와 같은 식은 허용하지 않는다. Haskell에서 타입 클래스(type class)를 사용하면 타입이 다른 원소들의 리스트를 표현할 수는 있지만 복잡하다. 콕 시스템은 ML이나 Haskell보다 더 복잡한 타입 시스템을 갖추고 있어 상대적으로 간단하게 이러한 리스트를 표현할 수 있다.


콕 시스템에서 타입이 다른 원소들의 리스트를 만드는 방법을 살펴본다. 기본적인 아이디어는 리스트 타입을 타입 수준의 리스트로 색인을 달아 각 원소의 타입이 무엇인지 설명하는 것이다. 간단한 생각이지만 콕으로 표현했을때 간단한 리스트도 꽤 복잡해진다. 


Inductive hlist (A:Type) (B:A ->Type) : list A -> Type :=

   HNil : hlist A B nil

| HCons : forall (x:A) (ls:list A), B x -> hlist A B ls -> hlist A B (x::ls).


예를 들어 hlist의 쓰임새를 살펴보자. 먼저, HCons의 타입은 선언된 바와 같다. 전칭 한정 변수가 네 개이다.


Check HCons.


HCons

     : forall (A : Type) (B : A -> Type) (x : A) (ls : list A),

       B x -> hlist A B ls -> hlist A B (x :: ls)



첫번째 전칭 한정 변수 A를 Set으로 대체한다. 


Check HCons Set.


HCons Set

     : forall (B : Set -> Type) (x : Set) (ls : list Set),

       B x -> hlist Set B ls -> hlist Set B (x :: ls)


두번째 전칭 한정 변수 B를 (fun T: Set => T)로 대체한다. 사실 이 함수는 Set -> Set 타입을 갖는다. 서브 타입 관계에 의해 Set -> Type으로 간주한다. 


Check HCons Set (fun T:Set => T).


HCons Set (fun T : Set => T)

     : forall (x : Set) (ls : list Set),

       (fun T : Set => T) x ->

       hlist Set (fun T : Set => T) ls ->

       hlist Set (fun T : Set => T) (x :: ls)


그 다음 전칭 한정 변수 x에 bool을 넘긴다. bool의 타입은 Set이다.


Check HCons Set (fun T:Set => T) bool.


HCons Set (fun T : Set => T) bool

     : forall ls : list Set,

       (fun T : Set => T) bool ->

       hlist Set (fun T : Set => T) ls ->

       hlist Set (fun T : Set => T) (bool :: ls)


마지막 전칭 한정 변수 ls에 nil을 준다. nil은 list Set 타입이므로 타입 리스트이다.


Check HCons Set (fun T:Set => T) bool nil.


HCons Set (fun T : Set => T) bool nil

     : (fun T : Set => T) bool ->

       hlist Set (fun T : Set => T) nil ->

       hlist Set (fun T : Set => T) (bool :: nil)


(fun T : Set => T) bool을 베타 환원(beta redunction)으로 계산하면 bool이 된다. 따라서 HCons Set (fun T : Set => T) bool nil의 타입은 bool -> ... 형태이다. 그래서 이 함수의 부울 인자로 true를 지정한다.


Check HCons Set (fun T:Set => T) bool nil true.


HCons Set (fun T : Set => T) bool nil true

     : hlist Set (fun T : Set => T) nil ->

       hlist Set (fun T : Set => T) (bool :: nil)


HNil Set (fun T : Set => T)는 hlist의 정의에 의해 hlist Set (fun T : Set => T) nil 타입을 갖는다.


Check HNil Set (fun T : Set => T)


HNil Set (fun T : Set => T)

     : hlist Set (fun T : Set => T) nil


다시 원래 식으로 돌아가서 마지막 인자로 HNil Set (fun T : Set => T)를 넘기면 hlist 타입의 타입이 다른 원소들의 리스트가 된다.


Check HCons Set (fun T:Set => T) bool nil true (HNil Set (fun T:Set => T)).


HCons Set (fun T : Set => T) bool nil true (HNil Set (fun T : Set => T))

     : hlist Set (fun T : Set => T) (bool :: nil)


조금 간단하게 hlist를 사용하기 위해 다음 세 가지 정의를 도입하자.


Definition HList := hlist Set (fun T:Set => T).

Definition hcons := HCons Set (fun T:Set => T).

Definition hnil := HNil Set (fun T:Set => T).


list Set은 타입 리스트로, 타입이 다른 원소들의 리스트를 표현하는 아이디어가 HList의 타입에 그대로 표현되어 있다. 


Check HList.


HList

      : list Set -> Type


리스트 [1, true]를 다음과 같이 작성할 수 있다.


Check hcons nat (bool::nil) 1 (hcons bool nil true hnil).


hcons nat (bool :: nil) 1 (hcons bool nil true hnil)

     : hlist Set (fun T : Set => T) (nat :: bool :: nil)




저작자 표시 비영리 변경 금지
신고

8. 귀납적 성질


귀납적 정의로 새로운 술어를 기술할 수도 있다. 타입 A에 대한 술어는 A 타입의 원소를 입력 받아 명제 타입 Prop의 원소를 반환하는 함수로 간단히 기술할 수 있다. 귀납적 명제의 컨스트럭터는 술어로 규정하는 정리들이다. 이 술어에 기반한 문장에 대한 증명은 오직 이 컨스트럭터의 조합으로만 얻을 수 있다.


8.1 귀납적 술어 정의하기

짝수 자연수 집합을 뜻하는 술어를 다음과 같이 귀납적 정의를 쓸 수 있다.


Inductive even : nat -> Prop :=

   even0 : even 0

| evenS : forall x:nat, even x -> even (S (S x)).



x가 자연수라면 even x는 명제이다. 정리 even0는 even 0 명제를 증명할 때 사용하고, 정리 evenS는 명제 even 0로 부터 명제 even 2를 추론할 때 쓸 수 있다. evenS를 반복해서 사용하면 나머지 숫자들도 even 술어를 만족함을 증명하는데 이용할 수 있다.


귀납 타입처럼 case, elim, destruct 전술들을 사용해서 귀납 명제에 관련된 가정에 대해 추론할 수 있다. 이 전술들을 쓰면 귀납 정의의 각 컨스트럭터 별로 하나씩 목적 명제를 다시 만들어 낼 것이다. 덧붙이자면 컨스트럭터가 전제로 귀납 명제를 사용하면 elim과 induction 전술은 귀납 가정을 만든다.


8.2 귀납적 술어에 대한 귀납 증명

변수 x가 귀납적 성질을 만족한다면 그 변수 자체에 대한 귀납을 사용하는 것 보다 귀납적 성질에 대한 귀납을 사용해서 그 변수에 대한 성질을 증명하는 것이 종종 더 효율적이다. 다음 증명의 예를 보자.


Lemma even_mult : forall x, even x -> exists y, x = 2 * y.

intros x H; elim H.


2 subgoals

  

  x : nat

  H : even x

  ============================

   exists y : nat, 0 = 2 * y


subgoal 2 is:

 forall x0 : nat,

 even x0 -> (exists y : nat, x0 = 2 * y) -> exists y : nat, S (S x0) = 2 * y


첫번째 목적 명제는 even의 첫번째 컨스트럭터를 사용해주 even x를 증명하는 경우이다. 이때 변수 x는 0으로 바꾸어 이 목적 명제를 표시한다. y를 0으로 놓고 증명할 수 있다.


exists 0; ring.


1 subgoal

  

  x : nat

  H : even x

  ============================

   forall x0 : nat,

   even x0 ->

   (exists y : nat, x0 = 2 * y) -> exists y : nat, S (S x0) = 2 * y


그 다음 목적 명제는 even의 두번째 컨스트럭터를 가지고 even x를 증명하는 경우에 대한 것이다. 이때 x가 S (S x0)인 변수 x0가 반드시 존재해야 한다. 그리고 elim 전술은 even x0에 대한 귀납 가정을 도입한다. 이렇게 x0는 S (S x0)에 대해 증명할 성질을 만족할 것으로 가정한다. 이런 점에서 elim 전술은 귀납 가정을 생성한다. 이는 마치 induction 전술에서와 정확히 같다. 사실 elim대신 induction 전술을 쓸 수 있다. 두 전술은 거의 똑같다. 


intros x0 Hevenx0 IHx.


1 subgoal

  

  x : nat

  H : even x

  x0 : nat

  Hevenx0 : even x0

  IHx : exists y : nat, x0 = 2 * y

  ============================

   exists y : nat, S (S x0) = 2 * y


이제 IHx는 귀납 가정이다. x가 x0의 다음 다음이라면 x0의 반이되는 값 y가 존재함을 이미 알고 있음을 뜻한다. 이 값을 S (S x0)의 반을 구하기 위해 이용한다. 다음의 전술을 사용해서 증명을 완료한다.


destruct IHx as [y Heq].

rewrite Heq.

exists (S y).

ring.


destruct 전술을 이전과 다르게 사용했다. 이 전술로 원소를 새로 만들어 이름을 붙이고, 이 이름을 문맥에 도입한다. 


8.3 inversion 전술

inversion 전술은 귀납적 명제에 관한 문장을 증명하는 다양한 방법에서 쓰일 수 있다. 이 전술은 귀납적 명제의 모든 컨스트럭터를 분석하고, 적용할 수 없는 것은 버리며, 적용가능한 컨스트럭터에 대해서 새로운 목적 명제를 만들고 이 컨스트럭터의 전제들을 문맥에 불러들인다. 예를 들어, 1이 짝수가 아님을 증명하는데 매우 적합하다. 왜냐하면 어떤한 컨스트럭터도 명제 even 1로 결론짓지 않기 때문이다. evenS는1 = S (S x)를 증명해야하고, even0는 1=0을 증명해야하는데 모두 거짓이다.


Lemma not_even_1 : ~even 1.

intros even1.


1 subgoal

  

  even1 : even 1

  ============================

   False


inversion even1.

Qed.


inversion 전술을 사용하는 다른 예로, 짝수의 이전 이전 수는 짝수임을 증명해보자. 이 문장에서 주어진 수를 S (S x)로 놓고 이전 이전 수를 x로 놓자.


Lemma even_inv : forall x, even (S (S x)) -> even x.


intros x H.


1 subgoal

  

  x : nat

  H : even (S (S x))

  ============================

   even x


이 전술에서 even 술어의 컨스트럭터들을 분석하면 even0를 사용해서 가정 H를 증명할 수 없음을 인식한다. 오직 evenS만 사용될 수 있다. 그러므로 even x0와 S (S x) = S (S x0)가 성립하는 x0가 반드시 존재해야 한다. 즉, even x가 성립한다.


inversion H.


1 subgoal

  

  x : nat

  H : even (S (S x))

  x0 : nat

  H1 : even x

  H0 : x0 = x

  ============================

   even x


assumption.

Qed.


even_inv의 문장은 evenS 문장의 반대임을 참고하시오. 이 전술의 이름을 이렇게 붙이 이유이다. 


귀납적 성질은 매우 복잡한 개념을 표현하는데 사용할 수 있다. 프로그래밍 언어의 의미를 귀납적 정의로 정의할 수 있다. 기본적인 계산 단계에 각각 해당하는 컨스트럭터들을 도입할 수 있다. 



===

번역


(1장)

Expressions : 식

Formulas : 식

infix : 인픽스

Logical Formulas : 논리식

Symbolic Computation : 기호 계산

Terms : 텀

Well-formed : 제대로 된 형태


(2장)

Keyword : 키워드

Boolean : 부울

Conjunction : 곱

Disjunction : 합

Negation : 부정

Construct : 구문

Pattern-matching : 패턴 매칭

Recursivity : 재귀 형태

Structural Recursion : 구조적 재귀

Subterm : 부분식

Sublist : 부분리스트


(3장)

Fact: 사실 명제

Theorem: 정리

Implication : 함축

Predicate : (술어) 명제

Rewriting : 다시쓰기

Equality : 등식

Goal : 목적 명제

Tactic : 전술

Hypothesis : 가정

Universal Quantification : 전칭 한정

Transitive : 추이적

Instantiation : 사례화

Associativity : 결합성


(4장)

Proof by induction : 귀납적 증명

Existential : 존재

Lemma : 보조 정리


(5장)

the step case of the proof by induction : 귀납적 증명의 귀납적 경우


(6장)

datatype : 타입, 데이터 타입

Binary tree : 이진 트리

Internal Node : 내부 노드

Leaf : 끝 노드

Proof by Cases : 경우를 나누어 증명

Constructor : 컨스트럭터

Injective : 단사적


(7장)

Well-founded : 기초가 튼튼한(?)

Iterator : 반복자


(8장)


Predicate : 술어



저작자 표시
신고

+ Recent posts

티스토리 툴바