OOP에서도 variance를 유용하게 써먹기는 하지만, FP에서는 그거랑 비교도 안되게 할말이 많음. variance은 원래 카테고리 이론에서 나온건데 FP는 카테고리하고 관련이 워낙 깊어서.

* 커링 이런것 까지는 설명할 수가 없어서 그냥 쓸건데, 하스켈이나 함수형 프로그래밍 지식이 전혀 없으면 알아듣기 힘들 수 있음.

FP에서 variance는 covariant/contravariant functor로 정의됨.
먼저 covariant functor에 해당하는 하스켈 Functor를 보자.
class Functor (f :: Type -> Type) where
  fmap :: (a -> b) -> (f a -> f b)

f는 Type -> Type의 kind signature를 가지는 HKT인데, OOP에서 봤던 List<A>랑 마찬가지로 타입인자를 1개 받는 고차 타입임.
fmap은 이 f에 대해서 정의된 함수고, 흔히 리스트 map이라고 말하는 함수의 일반화임.

그리고 유의미한 구현을 강제하기 위한 functor law가 있는데, 당장은 중요하지 않으니 그냥 넘어감.

구체적인 인스턴스를 하나만 들어보자.
data List a = Nil | Cons a (List a)
instance Functor List where
  fmap f Nil = Nil
  fmap f (Cons x xs) = Cons (f x) (fmap f xs)

그냥 타입 정의에서 a가 나타나는 모든 부분을 f를 사용해서 b로 치환한다고 생각하면 쉬움.

contravariant functor는 위의 fmap에서 함수의 방향만 반대임.
class Contravariant (f :: Type -> Type) where
  contramap :: (a -> b) -> (f b -> f a)
  -- 혹은 타입변수 이름만 바꿔서,
  -- contramap :: (b -> a) -> (f a -> f b)

FP에서도 contravariant는 함수타입에서 나옴.
newtype Predicate a = Predicate (a -> Bool)
instance Contravariant Predicate where
  contramap f (Predicate p) = Predicate (p . f)

딱봐도 OOP에서 설명했던 covariance, contravariance하고 비슷한 느낌이 듬.
카테고리로 설명하자면 FP에서는 morphism이 a -> b, OOP에서는 a <: b인 차이일 뿐임.

covariant를 positive, contravariant를 negative 취급하는것도 똑같음.
기본적인 3가지 예시를 보면
product type (tuple) : (+a, +b)
sum type : Either (+a) (+b)
function type : (-a) -> (+b)

하스켈 ADT는 원리적으로 이 3가지 만으로 구성되기 때문에 이걸로 variance를 다 알 수 있음.
그래서 컴파일러 확장을 켜면 derive Functor같은것 까지 가능함. (펑터 구현을 자동으로 해줌)

이제 저번에 미뤄뒀던 Bivariant/Invariant 이야기를 좀 해보자.
먼저 Bivariant f는 f가 covariant 이면서 동시에 contravariant 인걸 말함.
굳이 코드로 정의해보자면
type Bivariant f = (Functor f, Contravariant f)
  -- constraint synonym

이런 타입이 실존하는지 의심스러울 수 있는데, 의외로 허망함.
newtype Const a b = Const a

Const 타입은 특이하게 인자로 받은 b를 전혀 사용하지 않는데, 이런걸 phantom type이라고 부름. b가 사용되지 않으니 fmap과 contramap이 자명하게 존재하고 따라서 Const a b는 b에 대해 covariant하면서 동시에 contravariant함.

사실 모든 bivariant는 이런 phantom type만이 가능하고, 결국 아래 같은 일이 벌어짐.
phantom :: (Functor f, Contravariant f) => f a -> f b

즉 a -> b 같은 함수 인자 없이도 f a -> f b를 만들 수가 있음.

invariant는 OOP에서도 이야기 했지만, covariant하지도 contravariant하지도 않은걸 말함.
data Foo a = Foo [a] (a -> Bool)

이 경우, a -> b로는 a -> Bool이 처리가 안되고, b -> a 로는 [a]가 처리가 안됨.
그런데 invariant functor에 대해서도 유용한 class를 정의할 수 있음
class Invariant (f :: Type -> Type)
  invmap :: (a -> b) -> (b -> a) -> (f a -> f b)

invmap은 a -> b와 b -> a를 모두 인자로 받음. 흔히 있는 일은 아니지만 HOAS같은거 할때 쓴다는듯.

여기까지만 하면 섭섭하니까 recursive type이야기를 좀 해보겠음.
data Nat = Z | S Nat

이건 증명언어 등에서 흔히 사용하는 자연수 정의임. Nat의 정의에 Nat이 재귀적으로 사용되었기 때문에 이런 타입을 재귀적이라고 부름.

그런데 카테고리 이론에 따르면 재귀적 타입은 functor와 관련이 깊음. 카테고리에서 재귀적 타입은(용어는 좀 다르지만) (covariant) endofunctor의 fixed point로 정의됨.

여기서 fixed point라는건 endofunctor F에 대해 F(X) ~ X, 그러니까 F(X) 와 X가 isomorphic해지는 X를 말함.
수학에서 흔히 나오는 fixed point f(x) = x 랑 유사해서 그렇게 불림.

덧붙여서 endofunctor의 fixed point는 한개가 아닐 수 있는데, fixed point를 얻는 두가지 방법중 initial algebra로 정의되는 fixed point가 data, terminal coalgebra로 정의되는 fixed point가 codata에 해당함. 하스켈에서 흔히 다루는 무한 리스트도 이거랑 관련되있음. (증명언어에서는 termination checking을 위해서 data/codata를 구분함.)

위의 Nat 타입을 fixed point를 사용해서 정의해보자면
newtype Fix f = Fix (f (Fix f))
newtype Nat =  Nat (Fix Maybe)

이렇게 됨. 밈스럽게 말하자면
"Natural number is just an initial o-bject in the category of algebras of maybe functor"

그런데 하스켈은 이 관점에 부합하지 않는 재귀적 타입도 허용함. 예를들어서
data Foo where
  Foo :: (Foo -> Void) -> Foo

newtype F a where
  F :: (a -> Void) -> F a

여기서 Foo는 F의 fixed point로 봐야하는데, 문제는 F가 contravariant functor라는 점임. 위에서 말했던 initial algebra/terminal coalgebra를 사용한 fixed point는 covariant functor에서만 정의됨.

게다가 위의 정의는 curry's paradox 때문에 Void를 증명하는데 사용할 수 있음. 혹은 재귀 없이 무한루프를 만들어내는데 사용할 수 있다고 생각하면 됨.

그래서 coq, agda, idris 같은 언어에서는 재귀적 데이터 타입을 정의할 때 strictly positive functor 에 대해서만 허용함. positive는 당연히 covariant를 말하는거고, strict 라는건 단순한 covariant보다 더 강한 조건인데 그 타입이 negative position에 오는 일이 없어야 한다는 말임.

예를들어 생성자의 타입에 따라서 아래와 같이 분류됨.
MkF :: a -> F a
  -- F는 strictly positive
MkF' :: (a -> Bool) -> F' a
  -- F'은 negative
MkF'' :: ((a -> Bool) -> Bool) -> F'' a
  -- F''은 positive, 그러나 strictly positive는 아님

사실 curry's paradox에 직접 해당하는건 negative인 경우고, non strict positive가 금지되는건 조금 다른 이유라고 함. coq에서 non strict positive를 가지고 모순을 증명하는건 아래 링크에 설명되있음. agda는 non strict positive를 허용해도 모순이 생기지 않을걸로 생각된다는듯.

그렇다고해서 contravariant, 혹은 invariant한 functor의 fixed point가 무의미한건 아니고, HOAS를 사용하기 위해서는 필수적임. HOAS는 FP에서 엄청 밀어주는 기능인데, 아이러니하게 함수형언어 최첨단인 증명언어에서는 curry's paradox 때문에 사용이 불가능함. 영영 안될것 같지는 않고, 타입이론이 더 발전하면 HOAS를 사용하면서도 termination checking이 가능한 언어가 나오지 않을까 싶음. (지금도 있는데 사용할 수준은 아닌걸로 앎)

현재로서는 HOAS를 사용하고싶다면 하스켈이 제일 나을거임.

- dc official App