확장 GADTs

Generalized Algebraic Data Type

참고 - 대수 타입 포스트

타입 매개 변수 해석

먼저 Sum 형태의 타입에서 타입 매개 변수가 어떻게 쓰이는지 살펴 보겠습니다.

data Some a = A a
            | B Int
            | C Bool

> :t B 7
B 7 :: Some a

> :t C True
C True :: Some a

func :: Some Int -> Bool 
func x = True

> func (C True) -- GHC가 알아서 Some Int 타입으로 추론합니다.
True

val1 :: Some Bool
val1 = B 5

> func val1
error: Couldn't match type ‘Bool’ with ‘Int’

Sum 형태의 대수 타입

보통 Sum 형태의 타입은 여러 타입들을 합쳐서 같은 부류로 취급할 때 씁니다.

data Expr a = I Int
            | B Bool
            | Add (Expr a) (Expr a)
            | Mul (Expr a) (Expr a)
            | Eq  (Expr a) (Expr a)

Expr 타입을 받는 함수는 I, B, Add, Mul, Eq 값을 받을 수 있습니다. 타입 모둠에 Expr이란 이름을 붙여 놓은 것과 같습니다. 그런데 Add 값은 Expr 타입 두 개를 받는데, 모든 Expr 타입을 받는게 아니라 B와 Eq는 빼고 받아야 합니다. 나중에 인터프리터에서 구별해도 되지만, 컴파일 단계에서 걸러내길 원합니다.

Add는 인자로 Expr Int 타입만 받도록 하고싶습니다.

-- Add가 Expr a가 아닌 Expr Int를 받도록 바꿨습니다.
data Expr a = ...
            | Add (Expr Int) (Expr Int)
            ...

> :t Add (I 3) (B True)
Add (I 3) (B True) :: Expr a
-- 그래도 여전히 B True 같은 값을 받아도 오류가 나지 않습니다. 
-- B True를 Expr Int 타입으로 추론해도 문제가 없기 때문입니다.

이럴 때, GADT 확장을 씁니다.

GADT - 값 생성자별로 구체 타입을 다르게 하기

Generalized Algebraic Data Types

GADT를 쓰면 각 값생성자들의 리턴 타입을 다르게 지정할 수 있습니다.

{-# LANGUAGE GADTs #-}

data Expr a where
  I   :: Int -> Expr Int
  B   :: Bool -> Expr Bool
  Add :: Expr Int -> Expr Int -> Expr Int
  Mul :: Expr Int -> Expr Int -> Expr Int
  Eq  :: Eq a => Expr a -> Expr a -> Expr Bool

얼핏 보면 GADT 없이도 Add (Expr Int) (Expr Int) 라고 선언하면 될 것처럼 보이지만, B나 Eq 값의 타입이 Expr a이면 GHC가 추론해서 맞춰버리기 때문에 Expr Bool이어야만 Add에서 걸러 낼 수 있습니다. 그러려면 값생성자들의 결과 타입을 폴리모픽이 아닌, 구체 타입으로 지정할 수 있어야 합니다. I, Add, Mul은 Expr Int타입이고, B,Eq는 Expr Bool 타입으로 지정하면 컴파일 단계에서 타입 체크를 할 수 있습니다.

실제 사용 예는 타입 레벨 프로그래밍을 다루는 포스트에서 다루도록 하겠습니다.

※ a를 보통의 타입처럼 읽어 보면 도움이 될 수 있습니다. a를 Int, Bool 처럼 그저 타입 중 하나로 구별하지 않고 읽어 보면, Expr a는 I :: Expr Int 타입의 값을 가질 수 있고, Eq :: ... Expr a 타입의 값을 가질 수 있습니다.

Q. 왜 이런 타입을 Generalized Algebraic DataTypes 라 부를까요?
대수 데이터 타입은, 타입을 써서(연산해서) 타입을 만드는 걸(주로 Sum 혹은 Product) 의미하는데,대수 타입 이 Generalized 됐다는 말이 무슨 말일까요? A. data Some a = C1 a | C2는 C1, C2 모두 Some a 타입으로 추론되지만,
data Some a where C1 :: ... C2 :: ...는 Some a로 추론되게 할 수도 있고, C1이나 C2가 Some Int등의 구체 타입으로 고정하는 것도 가능하게 표현력이 늘었으니, 더 일반화 됐다고 볼 수 있습니다. 나중에 더 다양한 표현이 필요하게 되면, “더 일반화”된 표현이 발견, 발명될지도 모르지요.

※ 팬텀 타입
실제 데이터를 위한 타입이 아니라, 타입 체커를 위한 타입 매개 변수를 팬텀 타입이라 부릅니다. I, Add, Mul 모두 결과가 Expr Int이지만, 내부에 가지고 있는 값은 Int만 있는게 아니라, Add나 Mul같은 수식일 수도 있습니다. Expr Int에서 Int는 타입 체커를 위한 표식입니다.

※ 값 생성자는 값을 만들 때 쓰이고, desconstruct하기 위해 패턴 매칭할 때 쓰입니다. Int를 Maybe Int로 만들 때 Just가 쓰이고, Just 안에 들어 있는 Int를 꺼낼 때 Just로 패턴매칭합니다.