하스켈 GADT

gadt.md

이 글은 하스켈 위키북스 Haskell/GADT를 읽고 정리한 것이다.

하스켈 GADT

• Generalized Algebraic DataTypes
• GHC 확장
• 데이터 타입 선언 시 값 생성자에 타입을 적을 수 있게 한다.

data Maybe a where
  Nothing :: Maybe a
  Just    :: a -> Maybe a

산술 표현식

아래와 같이 산술 표현식을 구현할 수 있는데 예를 들어 식 (5 + 1) * 7을 표현할 수 있다.

data Expr = I Int
          | Add Expr Expr
          | Mul Expr Expr
          deriving Show

eval :: Expr -> Int
eval (I n)       = n
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2

ghci> (I 5 `Add` I 1) `Mul` I 7
Mul (Add (I 5) (I 1)) (I 7)
ghci> eval it
42

Bool 타입 추가하기

식 5 + 1 == 7을 표현하기 위해 Bool 타입을 추가한다.

data Expr = I Int
          | B Bool
          | Add Expr Expr
          | Mul Expr Expr
          | Eq  Expr Expr
          deriving Show

식 5 + 1 == 7을 아래처럼 표현할 수 있다.

(I 5 `Add` I 1) `Eq` I 7

이 식을 eval로 평가하려면 함수 eval 타입을 아래처럼 바꿔야 한다.

eval :: Expr -> Either Int Bool

아래 두 경우는 구현하기 쉽다.

eval (I n) = Left n
eval (B b) = Right b

그런데 더하기나 곱하기는 어떻게 할 것인가?

eval (Add e1 e2) = eval e1 + eval e2

함수 +는 인자로 타입 Int를 기대할텐데 eval e1 타입은 Either Int Bool이므로 에러가 날 것이다. 게다가 eval 결과가 Int가 아니라 Bool이 오면 어떻게 처리할지 난감하다. 아래 식은 문법은 맞지만 말이 안 된다.

B True `Add` I 5 :: Expr

억지로 말이 되게 하려면 함수 eval 타입을 아래처럼 바꿔야 한다.

eval :: Expr -> Maybe (Either Int Bool)

팬텀 타입 Phantom types

data type 선언 시 타입 생성자에는 타입 변수가 있는데 값 생성자에서 그 타입 변수를 사용하지 않을 때 팬텀 타입이라고 한다.

아래와 같이 팬텀 타입을 이용해서

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

스마트 생성자 smart constructor를 만들면

add :: Expr Int -> Expr Int -> Expr Int
add = Add

b :: Bool -> Expr Bool
b = B

i :: Int -> Expr Int
i = I

이제 아래와 같은 식은 에러가 난다!

b True `add` i 5

식 b True 타입은 Expr Bool인데 스마트 생성자 add는 인자로 타입 Expr Int를 기대하기 때문에 에러가 난다.

함수 eval을 구현해보자.

eval :: Expr a -> a
eval (I n) = n

이렇게 하면 에러가 난다. 생성자 I만으로는 a가 Int인지 알 수 없다. 게다가 아래 식은 에러도 안 난다.

I 5 :: Expr String

스마트 생성자를 이용하는 방법은 유용하긴 하지만 위와 같은 문제를 해결하려면 생성자 자체로 타입을 제한할 수 있어야 한다.

GADTs

GADTs를 사용하려면 아래와 같이 GHC 확장을 사용해야 한다.

{-# LANGUAGE GADTs #-}

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

eval :: Expr a -> a
eval (I n) = n
eval (B b) = b
eval (Add e1 e2) = eval e1 + eval e2
eval (Mul e1 e2) = eval e1 * eval e2
eval (Eq  e1 e2) = eval e1 == eval e2

이제는 생성자 I만 봐도 타입 a가 Int인지 유추가 된다

대문