2013-10-04 14 views
10

Mi chiedevo come scrivere f x = zip x (tail x) in punto libero. Quindi ho usato il programma pointfree e il risultato è stato f = ap zip tail. ap è una funzione di Control.MonadCome funziona l'espressione `ap zip tail`

Non capisco come funzioni la definizione point free. Spero di riuscire a capirlo se riesco a comprenderlo dal punto di vista dei tipi.

import Control.Monad (ap) 
let f = ap zip tail 
let g = ap zip 
:info ap zip tail f g 
ap :: Monad m => m (a -> b) -> m a -> m b 
    -- Defined in `Control.Monad' 
zip :: [a] -> [b] -> [(a, b)] -- Defined in `GHC.List' 
tail :: [a] -> [a]  -- Defined in `GHC.List' 
f :: [b] -> [(b, b)] -- Defined at <interactive>:3:5 
g :: ([a] -> [b]) -> [a] -> [(a, b)] 
    -- Defined at <interactive>:4:5 

Osservando l'espressione ap zip tail penserei che zip è il primo parametro di ap e la coda è il secondo parametro di ap.

Monad m => m (a -> b) -> m a -> m b 
      \--------/ \---/ 
       zip  tail 

Ma ciò non è possibile, poiché le forme di zip e tail sono completamente diverso da quello che richiede la funzione ap. Anche tenendo conto che la lista è una sorta di monade.

+0

L'unica cosa che posso inventare è che il 'a' nel tipo di ap diventa il' [a] -> [b] 'del tipo di zip. Se è così, allora quali sono le regole di unificazione (se è la parola giusta) che governano questo in generale? – user7610

+1

ghci dice che il tipo è 'ap zip tail :: Monad ((->) [b]) => [b] -> [(b, b)]' ... senza troppe indagini, direi che 'Monad ((->) [b])' è ciò che vuoi leggere. I * think * http://learnyouahaskell.com/for-a-few-monads-more#reader potrebbe aiutarti a capire cosa sta succedendo qui. –

+0

Per inciso, 'zip <*> tail' è equivalente e più bella cercando – jozefg

risposta

11

Quindi la firma del tipo di ap è Monad m => m (a -> b) -> m a -> m b. Gli hai dato zip e tail come argomenti, quindi diamo un'occhiata al loro tipo di firme.

Partendo tail :: [a] -> [a] ~ (->) [a] [a] (qui ~ è l'operatore di uguaglianza per i tipi), se confrontiamo questo tipo contro il tipo del secondo argomento per ap,

(->) [x] [x] ~ m a 
((->) [x]) [x] ~ m a 

otteniamo a ~ [x] e m ~ ((->) [x]) ~ ((->) a). Già possiamo vedere che la monade in cui ci troviamo è (->) [x], non []. Se sostituiamo quello che possiamo nella firma tipo di ap otteniamo:

(((->) [x]) ([x] -> b)) -> (((->) [x]) [x]) -> (((->) [x]) b) 

Poiché questo non è molto leggibile, può più normalmente essere scritto come

([x] -> ([x] -> b)) -> ([x] -> [x]) -> ([x] -> b) 
~ ([x] -> [x] -> b) -> ([x] -> [x]) -> ([x] -> b) 

Il tipo di zip è [x] -> [y] -> [(x, y)]. Possiamo già vedere che questo si allinea con il primo argomento di cui ap

[x]   ~ [x] 
[y]   ~ [x] 
[(x, y)] ~ b 

Qui ho elencato i tipi verticalmente in modo che si può facilmente vedere quali tipi allineano. Così, ovviamente x ~ x, y ~ x, e [(x, y)] ~ [(x, x)] ~ b, in modo che possiamo finire sostituendo b ~ [(x, x)] nella firma di tipo ap s' e ottenere

([x] -> [x] -> [(x, x)]) -> ([x] -> [x]) -> ([x] -> [(x, x)]) 
-- zip      tail  (ap zip tail) 
--           ap zip tail u = zip u (tail u) 

Spero che cancella le cose per voi.

EDIT: Come danvaripointed out nei commenti, la monade (->) a è talvolta chiamato monade lettore.

+5

potrebbe valere la pena di menzionare che (->) è il Reader-monade – dnaq

5

Ci sono due aspetti per comprendere questo:

  1. Il tipo di magia
  2. Il flusso informativo dell'attuazione

primo luogo, questo mi ha aiutato a capire il tipo di magia:

1) zip   : [a] → ([a] → [(a,a)]) 
2) tail   : [a] → [a] 
3) zip <*> tail : [a] → [(a,a)] 

4) <*> : Applicative f ⇒ f (p → q) → f p → f q 

In questo caso, ad <*>,

5) f x = y → x 

noti che in 5, f è un costruttore di tipo. L'applicazione di f a x produce un tipo. Inoltre, qui = è sovraccaricato per significare equivalenza di tipi.

y è attualmente un luogo titolare, in questo caso, è [a], che significa

6) f x = [a] -> x 

Usando 6, possiamo riscrivere 1,2 e 3 come segue:

7) zip   : f ([a] → [(a,a)]) 
8) tail   : f [a] 
9) zip <*> tail : f ([a] → [(a,a)]) → f [a] → f [(a,a)] 

Quindi, guardando a 4, stiamo sostituendo come segue:

10) p = [a] 
11) q = [(a,a)] 
12) f x = [a] → x 

(Ripetizione di 6 qui 12)

In secondo luogo, il flusso di informazioni , ovvero la funzionalità effettiva. Questo è più facile, è chiaro dalla definizione di <*> per la Applicative instance of y →, che viene riscritta qui con nomi diversi identificatore e con infisso stile:

13) g <*> h $ xs = g xs (h xs) 

Sostituendo come segue:

14) g = zip 
15) h = tail 

Gives:

zip <*> tail $ xs  (Using 14 and 15) 
    == 
zip xs (tail xs)   (Using 13)