runST e la funzione di composizione

Question

Perché questo TYPECHECK:

runST $ return $ True 

Mentre il seguente non lo fa:

runST . return $ True 

GHCI lamenta:

Couldn't match expected type `forall s. ST s c0' 
      with actual type `m0 a0' 
Expected type: a0 -> forall s. ST s c0 
    Actual type: a0 -> m0 a0 
In the second argument of `(.)', namely `return' 
In the expression: runST . return 

Answer 1

La risposta breve è che l'inferenza di tipo non funziona sempre con tipi di rango superiore. In questo caso, non è in grado di dedurre il tipo di (.), ma digitare controlla se aggiungiamo un tipo esplicito di annotazione:

> :m + Control.Monad.ST 
> :set -XRankNTypes 
> :t (((.) :: ((forall s0. ST s0 a) -> a) -> (a -> forall s1. ST s1 a) -> a -> a) runST return) $ True 
(((.) :: ((forall s0. ST s0 a) -> a) -> (a -> forall s1. ST s1 a) -> a -> a) runST return) $ True :: Bool 

Lo stesso problema si verifica anche con il vostro primo esempio, se sostituiamo ($) con la nostra versione:

> let app f x = f x 
> :t runST `app` (return `app` True) 
<interactive>:1:14: 
    Couldn't match expected type `forall s. ST s t0' 
       with actual type `m0 t10' 
    Expected type: t10 -> forall s. ST s t0 
     Actual type: t10 -> m0 t10 
    In the first argument of `app', namely `return' 
    In the second argument of `app', namely `(return `app` True)' 

nuovo, questo può essere risolto aggiungendo annotazioni di tipo:

> :t (app :: ((forall s0. ST s0 a) -> a) -> (forall s1. ST s1 a) -> a) runST (return `app` True) 
(app :: ((forall s0. ST s0 a) -> a) -> (forall s1. ST s1 a) -> a) runST (return `app` True) :: Bool 

Cosa sta succedendo qui è che c'è una Regola di digitazione speciale in GHC 7 che si applica solo all'operatore standard ($). Simon Peyton-Jones spiega questo comportamento in a reply on the GHC users mailing list:

Questo è un esempio motivante per inferenza di tipo in grado di affrontare tipi impredicativa. Considerare il tipo di ($):

($) :: forall p q. (p -> q) -> p -> q 

Nell'esempio abbiamo bisogno di istanziare p con (forall s. ST s a), e questo è ciò che significa polimorfismo impredicativa: istanziare una variabile di tipo con un tipo polimorfico .

Purtroppo, non conosco alcun sistema di ragionevole complessità che possa risolvere il problema con questo . Ci sono un sacco di sistemi complicati, e ho stato un coautore su documenti su almeno due, ma sono tutti troppo Jolly Complicato per vivere in GHC. Abbiamo implementato i tipi di boxe , ma l'ho estratto quando ho implementato il nuovo typechecker. Nessuno l'ha capito.

Tuttavia, le persone spesso scrivono

runST $ do ... 

che nel GHC 7 ho implementato uno speciale regola di battitura, solo per usi infissa di ($). Basti pensare allo (f $ x) come un nuovo modulo sintattico , con l'ovvia regola di digitazione e via.

Il secondo esempio non riesce perché non esiste alcuna regola per (.).

Answer 2

Il modello runST $ do { ... } è così comune, e il fatto che normalmente non verrebbe controllato è così fastidioso, che GHC includeva alcuni ST specifici hack di controllo dei tipi per farlo funzionare. Questi hack probabilmente stanno sparando qui per la versione ($), ma non per la versione (.).

Answer 3

I messaggi confondono un po 'il punto (o così mi sento). Permettetemi di riscrivere il codice:

runST (return True) -- return True is ST s Bool 
(runST . return) True -- cannot work 

Un altro modo per mettere questo è che il monomorfa m0 a0 (il risultato di ritorno, se sarebbe ottenere un a0) non può essere unificato con (forall s.ST s a).