아담 칠리파라(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)
'Coq 증명기' 카테고리의 다른 글
소프트웨어 기초(Software Foundations) (0) | 2017.09.11 |
---|---|
[Coq 증명기] 콕, 빨리 빨리: 8장 귀납적 성질 (0) | 2014.08.09 |
[Coq 증명기] 콕, 빨리 빨리: 7장 콕 시스템의 숫자 (0) | 2014.08.09 |
[Coq 증명기] 콕, 빨리 빨리: 6장 새로운 데이터 타입 정의하기 (0) | 2014.08.09 |
[Coq 증명기] 콕, 빨리 빨리: 5장 리스트 프로그램의 성질을 증명하기 (0) | 2014.08.09 |