Errore di tipo strano in Let-expression di Haskell: qual è il problema?

Question

Mi sono imbattuto in un frustrante qualcosa di in Haskell oggi.

Ecco cosa è successo:

1. ho scritto una funzione in ghci e lo diede una firma tipo
2. ghci lamentavano il tipo
3. ho rimosso la firma di tipo
4. ghci accettate la funzione
5. Ho controllato il tipo dedotto
6. il tipo dedotto era esattamente lo stesso del tipo che ho provato a dargli
7. ero molto angosciato
8. ho scoperto che avrei potuto riprodurre il problema in qualsiasi let-espressione
9. stridore di denti; ha deciso di consultarsi con gli esperti di SO

---

tentativo di definire la funzione con una firma tipo:

Prelude Control.Monad> let myFilterM f m = do {x <- m; guard (f x); return x} :: (MonadPlus m) => (b -> Bool) -> m b -> m b 

<interactive>:1:20: 
    Inferred type is less polymorphic than expected 
     Quantified type variable `b' is mentioned in the environment: 
     m :: (b -> Bool) -> m b -> m b (bound at <interactive>:1:16) 
     f :: (m b -> m b) -> Bool (bound at <interactive>:1:14) 
     Quantified type variable `m' is mentioned in the environment: 
     m :: (b -> Bool) -> m b -> m b (bound at <interactive>:1:16) 
     f :: (m b -> m b) -> Bool (bound at <interactive>:1:14) 
    In the expression: 
      do { x <- m; 
       guard (f x); 
       return x } :: 
      (MonadPlus m) => (b -> Bool) -> m b -> m b 
    In the definition of `myFilterM': 
     myFilterM f m 
        = do { x <- m; 
          guard (f x); 
          return x } :: 
         (MonadPlus m) => (b -> Bool) -> m b -> m b 

Definita la funzione senza firma tipo, controllato il tipo derivato:

Prelude Control.Monad> let myFilterM f m = do {x <- m; guard (f x); return x} 
Prelude Control.Monad> :t myFilterM 
myFilterM :: (MonadPlus m) => (b -> Bool) -> m b -> m b 

utilizzata la funzione per la gran bene - ha funzionato correttamente:

Prelude Control.Monad> myFilterM (>3) (Just 4) 
Just 4 
Prelude Control.Monad> myFilterM (>3) (Just 3) 
Nothing 

---

La mia ipotesi migliore da quello che sta succedendo:
annotazioni di tipo in qualche modo non funzionano bene con Let-espressioni , quando c'è un blocco.

per i punti bonus:
c'è una funzione nella distribuzione standard Haskell che fa questo? Sono stato sorpreso che lo filterM faccia qualcosa di molto diverso.

Answer 1

Il problema è la precedenza dell'operatore di tipo (::). Stai cercando di descrivere il tipo di myFilterM ma quello che si sta effettivamente facendo è questo:

ghci> let myFilterM f m = (\ 
     do {x <- m; guard (f x); return x} \ 
     :: \ 
     (MonadPlus m) => (b -> Bool) -> m b -> m b)\ 
    ) 

(backslash inseriti per facilitarne la lettura solo, non legittima la sintassi ghci)

Non si vede il problema?Ottengo lo stesso problema per qualcosa di semplice come

ghci> let f x = x + 1 :: (Int -> Int) 
<interactive>:1:15: 
    No instance for (Num (Int -> Int)) 
     arising from the literal `1' 
    Possible fix: add an instance declaration for (Num (Int -> Int)) 
    In the second argument of `(+)', namely `1' 
    In the expression: x + 1 :: Int -> Int 
    In an equation for `f': f x = x + 1 :: Int -> Int 

La soluzione è quella di attaccare la firma di tipo all'elemento corretto:

ghci> let f :: Int -> Int ; f x = x + 1 
ghci> let myFilterM :: (MonadPlus m) => (b -> Bool) -> m b -> m b; myFilterM f m = do {x <- m; guard (f x); return x} 

E per i punti bonus, si vuole mfilter (hoogle is your friend).

Answer 2

Non so che tipo di compilatore si utilizza, ma sulla mia piattaforma (GHC 7.0.3) ottengo un tipo semplice non corrispondente:

$ ghci 
GHCi, version 7.0.3: http://www.haskell.org/ghc/ :? for help 
Loading package ghc-prim ... linking ... done. 
Loading package integer-gmp ... linking ... done. 
Loading package base ... linking ... done. 
Loading package ffi-1.0 ... linking ... done. 
Prelude> :m +Control.Monad 
Prelude Control.Monad> let myFilterM f m = do {x <- m; guard (f x); return x} :: (MonadPlus m) => (b -> Bool) -> m b -> m b 

<interactive>:1:30: 
    Could not deduce (t1 ~ ((b1 -> Bool) -> m1 b1 -> m1 b1)) 
    from the context (MonadPlus m) 
     bound by the inferred type of 
       myFilterM :: MonadPlus m => t -> t1 -> (b -> Bool) -> m b -> m b 
     at <interactive>:1:5-100 
    or from (MonadPlus m1) 
     bound by an expression type signature: 
       MonadPlus m1 => (b1 -> Bool) -> m1 b1 -> m1 b1 
     at <interactive>:1:21-100 
     `t1' is a rigid type variable bound by 
      the inferred type of 
      myFilterM :: MonadPlus m => t -> t1 -> (b -> Bool) -> m b -> m b 
      at <interactive>:1:5 
    In a stmt of a 'do' expression: x <- m 
    In the expression: 
     do { x <- m; 
      guard (f x); 
      return x } :: 
      MonadPlus m => (b -> Bool) -> m b -> m b 
    In an equation for `myFilterM': 
     myFilterM f m 
      = do { x <- m; 
       guard (f x); 
       return x } :: 
       MonadPlus m => (b -> Bool) -> m b -> m b 

<interactive>:1:40: 
    Could not deduce (t ~ ((m1 b1 -> m1 b1) -> Bool)) 
    from the context (MonadPlus m) 
     bound by the inferred type of 
       myFilterM :: MonadPlus m => t -> t1 -> (b -> Bool) -> m b -> m b 
     at <interactive>:1:5-100 
    or from (MonadPlus m1) 
     bound by an expression type signature: 
       MonadPlus m1 => (b1 -> Bool) -> m1 b1 -> m1 b1 
     at <interactive>:1:21-100 
     `t' is a rigid type variable bound by 
      the inferred type of 
      myFilterM :: MonadPlus m => t -> t1 -> (b -> Bool) -> m b -> m b 
      at <interactive>:1:5 
    The function `f' is applied to one argument, 
    but its type `t' has none 
    In the first argument of `guard', namely `(f x)' 
    In a stmt of a 'do' expression: guard (f x) 
Prelude Control.Monad> 

Credo che il problema sta nel fatto, che il :: non raggiunge l'argomento. Questa piccola variazione (notare la dichiarazione del tipo separato)

let myFilterM f m = do {x <- m; guard (f x); return x}; myFilterM :: (MonadPlus m) => (b -> Bool) -> m b -> m b 

funziona senza problemi. Può essere correlato al nuovo type-checker in GHC 7.

Answer 3

Questo è probabilmente solo un problema di sintassi di annotazione del tipo e precondizione di binding. Se scrivi il tuo esempio come,

let myFilterM :: (MonadPlus m) => (b -> Bool) -> m b -> m b; myFilterM f m = do {x <- m; guard (f x); return x} 

allora GHCi ti darà un cinque e ti manderà sulla tua strada.