runST i funkcja skład

Question

Dlaczego ten typecheck:

runST $ return $ True 

Choć po nie:

runST . return $ True 

GHCI narzeka:

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

Krótka odpowiedź brzmi, że wnioskowanie typu nie zawsze działa z typami wyższej rangi. W tym przypadku, nie jest w stanie wywnioskować typ (.), ale to typ kontroli jeśli dodamy wyraźny typ adnotacji:

> :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 

Ten sam problem występuje również z pierwszego przykładu, jeśli wymienimy ($) z własnym wersja:

> 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)' 

Znowu ten można rozwiązać poprzez dodanie typu adnotacji:

> :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 

Co się tu dzieje jest, że istnieje specjalna reguła pisania w GHC 7, która dotyczy tylko operatora standardowego ($). Simon Peyton-Jones wyjaśnia to zachowanie w a reply on the GHC users mailing list:

To jest motywujące przykładem typu wnioskowania, które mogą poradzić sobie z impredicative typów. Rozważyć rodzaj ($):

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

W przykładzie musimy instancję p z (forall s. ST s a), a to co polimorfizm impredicative oznacza: utworzenie wystąpienia zmiennej typu z typu polimorficznych.

Niestety, nie znam żadnego systemu o rozsądnej złożoności, który może typecheck [ten] bez pomocy. Istnieje wiele skomplikowanych systemów, a ja mam , który był współautorem artykułów na co najmniej dwóch, ale wszystkie są Too Jolly Skomplikowane do życia w GHC. Mieliśmy implementację typów boxy , ale wyjąłem ją podczas implementacji nowego sprawdzania poprawności. Nikt tego nie rozumiał.

Jednak ludzie tak często pisać

runST $ do ... 

że w GHC 7 I wdrożone specjalną regułę pisania, tylko do zastosowań infiksowych z ($). Pomyśl o (f $ x) jako nowej formie syntaktycznej, z oczywistą zasadą pisania i odejdź.

Twój drugi przykład kończy się niepowodzeniem, ponieważ nie ma takiej reguły dla (.).

Answer 2

runST $ do { ... } wzór jest tak powszechne, i fakt, że normalnie nie sprawdzałby typu jest tak denerwujący, że GHC zawierało około ST -specyficzne sprawdzanie typu, aby działało. Te hacki prawdopodobnie wystrzelają tutaj dla wersji ($), ale nie dla wersji (.).

Answer 3

Wiadomości są nieco mylące punkt (a przynajmniej tak się czuję). Pozwól mi przepisać kod:

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

Innym sposobem, aby umieścić to, że jednokształtny m0 a0 (wynik zwrotu, jeśli byłoby uzyskać A0) nie może być ujednolicone z (forall s.ST s a).