# Inductive type

> 타입 이론에서 어떤 타입이 재귀 타입이면서 동시에 합 타입이면 귀납 타입이라고 부른다.

[타입 이론](https://wiki.g15e.com/pages/Type%20theory.txt)에서 어떤 타입이 [재귀 타입](https://wiki.g15e.com/pages/Recursive%20type.txt)이면서 동시에 [합 타입](https://wiki.g15e.com/pages/Sum%20type.txt)이면 귀납 타입이라고 부른다.

> Recursive sum types are called inductive datatypes, because <mathematical induction> may be used to prove statements about them. When programming, inductive datatypes are consumed through pattern matching and recursive functions. --[Functional programming in Lean](https://lean-lang.org/functional_programming_in_lean/getting-to-know/datatypes-and-patterns.html)

## 프로그래밍 언어 예시

[Lean](https://wiki.g15e.com/pages/Lean%20(programming%20language.txt))에서는 이런 식으로 정의한다.

```lean
inductive Bool where
  | false : Bool
  | true : Bool
```

[객체지향](https://wiki.g15e.com/pages/Object-oriented%20programming.txt) 언어에서는 클래스와 상속으로 표현할 수 있다. 다음은 [자바](https://wiki.g15e.com/pages/Java.txt) 예시:

```java
abstract class Bool {}

class True extends Bool {}
class False extends Bool {}
```

두 방식의 차이점:

> However, the specifics of these representations are fairly different. In particular, each non-abstract class creates both a new type and new ways of allocating data. In the object-oriented example, True and False are both types that are more specific than Bool, while the Lean definition introduces only the new type Bool. --[Functional programming in Lean](https://lean-lang.org/functional_programming_in_lean/getting-to-know/datatypes-and-patterns.html)

<페아노 공리>와 유사한 방식으로 자연수 정의하기:

```lean
inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat
```