Dependent Types의존 타입

일반 타입:     List Int         (임의 길이 리스트)
의존 타입:     Vec Int 3        (길이 3인 벡터)

-- Pi 타입 (의존 함수 타입): Πx:A. B(x)
-- 반환 타입이 입력값 x에 의존
replicate : (n : Nat) -> A -> Vec A n

-- Sigma 타입 (의존 쌍 타입): Σx:A. B(x)
-- 두 번째 구성요소의 타입이 첫 번째 값에 의존
NonEmptyList : Σ(n:Nat). n > 0 × Vec A n

-- 자연수 정의
data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

-- 길이 인덱스된 벡터
data Vec (A : Set) : Nat → Set where
  []  : Vec A zero
  _∷_ : A → Vec A n → Vec A (suc n)

-- 안전한 head: 빈 벡터 불가
head : Vec A (suc n) → A
head (x ∷ _) = x
-- 컴파일 타임에 빈 벡터 접근 방지!

-- 타입 레벨 덧셈
_++_ : Vec A m → Vec A n → Vec A (m + n)
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

(* 정렬된 리스트를 타입으로 표현 *)
Inductive Sorted : list nat -> Prop :=
  | sorted_nil  : Sorted []
  | sorted_one  : forall x, Sorted [x]
  | sorted_cons : forall x y l,
      x <= y -> Sorted (y :: l) ->
      Sorted (x :: y :: l).

(* 삽입 정렬이 Sorted를 만족함을 증명 *)

-- 행렬 곱셈: 차원 불일치 컴파일 에러
matMul : Matrix m n -> Matrix n p -> Matrix m p

-- 효과 타입 시스템
readLine : IO String
writeFile : (path : String) -> (content : String) -> IO ()