데이터 타입

데이터 타입 (Data Types)

단순 데이터 타입 (Simple datatypes)

예제 데이터 타입 (Example datatypes)

서론에서 이미 (단항 표기의) 자연수 데이터 타입의 정의를 보여줬어요:

data Nat : Set where
    zero : Nat
    suc  : Nat → Nat

몇 가지 예를 더 들어볼게요. 먼저 진리값 데이터 타입:

data Bool : Set where
  true  : Bool
  false : Bool

True 집합은 자명하게 참인 명제를 나타내요:

data True : Set where
    tt : True

False 집합은 생성자가 없어서 원소도 없어요. 이것은 자명하게 거짓인 명제를 나타내요:

data False : Set where

또 다른 예는 잎에 자연수를 가진 비어 있지 않은 이진 트리 데이터 타입이에요:

data BinTree : Set where
  leaf   : Nat → BinTree
  branch : BinTree → BinTree → BinTree

마지막으로 Brouwer 서수의 데이터 타입:

data Ord : Set where
  zeroOrd : Ord
  sucOrd  : Ord → Ord
  limOrd  : (Nat → Ord) → Ord

일반 형태 (General form)

단순 데이터 타입 D 의 정의의 일반적인 형태는 다음과 같아요:

data D : Setᵢ where
  c₁ : A₁
  ...
  cₙ : Aₙ

데이터 타입의 이름 D와 생성자의 이름 c₁, …, cₙ은 현재 시그니처와 문맥에 대해 새 것이어야 하고, 타입 A₁, …, Aₙ은 D로 끝나는 함수 타입이어야 해요. 즉, 다음과 같은 형태여야 해요:

(y₁ : B₁) → ... → (yₘ : Bₘ) → D

매개변수화된 데이터 타입 (Parametrized datatypes)

데이터 타입은 매개변수를 가질 수 있어요. 매개변수는 데이터 타입 이름 뒤, 콜론 앞에 선언돼요. 예를 들어:

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

인덱스된 데이터 타입 (Indexed datatypes)

매개변수에 더해 데이터 타입은 인덱스도 가질 수 있어요. 모든 생성자에 대해 동일해야 하는 매개변수와 달리, 인덱스는 생성자마다 달라질 수 있어요. 인덱스는 콜론 뒤에 Set에 대한 함수 인자로 선언돼요. 예를 들어 고정 길이 벡터는 그들의 Nat 타입 길이로 인덱싱해 정의할 수 있어요:

data Vector (A : Set) : Nat → Set where
  []  : Vector A zero
  _∷_ : {n : Nat} → A → Vector A n → Vector A (suc n)

매개변수 A는 모든 생성자에 대해 한 번 바인딩되는 반면, 인덱스 {n : Nat}는 생성자 _∷_에서 로컬로 바인딩되어야 한다는 점에 주의하세요.

인덱스된 데이터 타입은 술어(predicate)를 설명하는 데도 사용될 수 있어요. 예를 들어 술어 Even : Nat → Set은 다음과 같이 정의할 수 있어요:

data Even : Nat → Set where
  even-zero  : Even zero
  even-plus2 : {n : Nat} → Even n → Even (suc (suc n))

일반 형태 (General form)

(매개변수화, 인덱스된) 데이터 타입 D 의 정의의 일반적인 형태는 다음과 같아요:

data D (x₁ : P₁) ... (xₖ : Pₖ) : (y₁ : Q₁) → ... → (yₗ : Qₗ) → Set ℓ where
  c₁ : A₁
  ...
  cₙ : Aₙ

여기서 타입 A₁, …, Aₙ은 다음 형태의 함수 타입이에요:

(z₁ : B₁) → ... → (zₘ : Bₘ) → D x₁ ... xₖ t₁ ... tₗ

엄격 양성 (Strict positivity)

데이터 타입 D 를 정의할 때, Agda는 D 의 생성자 타입에 추가 요구 사항을 부과해요. 즉, D 는 자신의 인자 타입에 엄격하게 양(strictly positive)으로만 나타날 수 있어요.

구체적으로, 생성자 c₁ : A₁, …, cₙ : Aₙ을 가진 데이터 타입에 대해 Agda는 각 Aᵢ가 다음 형태인지 검사해요:

(y₁ : B₁) → ... → (yₘ : Bₘ) → D

여기서 생성자의 인자 타입 Bᵢ는 다음 중 하나예요:

  • 비-귀납적(부수 조건)이고 D를 전혀 언급하지 않거나,
  • 귀납적이고 다음 형태를 가짐: 
    (z₁ : C₁) → ... → (zₖ : Cₖ) → D
    여기서 D는 어떤 Cⱼ에도 나타나지 않아야 해요.

엄격 양성 조건은 다음과 같은 선언을 배제해요:

data Bad : Set where
    bad : (Bad → Bad) → Bad
    --     A     B      C
    -- A is in a negative position, B and C are OK

생성자의 인자 타입에 Bad의 부정적 발생(negative occurrence)이 있기 때문이에요. (참고로 Bad의 대응하는 데이터 타입 선언은 Haskell이나 ML 같은 표준 함수형 언어에서는 허용돼요.)

엄격 양성이 아닌 선언은 비종료 함수를 허용하기 때문에 거부돼요.

양성 검사가 비활성화되면, 즉 Bad의 유사한 선언이 허용되면, 재귀 없이도 빈 타입의 항을 구성할 수 있어요.

{-# OPTIONS --no-positivity-check #-}

data ⊥ : Set where

data Bad : Set where
  bad : (Bad → ⊥) → Bad

self-app : Bad → ⊥
self-app (bad f) = f (bad f)

absurd : ⊥
absurd = self-app (bad self-app)

종료에 대한 더 일반적인 정보는 종료 검사를 참고하세요.

더 알아보기 (Learn more)