Zrozumienie skomplikowanego typu Podpis

Question

Potrzebuję pomocy w zrozumieniu podpisu tego typu, który pochodzi z pakietu 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) 

Jestem zdezorientowany z kilku rzeczy.

Po pierwsze jakie są symbole +> i ~>? Gdzie są udokumentowane i jak się nazywają?

Ale moje zamieszanie się tam kończy. Zdaję sobie sprawę, że kwantyfikacja opisuje gwintowanie typów Thristla, ale nie jestem pewien, czy opisuje relację, która zachodzi dla pierwszego argumentu, czy całej funkcji, czy kto wie ...

W innych przypadkach, w których Widziałem egzystencjalną kwantyfikację, fraza kończy się okresem, ale tu kończy się ->, czy to jest znaczące?

Answer 1

Po pierwsze jakie są symbole +> i ~>? Gdzie są udokumentowane i jak się nazywają?

Są to identyfikatory infiksów, tak jak w przypadku użycia ich jako nazwy funkcji. Z tego samego powodu, będące odpowiednikami małych identyfikatorów (w przeciwieństwie do operatorów rozpoczynających się od :, które są odpowiednikami dużych alfanumerycznych identyfikatorów), w sygnaturze typu są po prostu zmiennymi typu. Innymi słowy, jest to równoznaczne z tym:

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

Ale mój zamieszanie tam nie zatrzyma. Zdaję sobie sprawę, że jest ilościowe opisujące gwintowanie typów Thrist, ale nie jestem pewien, czy opisuje związek, który odnosi się do pierwszego argumentu, albo całą funkcję, albo kto wie ...

Explicit Kwantyfikatory są ograniczone tylko do otaczających nawiasów lub do końca wyrażenia. W tym przypadku opisują tylko pierwszy argument, ponieważ wprowadzone zmienne typu są tylko w zakresie tego argumentu.

W tym przypadku oznacza to tylko, że funkcja podana jako pierwszy argument musi być w pełni polimorficzna w tych typach. Na przykład funkcja, której typ podpisu zaczyna się od (a -> a) -> ..., może być podana jako not jako pierwszy argument, jednocząc a z Bool. W przeciwieństwie do tego, jeśli podpis typu rozpoczynający się od (forall a. a -> a) -> ... wymagałby funkcji działającej dla wszystkich możliwych typów, to jedyną taką funkcją jest id.