Несоответствие подписи типа в определении экземпляра Bifunctor

Question

Я узнаю о Haskell, работая над книгой " Программирование на Haskell от первых принципов", Аллен и Моронуки.

В упражнениях к главе о преобразователях монад, функторах и аппликативной композиции читателю предлагается написать экземпляр бифунктора для следующего типа

data SemiDrei a b c = SemiDrei a

Моя первая попытка (которая компилируется) была

instance Bifunctor (SemiDrei a) where
    bimap f g (SemiDrei a) = SemiDrei a

Но, глядя на это, мне казалось, что я должен уметь писать bimap f g = id потому что последний аргумент остается неизменным или напишите bimap f g x = x. Оба дали мне ошибки компиляции, и я надеюсь, что кто-нибудь сможет объяснить мне, почему я не могу выразитьbimap с этими более короткими альтернативами, т.е. почему я должен указывать (SemiDrei a).

Я запускал это на Haskell 8.6.5 (если это актуально)

попытка: id

instance Bifunctor (SemiDrei a) where
    bimap f g = id

-- compile error message:
• Couldn't match type ‘a1’ with ‘b’
  ‘a1’ is a rigid type variable bound by
    the type signature for:
      bimap :: forall a1 b c d.
               (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
    at src/Main.hs:69:5-9
  ‘b’ is a rigid type variable bound by
    the type signature for:
      bimap :: forall a1 b c d.
               (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
    at src/Main.hs:69:5-9
  Expected type: SemiDrei a a1 c -> SemiDrei a b d
    Actual type: SemiDrei a b d -> SemiDrei a b d
• In the expression: id
  In an equation for ‘bimap’: bimap f g = id
  In the instance declaration for ‘Bifunctor (SemiDrei a)’
• Relevant bindings include
    f :: a1 -> b (bound at src/Main.hs:69:11)
    bimap :: (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
      (bound at src/Main.hs:69:5)
   |
69 |     bimap f g = id
   |                 ^^

попытка: f g x = x

instance Bifunctor (SemiDrei a) where
    bimap f g x = x

-- compile error message:
• Couldn't match type ‘a1’ with ‘b’
  ‘a1’ is a rigid type variable bound by
    the type signature for:
      bimap :: forall a1 b c d.
               (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
    at src/Main.hs:69:5-9
  ‘b’ is a rigid type variable bound by
    the type signature for:
      bimap :: forall a1 b c d.
               (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
    at src/Main.hs:69:5-9
  Expected type: SemiDrei a b d
    Actual type: SemiDrei a a1 c
• In the expression: x
  In an equation for ‘bimap’: bimap f g x = x
  In the instance declaration for ‘Bifunctor (SemiDrei a)’
• Relevant bindings include
    x :: SemiDrei a a1 c (bound at src/Main.hs:69:15)
    f :: a1 -> b (bound at src/Main.hs:69:11)
    bimap :: (a1 -> b) -> (c -> d) -> SemiDrei a a1 c -> SemiDrei a b d
      (bound at src/Main.hs:69:5)
   |
69 |     bimap f g x = x
   |                   ^

Answer 1

Последний аргумент фактически не остается неизменным: изменяется его тип. ВходSemiDrei a x y и выход SemiDrei a p q, где f :: x -> p а также g :: y -> q.

Это означает, что вам нужно деконструировать значение исходного типа и восстановить значение нового типа, что вы и делаете в исходной реализации.

Но ваша интуиция верна: эти два значения имеют одинаковое представление в памяти. И GHC может вывести этот факт, и когда это произойдет, он автоматически решит Coercible ограничение для вас, что означает, что вы можете использовать coerce функция для преобразования одного в другое:

 bimap _ _ = coerce

Answer 2

Это показывает ту же проблему в более простом случае:

data T a = K

foo :: T a -> T b
foo K = K  -- type checks

bar :: T a -> T b
bar x = x  -- type error

-- bar = id would also be a type error, for the same reason

Проблема здесь в том, что два K в fooзначения скрывают параметры своего типа. Более точное определение было бы

-- pseudo code
foo (K @a) = K @b

Здесь вы можете видеть, что аргумент неявного типа изменяется. GHC автоматически выводит для нас эти аргументы типа, когда мы пишемK в определении foo. Поскольку они неявны, они выглядят так, как будто они такие жеKs, но они не подходят для проверки типов.

Вместо этого, когда мы используем x в определении bar, нет никаких аргументов неявного типа для вывода. У нас есть этоx :: T aи это все. Мы не можем использоватьx и утверждать, что имеет другой тип T b.

Наконец, обратите внимание, что с помощью "безопасного принуждения" мы можем выполнять интуитивно правильный вид -id который становится одним K (в одном типе) в другой K другого типа:

import Data.Coerce

baz :: T a -> T b
baz = coerce

Спорный вопрос, лучше ли это. В простых случаях сопоставление с образцом легче понять, чемcoerce, поскольку последний может выполнять широкий спектр (безопасных) приведений, возможно, оставляя читателя гадать о том, что на самом деле происходит на уровне типа.

Answer 3

Ключ к этому - в сигнатуре типа bimap:

bimap :: Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d

В данном конкретном случае, если мы специализируемся p к SemiDrei a и переименуйте переменные типа, чтобы избежать путаницы с этим a, мы получили:

bimap :: (b -> c) -> (d -> e) -> SemiDrei a b d -> SemiDrei a c e

Итак, когда вы пытаетесь реализовать это:

bimap f g = ...

Функции f а также g совершенно произвольны не только по своей реализации, но и по типам ввода и возврата. f имеет тип b -> c где b а также c может быть абсолютно любым - аналогично для g. Приведенное вами определение должно работать абсолютно для любых типов и функций, которые предоставляет вызывающий - это то, что означает быть (параметрически) полиморфным.

Если мы теперь рассмотрим ваши три определения в этих терминах, мы сможем разгадать очевидную загадку:

Первый:

bimap f g (SemiDrei a) = SemiDrei a

это совершенно нормально, как вы видели. SemiDrei a имеет тип SemiDrei a b c, где только aуказан. Это означает, что он может принимать любой тип, напримерSemiDrei a Int String, или SemiDrei [Bool] (Char, [Double]), или что угодно. SemiDrei aсам по себе полиморфен, он может быть любого совместимого типа. Это означает, что, в частности, он может действовать какSemiDrei a b c и SemiDrei a c e в подписи выше bimap.

Сравните с другими вашими попытками:

bimap f g = id

Проблема здесь в том, что id, Хотя полиморфные, не полиморфный достаточно для этой цели. Его типa -> a (для любого a), который, в частности, может быть специализирован для SemiDrei a b c -> SemiDrei a b c. Но он не может быть специализирован для типаSemiDrei a b d -> SemiDrei a c e по мере необходимости, потому что b, c, d а также eвообще будут совершенно разные типы. Напомним, что вызывающему изbimap может выбирать типы - они могут легко выбирать функции f а также g где b а также c бывают разных типов, например, и тогда нет возможности id может взять SemiDrei a b d к SemiDrei a c e, потому что они разные.

На этом этапе вы можете возразить, что значение SemiDrei aможет быть значением всех таких типов. Это совершенно верно, но это не относится к выводу типов - компилятор заботится только о типах, а не о том, какие значения могут их населять. Следует учитывать, что разные типы имеют совершенно разные, непересекающиеся значения. И скажи,SemiDrei a Int String а также SemiDrei a Bool Charна самом деле разные типы. Опять же, компилятор не знает, чтоIntи т.д. фактически не используются ни одним из значений типа. Именно поэтому такие "фантомные типы" (типы, которые появляются в определении типа, но не в каком-либо из их конструкторов данных) используются на практике - чтобы компилятор мог различать их по типу, даже если время выполнения представление может быть полностью эквивалентным.

Что касается вашей третьей попытки, bimap f g x = x, это точно так же, как и предыдущее - ограничивает bimap f gчтобы его тип вывода был таким же, как и его ввод. (На самом деле это полностью эквивалентноbimap f g = id.)

Таким образом, важным выводом является то, что на этапе проверки типов компилятор заботится только о типах - и два типа с разными именами считаются (и должны считаться) совершенно разными, даже если эквивалентные значения могут быть встроены в обе.