타입 클래스, 타입 추론, Dependent Haskell

타입 클래스

정적 타입이란, 컴파일 타임에 지정된 타입끼리 만나지 않는 상황이 생기면 마리 알려줘서 실행 타임에 오류를 줄이자는 것입니다. 그런데, 이 장점을 이용하려다 보니, 코딩시 일일이 타입을 “고정” 해야 하는 단점이 있습니다. 타입이 고정되면, 비슷한 동작을 하는, 아니 거의 같은 동작을 하는 함수들을 타입에 따라 모두 준비해야 합니다. (+) 함수를 정의하는데, Int 값을 받아들이게 만들었다면, Float를 위한 (+)를 또 만들고, 인자의 타입에 맞는 (+)를 골라서 써야 합니다.

• 타입별로 함수를 준비해야 하는 건 달라지지 않지만, 타입별 함수를 컴파일러가 자동으로 만들어 주면, 프로그래머 입장에선 (+) 함수 하나만 만들면 “여러 타입에 동작한다” 와 다를게 없는 상태로 만들 수 있습니다.

• 조금 더 확장해서, 라이브러리에선 일일이 타입별로 정의하지만, 컴파일러가 적절한 타입을 고르게 해서, 프로그래머가 타입에 대한 신경을 끌 수 있다면, 그 또한 “여러 타입에 동작한다”와 다를게 없습니다.

정적 타입 언어인 하스켈에서 타입 클래스 + 타입 추론을 써서 위와 같은 개념을 구현합니다.

코딩할 때, 타입을 고정하지 않고 열어 두면, 컴파일러가 타입 추론을 이용해 타입을 고정합니다. 열어 둘 때 활짝 열어 아무 타입이나 다 가능하게 해 놓을수도 있고, 살짝 열어, 특정 성격의 타입만 받아들이게 할 수 있습니다.

타입 추론

폴리모픽 매개 변수 forall a. a를 두면, GHC가 코드 조합을 할 때, 타입 결정을 뒤로 미루는 효과가 납니다. 하스켈의 타입 추론은 마치 하스켈의 Lazy한 함수 실행처럼 Lazy하게 타입을 결정합니다. 어떤 분류의 타입만 받게끔 해서 코드를 조합하다가 구체 타입이 필요한 시점이 되어서야 타입이 뭔지 결정합니다. 심지어 끝끝내 구체 타입을 알 필요가 없는 경우도 있긴 있습니다.(ex. length함수, 컨테이너 안에 들어 있는 엘리먼트 수만 세기때문에 엘리먼트 자체가 뭔지 알 필요가 없습니다.)
어찌됐든 GHC가 알아서 단서들을 모아서 타입 추론을 하는데, 이 때 GHC가 써먹도록 만드는게 타입 레벨 함수입니다.

타입 레벨 프로그래밍

Dependent Haskell

이렇게 할 수 있는 이유는, 하스켈은 강력한 타입 추론 기능을 가지고 있기 때문입니다. 이렇게 강력한 기능을 좀 더 적극적으로 써보자는 개념이 Dependent Haskell 입니다. (하스켈에서 가지를 친 이드리스Idris 언어는 이 개념에 특화되어 있는 언어입니다.)

Dependent Function
https://serokell.io/blog/why-dependent-haskell

카인드 Kind

Int를 받고 Int를 내뱉는 함수라면, 2같은 값을 받아 연산해서 3같은 값을 결과로 내 뱉습니다.
* -> * 카인드를 받고 * 카인드를 내 뱉는 타입 레벨 함수는 결과로 Int같은 타입을 내 뱉습니다.

1,2,3... 등을 뭉뚱그려서(추상화 해서) Int 타입이라 분류했습니다.
Int, Double, Char 등을 뭉뚱그려서 * 카인드로 분류하고
Maybe a, List a, Some a 등을 뭉뚱그려서 * -> * 카인드로 분류합니다.

값은 타입으로 분류하고(추상화하고), 타입은 카인드로 분류(추상화)합니다.

런타임에는 타입이 없다

타입은 컴파일 타임에 코드를 “조립”할 때만 필요합니다. 예를 들어, 반드시 Int 타입만 받게 지정해 놓은 타입에 Double을 내뱉는 코드 조각이 맞춰지는 상황이 오면 문제를 잡아냅니다. 이렇게 타입 체크를 일일이 하면서 문제 없이 모든 코드 조각을 맞췄다면(타입 추론을 통과했다면), 타입이 달라 문제가 생기는 경우는 없게됩니다. 그러면 런타임에는 굳이 타입 정보를 끌고 다녀야 할 이유가 없어집니다. 그렇기 때문에 타입 레벨 프로그래밍도 컴파일 타임까지만 노리고 개념을 활용하는데, 너무 적극적으로 쓰다 보면 런타임에도 타입 레벨에 있는 정보가 필요할 때가 있습니다. 이럴 때 싱글턴 라이브러리의 도움을 받습니다.

참고 - stackoverflow - type level programming meaning at run time
## 타입 레벨과 값 레벨을 이어주는 브릿지 처음 볼 때, 타입 레벨에 존재하는 정보들을 값 레벨로 가져오는 방법이 궁금했습니다. 두 레벨을 이어주는 방법은 reflection, singleton 패턴등이 있다고 말합니다. 복잡하게 생각했는데, 엄밀히 말하면, 두 레벨을 이어주는 방법은 타입 인스턴스 뿐이 없습니다. 예를 들어 Int -> Bool 이라 하면, Int 타입과 Bool 타입을 이어주는 함수입니다. 서로 다른 타입인데 연결을 맺듯이, 타입과 값을 이어 주는 것도 어딘가의 함수로 나타날 거라 예상할 수 있습니다. Int가 뭐냐에 따라 Bool값이 달라지는 걸 함수라 합니다. 1 - True, 2 - False, 3 -True… 처럼 매핑을 해놓으면 함수 구실을 하게 됩니다. 마찬가지로 타입과 값이 매핑되는 방법을, 하스켈 문법에서 찾으면, 바로 타입 클래스와 인스턴스입니다.

data One
data Two

class ValueInType t where
  get :: Proxy t -> Int

instance ValueInType One where
  get _ = 1

instance ValueInType Two where
  get _ = 2

위와 같이 Three, Four … 타입들을 만들면, 타입 레벨에 자연수를 만들 수 있을 겁니다. 설마, 이 걸 다 만들까 싶은데, Nat kind의 윈리가 이 것과 같습니다. 값 1,2…는 타입으로 그룹짓고, 1,2… 타입은 Nat 카인드로 그룹 짓습니다.

※ Nat,Symbol,Char 카인드(타입이 아닙니다.)는 GHC에 하드 코딩된 리터럴 카인드입니다. 아마도 이들을 위해 특별한 동작이 GHC에 들어가 있을 거라 예상합니다. GHC의 아무런 지원 없이 타입 레벨 프로그래밍을 하긴 어렵습니다.

-- 보통 class Some a where 라고 써서 * 카인드에 대한 클래스를 정의하는데,
-- 여기선 Nat 카인드에 대해서 정의하고 있습니다.
-- 이 클래스"류"가 되려면, 즉 Nat 카인드 타입만 인스턴스를 만들 수 있습니다.
-- SNat은 Singleton Natural을 의미합니다.
-- Int 타입, Bool 타입, 1 타입, 2 타입, ... 낯설긴 하지만, 여기서 1은 값이 아니라 타입을 의미합니다. 실제 코드로 3 타입, 4 타입 ...을 모두 정의하는 것이 아니라, GHC가 컴파일 타임에 내부적으로 Adhoc한 방식으로 처리할 거라 예상합니다.
-- 1 타입, 2 타입, ... 들은 Nat 카인드로 그룹 지었습니다.
-- KnownNat 클래스는 1타입, 2타입... 등과 매핑되는 대상을 정해주는 함수입니다. 1 타입과 매핑되는 natSing의 결과값은 SNat 1타입 입니다.
class KnownNat (n :: Nat) where
  natSing :: SNat n -- Some Intger 랑 비교


-- 보통 data SNat a where 로 정의하는데, 여기선 Nat 카인드 타입만 해당합니다.
data SNat (n :: Nat) where
  SNat :: Integer -> SNat n
  -- SNat 값 생성자는 정수를 받아, Nat 카인드 타입을 가진 SNat 타입을 반환합니다.

natVal :: forall n proxy. KnownNat n => proxy n -> Natural
natVal _ = case natSing :: SNat n of
             UnsafeSNat x -> x

This class gives the integer associated with a type-level natural.
이 클래스는 타입 레벨 자연수와 연관된 정수를 돌려 준다. GHC-TypeLits

클래스가 값을 준다는 조금은 이상한 표현처럼 느껴집니다. 생각해 보면, 클래스는 타입에 대응하는 여러 인스턴스들을 정의하는 방법으로, (인스턴스에 있는 메소드들은 결국 값을 돌려 주니) 타입에 따른 “값”을 돌려 주는 함수입니다.

싱글턴 라이브러리

런타임에는 타입 정보가 모두 사라집니다. 컴파일 타임을 넘어 런타임에도 타입 레벨에 있는 정보가 필요할 경우, 값 레벨로 정보를 복사해 놓을 때 쓰는 라이브러리입니다.
https://ryanglscott.github.io/2019/08/29/how-ghc-8-8-nearly-killed-singletons/
https://blog.jle.im/entry/introduction-to-singletons-1.html

필요한 확장

TypeFamilies
DataKinds
PolyKinds
GADTs
RankNTypes
ScopedTypeVariables
TypeApplications
TypeOperators
MultiParamTypeClasses
FlexibleContexts
FlexibleInstances