Написание функции Полиморфизм в семействе типов

Я экспериментировал с семействами типов вчера и столкнулся с препятствием со следующим кодом:

  {-# LANGUAGE TypeFamilies #-}

  class C a where
      type A a
      myLength :: A a -> Int

  instance C String where
      type A String = [String]
      myLength = length

  instance C Int where
      type A Int = [Int]
      myLength = length

  main = let a1 = [1,2,3]
             a2 = ["hello","world"]
         in print (myLength a1)
            >> print (myLength a2)

Здесь у меня есть тип, связанный с классом C и функция, которая вычисляет длину связанного типа. Однако приведенный выше код дает мне эту ошибку:

 /tmp/type-families.hs:18:30:
     Couldn't match type `A a1' with `[a]'
     In the first argument of `myLength', namely `a1'
     In the first argument of `print', namely `(myLength a1)'
     In the first argument of `(>>)', namely `print (myLength a1)'
 /tmp/type-families.hs:19:30:
     Couldn't match type `A a2' with `[[Char]]'
     In the first argument of `myLength', namely `a2'
     In the first argument of `print', namely `(myLength a2)'
     In the second argument of `(>>)', namely `print (myLength a2)'
 Failed, modules loaded: none.

Если, однако, я изменяю "тип" на "данные", код компилируется и работает:

  {-# LANGUAGE TypeFamilies #-}

  class C a where
      data A a
      myLength :: A a -> Int

  instance C String where
      data A String = S [String]
      myLength (S a) = length a

  instance C Int where
      data A Int = I [Int]
      myLength (I a) = length a

  main = let a1 = I [1,2,3]
             a2 = S ["hello","world"]
             in
               print (myLength a1) >>
               print (myLength a2)

Почему "длина" работает не так, как ожидалось в первом случае? Строки "type A String..." и "type A Int..." указывают, что тип "A a" - это список, поэтому myLength должен иметь следующие типы соответственно: "myLength:: [String] → Int" или "myLength:: [Int] → Int".

Ответ 1

Hm. Давайте забудем о типах на мгновение.

Скажем, у вас есть две функции:

import qualified Data.IntMap as IM

a :: Int -> Float
a x = fromInteger (x * x) / 2

l :: Int -> String
l x = fromMaybe "" $ IM.lookup x im
  where im = IM.fromList -- etc...

Скажите, что существует какое-то значение n :: Int, о котором вы заботитесь. Учитывая только значение a n, как вы находите значение l n? Разумеется, вы этого не сделаете.

Как это уместно? Ну, тип myLength равен A a -> Int, где A a является результатом применения "функции типа" A к некоторому типу A. Тем не менее, myLength является частью класса типа, параметр class A используется для выбора реализации myLength для использования. Итак, учитывая значение какого-либо определенного типа B, применение myLength к нему дает тип B -> Int, где B ~ A a, и вам нужно знать A, чтобы найти реализацию myLength. Учитывая только значение A a, как вы находите значение A? Конечно, вы этого не делаете.

Вы можете обоснованно возразить, что в вашем коде функция A обратима, в отличие от функции A в моем предыдущем примере. Это верно, но компилятор ничего не может с этим сделать из-за предположения открытого мира, где задействованы классы типов; теоретически, ваш модуль может быть импортирован другим модулем, который определяет свой собственный экземпляр, например:

instance C Bool where
    type A Bool = [String]

Глупый? Да. Действительный код? Также да.

Во многих случаях использование конструкторов в Haskell служит для создания тривиально-инъективных функций: конструктор вводит новую сущность, которая определяется только и уникально аргументами, которые она дала, что упрощает восстановление исходных значений. Это как раз разница между двумя версиями вашего кода; семейство данных делает функцию типа обратимой, определяя новый, различный тип для каждого аргумента.