Подтвердить что ты не робот

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

Согласно нескольким источникам, реализация Haskell для компоновки функторов более или менее следующая:

import Data.Functor.Compose

newtype Compose f g a = Compose { getCompose :: f (g a) }

instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose x) = Compose (fmap (fmap f) x)

Мой вопрос: Каков тип x в последнем определении?

Я бы сказал, что это f g a, но даже там я изо всех сил стараюсь "видеть" вычисление fmap (fmap f) x

Может ли кто-нибудь быть таким добрым, чтобы обеспечить четкий и полный рабочий пример этого момента? Как насчет fmapping a Tree of Maybe, обращая внимание на Empty и Node 's?

Спасибо заранее.

4b9b3361

Ответ 1

Тип x - f (g a). Например, x может быть списком деревьев целых чисел: [Tree Int] (который также может быть записан как [] (Tree Int), чтобы он соответствовал f (g x)).

В качестве примера рассмотрим функцию succ :: Int -> Int, которая добавляет ее к целому. Затем функция fmap succ :: Tree Int -> Tree Int будет увеличивать каждое целое число в дереве. Кроме того, fmap (fmap succ) :: [Tree Int] -> [Tree Int] применит предыдущий fmap succ ко всем деревьям в списке, следовательно, он будет увеличивать каждое целое число в списке деревьев.

Если вместо этого у вас есть Tree (Maybe Int), то fmap (fmap succ) будет увеличивать каждое целое число в таком дереве. Значения в дереве формы Nothing не будут затронуты, а значения Just x будут иметь значение x.

Пример: (сеанс GHCi)

> :set -XDeriveFunctor
> data Tree a = Node a (Tree a) (Tree a) | Empty deriving (Show, Functor)
> let x1 = [Node 1 Empty Empty]
> fmap (fmap succ) x1
[Node 2 Empty Empty]
> let x2 = [Node 1 Empty Empty, Node 2 (Node 3 Empty Empty) Empty]
> fmap (fmap succ) x2
[Node 2 Empty Empty,Node 3 (Node 4 Empty Empty) Empty]
> let x3 = Just (Node 1 Empty Empty)
> fmap (fmap succ) x3
Just (Node 2 Empty Empty)

Ответ 2

Каков тип x в последнем определении?

Прежде чем говорить что-нибудь еще по этому поводу, вы можете спросить GHC! GHC 7.8 и выше поддерживает TypedHoles, что означает, что если вы помещаете знак подчеркивания в выражении (не шаблон) и нажимаете на загрузку или компилируете, вы получаете сообщение с ожидаемым типом подчеркивания и типами переменных в локальной области.

newtype Compose f g a = Compose { getCompose :: f (g a) }

instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose x) = _

GHC говорит, что некоторые части пропущены:

Notes.hs:6:26: Found hole ‘_’ with type: Compose f g b …
    -- omitted type variable bindings --
    Relevant bindings include
      x :: f (g a)
        (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:21)
      f :: a -> b
        (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:10)
      fmap :: (a -> b) -> Compose f g a -> Compose f g b
        (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:5)
    In the expression: _
    In an equation for ‘fmap’: fmap f (Compose x) = _
    In the instance declaration for ‘Functor (Compose f g)’

Там вы идете, x :: f (g a). И после некоторой практики TypedHoles может помочь вам в изучении сложного полиморфного кода. Попробуем выяснить наш текущий код, написав правую сторону с нуля.

Мы уже видели, что отверстие имеет тип Compose f g b. Поэтому мы должны иметь a Compose _ в правой части:

instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose x) = Compose _

Новое отверстие имеет тип f (g b). Теперь мы должны посмотреть на контекст:

Relevant bindings include
  x :: f (g a)
    (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:21)
  f :: a -> b
    (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:10)
  fmap :: (a -> b) -> Compose f g a -> Compose f g b
    (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:5)

Цель состоит в том, чтобы получить f (g b) из ингредиентов в контексте. fmap в приведенном выше списке, к сожалению, относится к определяемой функции, что иногда полезно, но не здесь. Нам лучше знать, что f и g - оба функтора, поэтому они могут быть fmap -перечисленными. Поскольку мы имеем x :: f (g a), мы предполагаем, что мы должны fmap что-то над x получить f (g b):

fmap f (Compose x) = Compose (fmap _ x)

Теперь отверстие становится g a -> g b. Но теперь g a -> g b очень легко, так как мы имеем f :: a -> b и g a Functor, поэтому мы также имеем fmap :: (a -> b) -> g a -> g b и, следовательно, fmap f :: g a -> g b.

fmap f (Compose x) = Compose (fmap (fmap f) x)

И все готово.

Чтобы завершить технику:

  • Начните с размещения дыры в том месте, где вы не знаете, как действовать. Здесь мы начали с размещения дыры вместо всей правой стороны, но часто вы будете иметь хорошее представление о большинстве частей реализации, и вам понадобится отверстие в конкретном проблемном подвыражении.

  • Изучая типы, попытайтесь сузить, какие реализации могут привести к цели, а какие не могут. Заполните новое выражение и переместите отверстие. В жаргоне-помощнике это называется "рафинирование".

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

Вышеупомянутая техника иногда называется "тип тетрис". Возможным недостатком является то, что вы можете реализовать сложный код, просто играя "тетрис", не понимая, что вы делаете. И иногда, заходя слишком далеко, вы серьезно застряли в игре, а затем вам нужно начать думать о проблеме. Но в конечном итоге это позволяет вам понимать код, который в противном случае очень трудно понять.

Я лично использую TypedHoles все время и в основном как рефлекс. Я очень полагался на это, так что по случаю, когда мне пришлось вернуться в GHC 7.6, мне стало неудобно (но, к счастью,