Понимание сложной подписи типа

Question

Мне нужна помощь в понимании подписи этого типа, которая входит в пакет Thrist.

import Prelude hiding ((.), id)
import Control.Category
import Data.Monoid
import Control.Arrow
import Control.Monad

foldlThirst :: (forall j k . (a +> j) -> (j ~> k) -> (a +> k))  
               -> (a +> b) 
               -> Thrist (~>) b c  
               -> (a +> c)

Я запутался в нескольких вещах.

Во-первых, что такое символы +> и ~>?Где они задокументированы и как они называются?

Но мое замешательство на этом заканчивается.Я понимаю, что количественное определение описывает многопоточность типов Thrist, но я не уверен, описывает ли отношение, которое имеет место для первого аргумента, или всей функции, или кто знает ...

ВВ других случаях, когда я видел экзистенциальное количественное определение, фраза заканчивается точкой, но здесь она заканчивается -> это значимо?

Answer 1

Во-первых, что это за символы +> и ~>? Где они документированы и как они называются?

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

(forall j k . (f a j) -> (g j k) -> (f a k)) 
  -> etc . . .

Но мое замешательство на этом и заканчивается. Я понимаю, что количественное определение описывает потоки типов Thrist, но я не уверен, описывает ли отношение, которое имеет место для первого аргумента, или всей функции, или кто знает ...

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

В данном случае это просто означает, что функция, указанная в качестве первого аргумента, должна быть полностью полиморфной в этих типах. Например, функции, чья сигнатура типа начинается с (a -> a) -> ..., можно было бы задать not в качестве первого аргумента, объединяя a с Bool. В отличие от этого, если сигнатура типа начинается с (forall a. a -> a) -> ..., для этого потребуется функция, которая работает для всех возможных типов a, единственной такой функцией является id.