확장 InstanceSigs (작성 중)

생각 스트레칭

Supertype, Subtype

forall a.a -> a와 Int -> Int 둘 중 누가 Supertype이고, 누가 Subtype일까요?
엄밀히 말하면, 하스켈엔 서브 타이핑이 없으므로-예) Int와 Double, 둘 모두의 Supertype이 되는 Number 타입 같은 게 없습니다.-, 누가 Super처럼 보이고, 누가 Sub처럼 보이느냐고 물어야 합니다.
forall a.a -> a는 어떤 타입을 받아도 되는 구현을 가졌으니, 이 구현을 Bool -> Bool로 봐도, Int -> Int로 봐도 문제가 없다는 말입니다. forall a.a -> a에 인자로 Int를 넣어줘도, Bool을 넣어줘도 문제가 없습니다. 이렇게 모든 타입에 대응하니, 당연히 더 forall a.a -> a가 Super해 보이긴 하는데, 함정이 있습니다.

func1 :: (Int -> Int) -> Int 
func2 :: (forall a.a -> a) -> Int 

func1에는 인자로 forall a.a -> a를 넘길 수 있습니다. 하지만,
func2에는 인자로 Int -> Int를 넘길 수 없습니다.

무슨 말이냐 하면, func1이나, func2는 인자로 함수를 받았으니, 그 함수들을 실행하기 위해서, 내부에서 인자를 넣어 줄 겁니다.

이 때, func2 함수 내부에서는 (forall a.a -> a)가 들어오면, 이 함수가 무슨 타입이든 문제 없다고 하니, 뭘 넣어 줄지 모릅니다. 한 타입이 아니라, 여러 타입을 넣고 있을 수도 있습니다. Int를 넣어도 문제 없어야 하고, Bool을 넣어도 문제 없어야 합니다. 그런데, 여기에 Int -> Int가 들어오면, 반드시 Int만 받아야 되는 상황이 됩니다.

이 번엔, func1을 보겠습니다. func1은 Int -> Int 함수를 받아 내부에서 Int를 넣어 줄 겁니다. 그런데 여기에 forall a.a -> a를 넣으면 어떻게 될까요? 어떤 타입이든 받아준다 했으니, 당연히 Int가 들어와도 아무 문제 없습니다.

정리하면, Int -> Int 자리에는 forall a.a -> a를 넣어줄 수 있고,
forall a.a -> a자리에는 Int -> Int를 넣어줄 수 없습니다.

하스켈엔 서브 타이핑이 없지만, 대체 가능 여부로 subtype, supertype을 나눈다면 forall a.a -> a는 Int -> Int의 subtype처럼 볼 수 있습니다.

Type families are functions from types to types

Why is forall a.a not considered a subtype of Int…

InstanceSigs

GHC 공식 문서 - 6.8.8.5. Instance signatures: type signatures in instance declarations

GHC2021에 포함되어 있습니다.

인스턴스를 정의할 때, 메소드의 서명을 써 줄 수 있습니다.

data T a = MkT a a
instance Eq a => Eq (T a) where
  (==) :: T a -> T a -> Bool   -- 인스턴스 메소드에 서명을 붙여 주고 있습니다.
  (==) (MkT x1 x2) (MkTy y1 y2) = x1==y1 && x2==y2

그냥 써 줄 수 있는 게 아니라, Class 선언과 같거나 더 폴리모픽하게 써 줄 수 있습니다.

instance Eq a => Eq (T a) where
   (==) :: forall b. b -> b -> Bool
   (==) x y = True

Eq클래스 정의는 아래와 같습니다.

class  Eq a  where
  (==) :: a -> a -> Bool

서명만 따로 모아 보면

  (==) :: a -> a -> Bool -- 클래스에 있는 서명
  (==) :: T a -> T a -> Bool   -- 인스턴스 메소드에 서명을 붙여 주고 있습니다.
  (==) :: forall b. b -> b -> Bool -- 클래스에 있는 서명과 같거나 더 폴리모픽해야 합니다.

두 번째보다 세 번째가 더 폴리모픽하면 됩니다. 이 때, 서명이 같거나 더 폴리모픽한지 체크하기 위해, GHC는 sub-type체크를 수행합니다. 생각 스트레칭에서 봤던 것처럼 이들 타입을 인자로 받는다고 가정하면,
T a -> T a -> Bool에는 forall b.b -> b -> Bool이 들어갈 수 있습니다. 왜냐 하면, T a -> T a -> Boool보다 forall b.b -> b -> Bool이 더 폴리모픽하기 때문입니다.