확장 ExistentialQuantification

ScopedTypeVariables
RankNTypes/Rank2Types
ExistentialQuantification
...

forall이 쓰는 확장은 매우 많은데, 여기서는 ExistentialQuantification 확장의 forall만 다룹니다.

원래 수학에서 쓰이는 뜻은
p를 만족하는 모든 값 forall x. p x
p를 만족하는 값이 존재한다면 exists x. p x

1차 술어 논리에서는 다음 둘이 동일하다.

(exists x. p x) -> q p를 만족하는 x가 존재하면 q이다.

forall x. (p x -> q) 모든 x가 p면 q이다를 만족한다.

이를 이용해 forall로 Existential Quntification을 붙일 수 있습니다.

이 확장을 켜면, 여러 타입들을 뭉뚱그려 하나의 타입으로 취급할 수 있습니다. 좀 더 학문적으로 얘기하면, 여러 타입을 추상화한 타입을 만들 수 있다고 말할 수 있습니다.

-- hetero 는 그리스어로 other, different를 의미한다.
{-# LANGUAGE ExistentialQuantification #-}
data T' = forall a. Show a => MkT' a

heteroList' = [MkT' 5, MkT' (), MkT' True, MkT' "Sartre"]
main = mapM_ (\(MkT' x) -> print x) heteroList'

위 소스에서 forall을 빼면

error: Not in scope: type variable ‘a’
2 | data T' = Show a => MkT' a

오류가 납니다. a가 뭔지 전혀 모르겠다는 오류입니다.

“a 가 무슨 타입이야?”
“몰라” vs “어떤 타입도(모든 타입이) 될 수 있어”

마치 둘 다 특정 타입을 콕 찝어 주지 않아, 같은 말처럼 느껴질지 모르지만, 전혀 다른 뜻을 가지고 있습니다. a는 가능한 타입이 하나일 수 있고, 여러 개일 수 있고, 모든 타입이 다 가능할 수도 있고, 하나도 없을 수도 있습니다. 이런 여러 가지 경우 중 어떤 건지 “몰라”와 이들 중 한 가지 경우인 “모든 타입이 될 수 있어”는 다른 정보,뜻입니다.

타입 서명을 써 줄 때 반드시 무슨 타입인지 써줘야 합니다. 컴파일러는 어떤 타입을 쓸 건지를 프로그래머한테 물어 봅니다. 그럼, 프로그래머는 타입 서명으로 대답하게 되는데, 어떤식으로든 항상 대답을 해야합니다. a라고만 (뭐든 소문자로 시작하면 다 폴리모픽을 의미합니다.) 써 주면, 컴파일러의 요청에 아무런 대답을 안하는 것과 마찬가지입니다.

여기다 forall a로 한정해 주면, 그 때서야  “응, 그건 모든 타입이 다 될 수 있어”  라고 대답 해주는 것과 같습니다. 그럼, 컴파일러는  “응, 그러면 나중에 구체 타입이 결정되겠군”  하고 넘어갑니다. 아주 야생적인informal 말로 하면, 타입 체크를 뒤로 미룬다고도 볼 수 있습니다.

※ 하스켈에서 특별한 quantifier 없이 쓰인 폴리모픽이 있는 서명들은 모두 암시적으로 가장 왼 쪽 바깥에 forall이 붙습니다.

forall 을 쓰면 5, (), True, "Sartre" 를 모두 다룰 수 있는 MkT' 이라는 타입을 만들 수 있습니다. Show a라는 제약을 주면 모든 타입이 아닌, show 함수를 적용할 수 있는 타입(달리 표현하면, Show 클래스의 인스턴스인 타입)으로 대상이 축소 됩니다.

forall 폴리모픽 변수를 만나면, 컴파일 타임에 코드 조합에 따라 컴파일러가 구체 타입을 결정합니다. 예를 들어, 타입을 받는 곳에 "a" 가 넘어가는 상황을 만나면 [Char] 타입이 되고, 'a' 를 만나면 Char 타입으로 추론됩니다.

영단어 뜻
existentially 실체론적으로, 실존(주의)적으로
quantified 뭔가를 울타리 안에 가두는, 한정, 제약
수학, 논리학에서 기호 ∃ (there exists) 입니다.

정리하면,

data S a = S a

오른쪽 a를 만나면, 컴파일러가 물어봅니다. “이 건 무슨 타입이야?”
“나중에 매개 변수(왼쪽 a)로 오는 거 보고 결정해” 라고 답해 준것과 같습니다.

data S = S a

이렇게 하면 컴파일러가 물어 볼 때, 아무런 대답을 안하는 것과 같습니다. 오류가 납니다.

data S = forall a. Show a => S a

“a가 폴리모픽”이라고 답하고, “a는 Show 클래스의 인스턴스인 타입이야” 라고 대답 하는겁니다. 야생적으로 얘기하면 “매개 변수로 받지 않아도 나중에 애매하지 않게 타입이 결정될거야” 라고 대답하는 옵션입니다. 대답을 듣고, 컴파일러는 타입 추론을 나중으로 미룹니다.

이걸 GADT 문법으로 표현하면, forall 을 생략해도 같은 의미입니다.

{-# LANGUAGE GADTs #-}
data S where
    S :: Show a => a -> S

Haskell/Existentially quantified types - wikibooks
Universal and Existential Quantification in Haskell - Serokell