Comprensión de una firma de tipo complicado

Question

Necesito ayuda para entender este tipo de firma que es del paquete 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) 

Estoy confundido acerca de varias cosas.

Primero, ¿cuáles son los símbolos +> y ~>? ¿Dónde están documentados y cómo se llaman?

Pero mi confusión se detiene allí. Me doy cuenta de que la cuantificación está describiendo el enhebrado de tipos de Thrist, pero no estoy seguro de si está describiendo una relación válida para el primer argumento, o toda la función, o quién sabe ...

En otros casos donde He visto la cuantificación existencial, la frase termina con un punto, pero aquí termina con ->, ¿es eso significativo?

Answer 1

Primero, ¿cuáles son los símbolos +> y ~>? ¿Dónde están documentados y cómo se llaman?

Son identificadores de infijo, como si los hubiera utilizado como el nombre de una función. Por la misma razón, siendo equivalentes a minúsculas identificadores (a diferencia de los operadores que comienzan con : que son equivalentes a los identificadores alfanuméricos en mayúsculas), en una firma de tipo son simplemente variables de tipo. En otras palabras, es equivalente a esto:

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

Pero mi confusión se detiene allí. Soy consciente de que la cuantificación está describiendo el enhebrado de tipos de la Thrist, pero no estoy seguro de si se describe una relación que mantiene para el primer argumento, o toda la función, o quien sabe ...

explícita los cuantificadores tienen un alcance solo dentro de paréntesis adjuntos, o hasta el final de la expresión. En este caso, describen solo el primer argumento, porque las variables de tipo introducidas están solo en el alcance de ese argumento.

En este caso, solo significa que la función dada como primer argumento debe ser completamente polimórfica en esos tipos. Como ejemplo, una función cuya firma de tipo comienza con (a -> a) -> ... podría tener not como primer argumento, unificando a con Bool. Por el contrario, si la firma de tipo comenzada con (forall a. a -> a) -> ... requeriría una función que funcione para todos los tipos posibles a, la única función de este tipo es id.