Nano Hash - криптовалюты, майнинг, программирование

Как получить тип композиции в Haskell

Я новичок в Хаскеле. Я пытаюсь понять, как работает композиция типов.

(.) :: (b -> c) -> (a -> b) -> a -> c

fmap :: Functor f => (x -> y) -> f x -> f y
fmap . fmap :: (Functor f1, Functor f2) => (x -> y) -> f1 (f2 x) -> f1 (f2 y)

Как я понял, приведенная выше информация о типе приведена ниже.


1. (x -> y) -> f1 x -> f1 y  -- First fmap
      -> (x' -> y') -> f2 x' -> f2 y'  -- Second fmap
2. Compare the (1) with (.) type signature then we get
     In (b -> c)
        b = (x -> y)
        c = f1 x -> f1 y
     In (a -> b)
        a = (x' -> y')
        b = f2 x' -> f2 y'
3. Now the result is a -> c but before that b in (b -> c) should be b in (a -> b)
     (x -> y) === f2 x' -> f2 y'
     That means x = f2 x' & y = f2 y'
4. Result is a -> c
     (x' -> y') -> f1 x -> f1 y
     Substituting (3) results here
     (x' -> y') -> f1 (f2 x') -> f1 (f2 y')
     This is Alpha equivalent to  (x -> y) -> f1 (f2 x) -> f1 (f2 y)

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


 f = undefined :: (x -> y -> w -> z -> a) -> g x -> g y
 -- Type of f . f in prelude
 f . f :: (x -> (w1 -> z1 -> a1) -> w2 -> z2 -> a2) -> g (y -> x) -> g y

Мой подход к вышеизложенному

1. (x -> y -> w -> z -> a) -> g x -> g y
     -> (x' -> y' -> w' -> z' -> a') -> g' x' -> g' y'
2. Comparing with (.) then 
     In (b -> c)
        b = (x -> y -> w -> z -> a)
        c = g x -> g y
     In (a -> b)
        a = (x' -> y' -> w' -> z' -> a')
        b = g' x' -> g' y'
3. Comparing b from (b -> c) & (a -> b)
     (x -> y -> w -> z -> a) === g' x' -> g' y'
     That means x = g' x'  &  y -> w -> z -> a = g' y'
4. Result is a -> c
     (x' -> y' -> w' -> z' -> a') -> g x -> g y
     Now there is no direct y I can substitute in g y

Мой подход к просмотру композиции меня не устраивает.


  • Я думаю, вы хотели сказать тип композиции, а не композицию типов. 04.11.2019
  • Не совсем связано с вопросом, но вот рекомендуемое чтение: adit .io/posts/2013-07-22-lenses-in-pictures.html 04.11.2019

Ответы:


1

Вывод типа — это чисто механический процесс.

(.)  ::              (b          -> c             ) -> (a          -> b             ) -> 
                                                       (a                             -> c)
fmap₂ :: Functor f => (t3 -> t4) -> (f t3 -> f t4)
fmap₁ :: Functor g =>                                  ((t1 -> t2) -> (g t1 -> g t2))
-------------------------------------------------------------------------------------------
                                                   a ~ (t1 -> t2)  b ~ (g t1 -> g t2)
                 b ~ (t3 -> t4)  c ~ (f t3 -> f t4)                b ~ (t3   -> t4  )
-------------------------------------------------------------------------------------------
fmap₂ . fmap₁ :: (Functor f, Functor g) 
              =>  a          ->  c
           ~      (t1 -> t2) ->  (f t3     -> f t4    )
           ~      (t1 -> t2) ->  (f (g t1) -> f (g t2))

Гораздо приятнее с кузеном (.), (>>>) fmap₁ fmap₂ = fmap₂ . fmap₁:

(>>>)  ::            (a           -> b                               ) -> 
                     (               b              -> c             ) -> 
                     (a                             -> c             )
fmap₁ :: Functor g =>  (t1 -> t2) -> (g t1 -> g t2)
fmap₂ :: Functor f =>                (t3   -> t4  ) -> (f t3 -> f t4) 
------------------------------------------------------------------------------
                  a ~ (t1 -> t2)   b ~ (g t1 -> g t2)
                                   b ~ (t3   -> t4  )  c ~ (f t3 -> f t4)
------------------------------------------------------------------------------
fmap₁ >>> fmap₂ :: (Functor f, Functor g) 
              =>    a             ->                   c
           ~          (t1 -> t2)  ->                   (f t3     -> f t4    )
           ~          (t1 -> t2)  ->                   (f (g t1) -> f (g t2))

К вашей конкретной проблеме:

f = undefined :: (x -> y -> w -> z -> a) -> g x -> g y

f₂ . f₁ = f₁ >>> f₂ :: 
 (x -> y -> w -> z -> a) -> ((->) (g x) (g       y               ))
                            ((->) x2    ((->) y2 (w2 -> z2 -> a2))) -> (g2 x2 -> g2 y2)
 ---------------------------------------------------------------------------------------
                       x2 ~ g x     g ~ ((->) y2)    y ~ (w2 -> z2 -> a2)
 ---------------------------------------------------------------------------------------
 (x -> y                -> w -> z -> a)                    ->  ( g2 x2        -> g2 y2)  ~
 (x -> y                -> w -> z -> a)                    ->  ( g2 (g     x) -> g2 y2)  ~
 (x -> (w2 -> z2 -> a2) -> w -> z -> a)                    ->  ( g2 (y2 -> x) -> g2 y2)

это то, что вы получили от GHCi, вплоть до переименования переменных.

04.11.2019
  • Не могли бы вы получить составной тип для этого, пожалуйста. f = undefined :: (x -> y -> w -> z -> a) -> g x -> g y. Я немного смущен этим примером. 04.11.2019
  • Спасибо, я попробую такой же вывод для еще нескольких типов, и я буду чувствовать себя комфортно, и я одобрю ответ. 04.11.2019
  • главное не паниковать, т.е. работать медленно и осторожно; и тщательно переименовывайте переменные типа для каждой новой ссылки на один и тот же объект. 04.11.2019
  • Новые материалы

    Кластеризация: более глубокий взгляд
    Кластеризация — это метод обучения без учителя, в котором мы пытаемся найти группы в наборе данных на основе некоторых известных или неизвестных свойств, которые могут существовать. Независимо от..

    Как написать эффективное резюме
    Предложения по дизайну и макету, чтобы представить себя профессионально Вам не позвонили на собеседование после того, как вы несколько раз подали заявку на работу своей мечты? У вас может..

    Частный метод Python: улучшение инкапсуляции и безопасности
    Введение Python — универсальный и мощный язык программирования, известный своей простотой и удобством использования. Одной из ключевых особенностей, отличающих Python от других языков, является..

    Как я автоматизирую тестирование с помощью Jest
    Шутка для победы, когда дело касается автоматизации тестирования Одной очень важной частью разработки программного обеспечения является автоматизация тестирования, поскольку она создает..

    Работа с векторными символическими архитектурами, часть 4 (искусственный интеллект)
    Hyperseed: неконтролируемое обучение с векторными символическими архитектурами (arXiv) Автор: Евгений Осипов , Сачин Кахавала , Диланта Хапутантри , Тимал Кемпития , Дасвин Де Сильва ,..

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

    Обеспечение масштабируемости LLM: облачный анализ с помощью AWS Fargate и Copilot
    В динамичной области искусственного интеллекта все большее распространение получают модели больших языков (LLM). Они жизненно важны для различных приложений, таких как интеллектуальные..