Type equality constraint "~"

Posted on July 14, 2020

인스턴스를 찾기 위한 타입 추론

Haskell Type Equality Constraints - Infinite Negative Utility 소스 발췌

{-# Language MultiParamTypeClasses #-}    
{-# Language FlexibleInstances #-}    
{-# Language TypeFamilies #-}    
{-# Language GADTs #-}    
    
class PairOf a b where    
    thePair :: (,) a b    
    
instance (Monoid a) => PairOf a a where    
    thePair = (mempty, mempty)    
    
obtuseMempty :: Monoid t => t    
obtuseMempty = fst thePair

컴파일 하면 b0를 추론할 수 없다고 나옵니다.

    • Could not deduce (PairOf t b0) arising from a use of ‘thePair’
      from the context: Monoid t
        bound by the type signature for:
                   obtuseMempty :: forall t. Monoid t => t
        at type.hs:12:1-29
      The type variable ‘b0’ is ambiguous

GHC가 인스턴스를 찾을 때는 constraint는 일단 제쳐두고, head로1 먼저 찾고, 그 다음 constraint를 봅니다.
obtuseMempty 함수는 Monoid 인스턴스를 리턴합니다. thePair 메소드는 모노이드 인스턴스의 튜플이니 여기서 fst로 첫 번째 걸 꺼내면 모노이드가 나올거라 예상할 수 있습니다. 왜 튜플의 두 번째 요소가 뭔지 모르겠다는 오류가 나왔을까요?
(Monoid a) => PairOf a a 에서 constraint를 보고 앞의 a와 뒤의 a가 같은 것으로 추론해줄 것 같은데 그렇지 않습니다. 같은 a를 받는다는 매칭 조건이지2, 추론 단서가 아닙니다.

GHC가 되어 추론해 봅시다.
어떤 instance의 thePair를 부를지 결정해야 합니다. (준비 되어 있는 인스턴스는 모노이드 인스턴스 두 개를 받는 인스턴스만 준비되어 있습니다.)
thePair 메소드를 찾으려면 PairOf a a 인스턴스를 찾는 단서인 a타입을 추론해야 합니다.
thePair에서 fst로 첫 번째 걸 꺼낸 게 obtuseMempty의 리턴 타입이니 첫 번째는 모노이드로 추론합니다.
그럼 두 번째는 뭘로 추론할까요? 두 번째 관련 단서가 젼혀 없습니다.
Monoid t => PairOf t b0 까지는 추론했는데, b0가 뭔지 모른다는ambiguous 에러입니다.

그럼 다음처럼 b도 모노이드로 추론할 수 있는 단서가 있을때는 어떻게 될까요?

obtuseMempty = mappend (fst thePair) (snd thePair)

거의 비슷하지만 이번엔 b0도 모르고 a0도 모르겠다는 에러가 납니다.


    • Could not deduce (PairOf t b0) arising from a use of ‘thePair’...
      The type variable ‘b0’ is ambiguous...
   |
13 | obtuseMempty = mappend (fst thePair) (snd thePair)
   |                             ^^^^^^^

    • Could not deduce (PairOf a0 t) arising from a use of ‘thePair’...
      The type variable ‘a0’ is ambiguous...
   |
13 | obtuseMempty = mappend (fst thePair) (snd thePair)
   |                                           ^^^^^^^

두 개다 추론할 단서가 있는데 왜 그럴까요?
fst thePair 와 snd thePair 에 있는 thePair는 같은 거란 단서는 없습니다.
그럼 두 개가 같을 경우는 어떻게 될까요?

obtuseMempty = let p = thePair                                   
               in mappend (fst p) (snd p)

ok입니다.

같은 모노이드 인스턴스로 이루어진 튜플을 만나면 PairOf클래스의 Monoid a => PairOf a a에 있는 thePair 메소드를 찾을 수 있습니다.

equality constraint ~

instance (Monoid a, a ~ b) => PairOf a b where    
    thePair = (mempty, mempty)

obtuseMempty :: Monoid t => t
obtuseMempty = fst thePair

a ~ b 는 a와 b가 같다는 뜻이 들어가면 에러가 나지 않습니다. 어차피 두 개다 a a 란 뜻인 것 같은데 왜 그럴까요?
Pair a a 라고 쓴 것과 a ~ b => Pair a b 는 다르게 작업이 진행됩니다. a a 인 경우는 인스턴스를 찾을 때 두 개 인자가 같은 타입인 경우만 매칭 되는데, a b 는 일단 인자가 두 개인 것과 매칭됩니다. 그 다음 b를 a와 같은 타입으로 추론합니다. a ~ b 를 constraint에 넣어서 a와 b가 같다는 정보를 head에서 constraint로 옮겼습니다. 인스턴스 resolution은 head 해석 후 constraint로 가니 두 개가 같아야 한다는 정보는 나중으로 미뤘다는 얘기입니다.3
이 번에는 (t, b0)로 추론한 후, 인스턴스를 찾으니 Pair a b와 매칭에 성공하고, b0를 a와 같은 타입으로 추론합니다. a ~ b 의 뜻은 “b가 당장 뭔지 몰라도 돼, 나중에 b는 a와 같은 타입으로 추론할거야” 란 뜻입니다.
GHC는 최종 (Monoid t) => (t, t) 로 추론합니다.

constraint를 이용한 선언과 타입 지정 선언 비교

https://memo.barrucadu.co.uk/tilde-instance-pattern.html 발췌

{-# Language FlexibleInstances #-}
{-# Language FlexibleContexts #-}
{-# Language GADTs #-}
{-# Language TypeFamilies #-}

newtype WrappedFunctor f a = WrappedFunctor (f a) deriving Show

instance Functor (WrappedFunctor Maybe) where -- (1)
  fmap f (WrappedFunctor fa) = WrappedFunctor (fmap f fa)

instance (f ~ Maybe)=> Functor (WrappedFunctor f) where -- (2)
  fmap f (WrappedFunctor fa) = WrappedFunctor (fmap f fa)

((1), (2) 동시에 정의하면 Overlap 됐다고 에러가 납니다. 하나씩만 정의해서 테스트 하세요.)

(1)번으로 정의하면

> :t fmap (+1) (WrappedFunctor (pure 3))
  :: (Num b, Applicative f, Functor (WrappedFunctor f)) =>
     WrappedFunctor f b
> fmap (+1) (WrappedFunctor (pure 3))
error:
    • Ambiguous type variable ‘f0’ arising from a use of ‘print’...

Maybe로 추론됐을 때만 (1)번 인스턴스와 매치되기 때문에, 위 구문은 어떤 인스턴스와도 매치되지 않은 상태입니다.

(2)번으로 정의하면

> :t fmap (+1) (WrappedFunctor (pure 3))
  :: Num b => WrappedFunctor Maybe b

> fmap (+1) (WrappedFunctor (pure 3))
WrappedFunctor (Just 4)

Pure 3을 만나도, 이걸 (2)번과 매칭에 성공하고, f를 Maybe로 추론합니다.

정리하면 constraint를 써서 정의하면 Maybe일수도 있는 걸 만나면 Maybe로 추론할 수 있습니다.
~는 constraint에 타입 추론 절차 하나를 심어 놨다고 보면 됩니다.

실제 코딩에서는 하나의 인스턴스만 필요할 때, 알아서 한가지로 추론되길 바랄 때 쓰는 트릭이라고 합니다.

참고

  1. Lazy 패턴 매치에서도 ~가 보이는데, 보통 ~가 쓰일 때는 그냥 같은게 아니라, 어떤 절차나 추론을 거치고 나면 같아질 때를 의미합니다.

  2. 어떤 값으로 추론되는지 볼 때 hole을 이용하면 도움이 됩니다.

> :t fst
fst :: (a, b) -> a
> 

> :t fst _

<interactive>:1:5: error:
    • Found hole: _ :: (a, b0)
      Where: ‘b0’ is an ambiguous type variable
             ‘a’ is a rigid type variable bound by
               the inferred type of it :: a
               at <interactive>:1:1
    • In the first argument of ‘fst’, namely ‘_’
      In the expression: fst _

  1. 인스턴스 표현식의 부분 부분을 다음처럼 부릅니다.

    instance (Num t) => SomeC [t] where
      constraint      head
    ↩︎

  2. 인스턴스의 constraint는 추론 단서로 쓰이는게 아닙니다. GHC가 constraint를 보고 타입을 추론해 주는게 아니라, 이미 다른 단서들을 이용해 타입을 추론하고, 그 다음 추론된 타입이 constraint에도 부합하는지 확인합니다. 추론된 타입이 constraint 조건을 만족하지 않으면 그냥 에러입니다. 하지만, ~가 들어가면 이건 추론 단서로 쓰인다고 볼 수 있습니다.↩︎

  3. 인스턴스 resolution 순서

    왜 인스턴스 resolution 부를까요? resolution은 뭔가를 구분해 내는 걸 뜻합니다. 여러 개의 인스턴스가 있을 때, 각각을 구별해서 뭔지 알게 되는 걸 resolution 이라 부를 수 있을 것 같습니다. 하는 일은 적당한 인스턴스를 찾는 걸 말합니다.
    영단어 뜻 : 조직이나 단체가 투표를 해서 정한 공식적인 결정

    instance (MyClass a, MyClass b) => MyClass (a, b) where

    직관대로, 순서대로 읽으면 a가 MyClass이고, b가 MyClass일 때 (a,b)가 MyClass 인스턴스라 읽으면 될 것 같지만, GHC가 추론할때는 반대 순서로 추론합니다. head를 먼저 해석하고, 그 다음 constraint를 해석합니다.
    가장 먼저 MyClass (a, b) 를 찾고, 그 다음 a가 MyClass 인스턴스인지, b가 MyClass 인스턴스인지 살펴봅니다.

    그리고, 인스턴스를 찾을 때 constraint는 영향을 주지 않습니다. head만 보고 매칭을 시도합니다.↩︎

Github 계정이 없는 분은 메일로 보내주세요. lionhairdino at gmail.com