아담 칠리파라(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)




Posted by lazyswamp :