타입 레벨 프로그래밍을 어디에 쓸까?

지난주 여행을 다녀오고 일기를 조금 쉬었다. 쓰고 싶을 때마다 마음대로 쓰는 일기라서 부담은 없다. 우리 회사는 매주 하스켈 위클리를 하고 있다. 사실 일정 맞추기가 어려워 1회를 진행했다. 나도 그렇지만 아직 모두 하스켈을 잘 아는 것이 아니기 때문에 서로 새로 알게 된 하스켈 지식을 공유하는 자리이다. 거기에 쌓여있는 주제들이 많이 있는데 그중, 다음 주에 공유할 내용을 오늘 일기로 써보려고 한다.

하스켈을 쓰려고 했을 때 가장 기대했던 기능이 타입 레벨 프로그래밍이다. 그만큼 관심이 많아 1회와 2회 하스켈 위클리 주제를 타입 레벨 프로그래밍으로 잡았다. 내부 컴포넌트 통신을 gRPC로 하기로 했기 때문에 여러 하스켈 라이브러리를 찾아보다가 mu-haskell이라는 패키지를 찾았고 서비스에 적용하고 있다.

mu-haskell은 타입 레벨 기능을 많이 사용하기 때문에 타입 레벨 프로그래밍을 잘 알아야 한다. 오늘 적을 내용은 타입 레벨 프로그래밍의 기초는 아니다. mu-haskell이 왜 타입 레벨 프로그래밍을 사용했는지 고민하고 느낀 점을 적어보려고 한다.

하스켈 타입 레벨 프로그래밍

그래도 아주 간단하게 하스켈에서 지원하는 타입 레벨 프로그래밍에 대해 적는 것이 좋겠다. 다른 언어들처럼 하스켈도 값과 타입이 있다. 값은 Term이라고 부르는데 값들은 타입에 속한다. 타입도 비슷한 종류로 묶을 수 있는데 대표적으로 타입 생성자와 타입은 다른 종류로 묶을 수 있다. 이렇게 타입을 묶은 것을 Kind라고 한다. 하스켈 GHCi에서 어떤 타입의 Kind를 확인할 수 있다.

> :kind Char
Char :: *
> :kind Maybe
Maybe :: * -> *

*라고 하는 것은 타입인데 NoStarIsType 언어 확장을 활성화하면 * 대신 Type으로 표시할 수 있다.

> :set -XNoStarIsType
> :kind Char
Char :: Type
> :kind Maybe
Maybe :: Type -> Type

Maybe 타입은 타입 변수를 하나 받기 때문에 Type -> Type Kind에 속한다. Type Class 같은 것은 Constraint라는 Kind에 속한다.

> :kind Monad
Monad :: (* -> *) -> Constraint

나만의 Kind도 만들 수 있는데 DataKinds 언어 확장을 사용하면 된다. DataKinds 언어 확장을 사용하면 data로 정의한 타입과 데이터 생성자가 각각 Kind와 타입으로 프로모션 된다.

data Flag = Red | Blue deriving (Eq, Show)

> :set -XDataKinds
> :type Red
Red :: Flag
> :kind 'Red 
'Red :: Flag

이렇게 Kind를 직접 만들 수 있다. DataKinds를 하면 1,2,3..과 같은 숫자 값(Term)과 "hello"와 같은 String 값이 각각 Nat Kind에 속하는 타입과 Symbol Kind에 속하는 타입으로 프로모션 된다. 따라서 1,2,3...이나 "hello"와 같은 값도 타입으로 쓸 수 있고 이러한 타입을 타입 레벨 리터럴이라고 한다.

> :kind 1
1 :: Nat
> :kind "Hello"
"Hello" :: Symbol 

Type level literal은 Term level로 변환할 수 있다.

data User a = User

userOne :: User 1
userOne = User

getUserValue :: forall a. KnownNat a => User a -> Integer
getUserValue _ = natVal (Proxy :: Proxy a)

-- >>> getUserValue userOne
-- 1

mu-haskell에서 타입 레벨 프로그래밍

mu-haskell은 gRPC나 GraphQL 스펙을 읽어 하스켈 타입으로 바꿔준다. 이때는 템플릿 하스켈 기능으로 코드를 생성한다. (템플릿 하스켈은 다음 일기 주제로 하면 좋겠다) gRPC나 GraphQL 스펙을 하스켈 코드로 어떻게 옮길 수 있을까? 예를 들어 다음과 같은 protoBuffer로 정의한 스펙이 있다고 해보자. 이것을 하스켈 코드로 어떻게 표현할 수 있을까?

message HelloRequest { string name = 1; }

아마 다음과 같이 하스켈 데이터 타입으로 만들 수 있을 것이다.

data HelloRequest = HelloRequest 
  { name :: String }
  
-- >>> HelloRequest "Todd"

이렇게 옮기면 될 것 같지만 사실 1이라고 하는 프로토콜 버퍼 아이디가 누락되었다. 이 정보는 어떻게 담을 수 있을까? 만약 다음과 같은 GraphQL Query 정의를 하스켈 타입으로 옮긴다면 어떻게 할 수 있을까?

type Query {
  author(name: String! = ".*"): Author
}

다음과 같이 최대한 옮겨볼 수 있을 것이다.

data Query = Query 
 { author :: String -> Author }

역시 필드 명인 name이라는 정보와 기본 값이 ".*" 정보는 누락되었다. 두 예제 모두 기본적인 하스켈 타입으로는 많은 것을 담지 못한다는 어려움이 있다.
그럼 다음과 같이 일반 데이터 타입으로 담으면 어떨까?

message HelloRequest { string name = 1; }

를 다음과 같이 하스켈 값으로 표현해보자.

messageSchema = ( "HelloRequest", ( "String", "name", 1 ))

그리고 실제 이 스키마에 해당하는 값은 다음과 같이 역시 하스켈 값으로 표현해 볼 수 있다.

messageValue = "Todd" 

이렇게 messageSchema과 messageValue로 표현했지만 두 값은 아무 관계가 없다. 그리고 컴파일 타임에 "Todd"라는 값이 messageSchema에서 정의하고 있는 String 타입이 맞는지 확인할 방법도 없다.

타입 레벨 프로그래밍으로 정보를 담기

이런 경우에 messageType을 타입으로 만들면 된다. DataKinds를 사용하면 Term 레벨을 타입 레벨로 올릴 수 있기 때문에 다음과 같은 타입을 만들 수 있다.

{-# LANGUAGE DataKinds #-}

type HelloRequestSchema = '( "HelloRequest", '( String, "name", 1 ) )

그리고 이 타입에 해당하는 값을 다음과 같이 정의해서 타입 변수로 연결해 볼 수 있다.

data Value s a = Value a deriving (Show)

-- >>> Value "Todd" :: Value HelloRequestSchema
-- Value "Todd"

하지만 단순히 Value s a에 타입 변수에 HelloRequestSchema 타입이라는 것을 알려줄 수 있지만 HelloRequestSchema가 정의하고 있는 String 타입인지 확인하는 것은 동작하지 않는다.

-- >>> Value 1 :: Value HelloRequestSchema
-- Value 1

스키마에 있는 타입을 컴파일 타임에 확인하기

Value 타입의 a 타입 변수가 HelloRequestSchema에 있는 String 타입과 일치하는지 확인하려면 기본 데이터 생성자(a -> Value s a)로는 힘들다. 하스켈은 GADT라는 언어 확장으로 기본 데이터 생성자 시그니처를 바꿀 수 있다. 다음은 GADT 확장을 사용해서 a 타입 변수가 HelloRequestSchema에 있는 String과 같은 타입을 보장하도록 정의한 데이터 생성자이다.

{-# LANGUAGE GADTs #-}

data Value s where
    Value :: a -> Value '( n , '( a , b , c) )

여기서 중요한 점은 a 타입이 HelloRequestSchema 타입의 안쪽에 있는 String 타입 위치에 오도록 제약한 점이다. 나머지 n,b,c 타입 변수는 사용하지 않는다. 이렇게 정의하고 Value를 생성해보면 다음과 같다. 그전에 Value 값을 확인할 수 있도록 Show 인스턴스를 만들자.

data Value s where
    Value :: (Show a) => a -> Value '( n , '( a , b , c) )

instance Show (Value HelloRequestSchema) where
    show (Value a) = show a

그리고 Value 값을 만들어 확인해보면 다음과 같다.

-- >>> (Value "Todd" :: Value HelloRequestSchema)
-- "Todd"
-- >>> (Value 1 :: Value HelloRequestSchema)
-- No instance for (Num String) arising from the literal ‘1’

이제 Value 데이터 생성자에 넘기는 타입이 HelloRequestSchema 스키마에 정의된 타입인 String이 아니면 컴파일이 되지 않는다.

여기까지 타입 레벨로 표현된 타입과 실제 타입 체크를 확인해봤다. 여기까지 오면서 그냥 String 타입으로 하면 되지 않느냐는 의문을 갖는다면 처음에 주의해서 읽지 않았기 때문이다. 중요한 점은 HelloRequestSchema는 값이 될 Value의 타입 정보만 가지고 있지 않고 프로토콜 버퍼 아이디와 필드명도 가지고 있다는 점이 중요하다. 그리고 이 정보는 앞에서 본 것처럼 Term 레벨에서 사용할 수 있다. 다음은 조금 더 확장성 있는 버전의 스키마를 정의하고 스키마에 있는 필드 명 정보를 사용해 showEntity를 구현한 예제이다. 이 예제는 mu-haskell을 만든 Alejandro Serrano의 발표 영상 예제를 참조해서 다시 만들었다.

data Field = Symbol ::: Type
type Schema = [ Field ]

type UserSchema = '[ "userid" '::: Integer
                   , "email" '::: String
                   ]

infixr 5 :&:
data Term (s :: Schema) where
    Nil :: Term '[]
    (:&:) :: v -> Term rs -> Term ((k '::: v) ': rs)

user3 :: Term UserSchema
user3 = 1 :&: "user3@example.com" :&: Nil

-- user4 :: Term UserSchema
-- user4 = "1" :&: "user3@example.com" :&: Nil -- 에러!!!! "1"이 Integer여야 한다!!

class ShowEntity (s :: Schema) where
    showEntity :: Term s -> String

instance ShowEntity '[] where
    showEntity Nil = ""

instance (KnownSymbol k, Show v, ShowEntity rs) => ShowEntity ((k '::: v) ': rs) where
    showEntity (v :&: rs) = symbolVal (Proxy :: Proxy k) ++ ": " ++ show v ++ "\n" ++ showEntity rs

>>> showEntity user3
userid: 1
email: "user3@example.com"