Dependent Types for Programmers: A Practical Introduction Using Lean 4

개요

Lean 4와 같은 도구를 통해 프로그래머에게 종속 타입(dependent types)의 실용적인 개념과 중요성을 소개하며, 컴파일러가 더 많은 프로그램 가정을 이해하도록 하여 소프트웨어의 오류를 줄이는 방법을 설명합니다.

주요 내용

• 일반적인 타입과 종속 타입의 차이: 일반적인 언어에서 타입은 값의 종류를 나타내지만(예: Int, String), 값의 속성(크기, 상태 등)은 명시하지 못합니다. 종속 타입은 타입 자체에 값이 포함될 수 있도록 하여(예: Vec Nat 3은 길이가 3인 자연수 벡터를 의미), 컴파일러가 값에 기반한 더 엄격한 검사를 수행하도록 합니다.
• 종속 타입의 실용적인 적용:
• 벡터의 크기 명시: Vec α n과 같은 타입은 벡터의 요소 타입(α)뿐만 아니라 그 크기(n)까지 타입 시스템 내에서 다룰 수 있게 합니다. 예를 들어, append : Vec α n → Vec α m → Vec α (n + m)는 두 벡터를 이어 붙였을 때 결과 벡터의 크기가 n + m이 됨을 타입 시스템이 이해하도록 합니다.
• 불변 조건(Invariants) 강제: 행렬 곱셈에서 a.columns == b.rows와 같은 암묵적인 규칙을 타입 시스템에 명시하여, 컴파일 시점에 잘못된 연산을 방지할 수 있습니다.
• 비어 있지 않은 리스트: head : Vec α (n + 1) → α와 같이, 타입 자체에 n + 1이라는 조건을 포함시켜 0이 될 수 없음을 명시함으로써 빈 리스트에 대한 head 연산 시 발생하는 오류를 사전에 차단합니다.
• 동적 입력과 종속 타입: 종속 타입은 컴파일 시점에 모든 값이 알려져야만 유용한 것이 아닙니다. 동적으로 입력받은 데이터도 유효성 검사를 거친 후에는 그 결과가 타입 시스템에 반영되어, AuthenticatedUser, ValidConfig, NonEmptyList와 같이 더 안전한 타입으로 취급될 수 있습니다.
• Lean의 탐구 방향: Lean은 단순한 정리 증명 도구를 넘어, 프로그램 불변 조건이 언어 자체의 일부가 되는 환경을 탐구하며, 주석과 희망에 의존하는 대신 증명과 강제(enforcement)를 통해 소프트웨어의 정확성을 높이는 모델을 제시합니다.

시사점

종속 타입은 프로그램의 명시적인 가정들을 타입 시스템에 통합하여, 주석이나 런타임 검사에 의존하던 많은 종류의 버그를 컴파일 시점에 탐지하고 방지하는 강력한 방법을 제공합니다.