operazioni intesa sulle tipologie functor composte

Question

Secondo diverse fonti, l'attuazione Haskell per la composizione di funtori è più o meno il seguente:

import Data.Functor.Compose 

newtype Compose f g a = Compose { getCompose :: f (g a) } 

instance (Functor f, Functor g) => Functor (Compose f g) where 
    fmap f (Compose x) = Compose (fmap (fmap f) x) 

La mia domanda è: qual è il tipo di x nell'ultimo definizione?

direi che è f g a, ma anche lì faccio fatica a 'vedere' il calcolo fmap (fmap f) x

si poteva essere così gentile da fornire un esempio chiaro e completo lavoro di questo punto? Che ne è di fare una copia di Tree di Maybe prestando attenzione sia a Empty che a Node?

Grazie in anticipo.

Answer 1

Il tipo di x è f (g a). Ad esempio, x potrebbe essere un elenco di alberi di numeri interi: [Tree Int] (che può anche essere scritto come [] (Tree Int) in modo che corrisponda più strettamente allo f (g x)).

Ad esempio, considerare la funzione succ :: Int -> Int che aggiunge uno a un numero intero. Quindi, la funzione fmap succ :: Tree Int -> Tree Int incrementerà ogni numero intero nell'albero. Inoltre, fmap (fmap succ) :: [Tree Int] -> [Tree Int] applicherà il precedente fmap succ a tutti gli alberi di un elenco, quindi incrementerà ogni numero intero di alberi.

Se invece si dispone di Tree (Maybe Int), allora fmap (fmap succ) incrementerà ogni numero intero in tale albero. I valori nell'albero del modulo Nothing non saranno interessati, mentre i valori Just x avranno x incrementato.

Esempio: (sessione GHCi)

> :set -XDeriveFunctor 
> data Tree a = Node a (Tree a) (Tree a) | Empty deriving (Show, Functor) 
> let x1 = [Node 1 Empty Empty] 
> fmap (fmap succ) x1 
[Node 2 Empty Empty] 
> let x2 = [Node 1 Empty Empty, Node 2 (Node 3 Empty Empty) Empty] 
> fmap (fmap succ) x2 
[Node 2 Empty Empty,Node 3 (Node 4 Empty Empty) Empty] 
> let x3 = Just (Node 1 Empty Empty) 
> fmap (fmap succ) x3 
Just (Node 2 Empty Empty) 

Answer 2

qual è il tipo di x nell'ultimo definizione?

Prima di dire altro sull'argomento: puoi chiedere a GHC! GHC 7.8 e versioni successive supporta TypedHoles, il che significa che se si inserisce un carattere di sottolineatura in un'espressione (non un pattern) e si preme il comando load o compile, si ottiene un messaggio con il tipo previsto del carattere di sottolineatura e i tipi delle variabili nell'ambito locale.

newtype Compose f g a = Compose { getCompose :: f (g a) } 

instance (Functor f, Functor g) => Functor (Compose f g) where 
    fmap f (Compose x) = _ 

GHC dice ora, con alcune parti omesse:

Notes.hs:6:26: Found hole ‘_’ with type: Compose f g b … 
    -- omitted type variable bindings -- 
    Relevant bindings include 
     x :: f (g a) 
     (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:21) 
     f :: a -> b 
     (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:10) 
     fmap :: (a -> b) -> Compose f g a -> Compose f g b 
     (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:5) 
    In the expression: _ 
    In an equation for ‘fmap’: fmap f (Compose x) = _ 
    In the instance declaration for ‘Functor (Compose f g)’ 

Ci si va, x :: f (g a). E dopo un po 'di pratica, TypedHoles può aiutarti enormemente a capire il codice polimorfico complesso. Proviamo a capire il nostro codice attuale scrivendo il lato destro da zero.

Abbiamo già visto che il foro aveva il tipo Compose f g b. Pertanto dobbiamo avere una Compose _ sul lato destro:

instance (Functor f, Functor g) => Functor (Compose f g) where 
    fmap f (Compose x) = Compose _ 

Il nuovo buco è di tipo f (g b).Ora dovremmo guardiamo al contesto:

Relevant bindings include 
    x :: f (g a) 
    (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:21) 
    f :: a -> b 
    (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:10) 
    fmap :: (a -> b) -> Compose f g a -> Compose f g b 
    (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:5) 

L'obiettivo è quello di ottenere un f (g b) con gli ingredienti nel contesto. Il numero fmap nella lista sopra purtroppo si riferisce alla funzione in fase di definizione, che a volte è utile, ma non qui. Stiamo meglio sapendo che f e g sono entrambi i funtori, quindi possono essere sostituiti da fmap. Dal momento che abbiamo x :: f (g a), abbiamo immaginare che dovremmo fmap qualcosa sopra x per ottenere un f (g b):

fmap f (Compose x) = Compose (fmap _ x) 

Ora il buco diventa g a -> g b. Ma g a -> g b è molto semplice ora, dato che abbiamo f :: a -> b e g è un Functor, quindi abbiamo anche fmap :: (a -> b) -> g a -> g b e quindi fmap f :: g a -> g b.

fmap f (Compose x) = Compose (fmap (fmap f) x) 

E abbiamo finito.

per concludere la tecnica:

1. Inizia con mettere un buco nel luogo in cui non si sa come procedere. Qui abbiamo iniziato col mettere il buco al posto dell'intero lato destro, ma spesso avrete una buona idea della maggior parte delle parti di un'implementazione e avrete bisogno del buco in una subexpression problematica specifica.

2. Osservando i tipi, provare a restringere quali implementazioni potrebbero portare all'obiettivo e quali no. Inserisci una nuova espressione e riposiziona il buco. In gergo dell'assistente tecnico questo è chiamato "raffinamento".

3. Ripeti il ​​passaggio 2 finché non ottieni l'obiettivo, nel qual caso hai finito, oppure l'obiettivo attuale sembra impossibile, nel qual caso fai il backtrack fino all'ultima scelta non ovvia che hai fatto e prova un raffinamento alternativo.

La tecnica di cui sopra viene talvolta chiamata scherzosamente "tipo tetris". Un possibile inconveniente è che è possibile implementare codice complesso semplicemente suonando il "tetris", senza effettivamente capire cosa si sta facendo. E a volte, dopo essere andato troppo lontano, si rimane seriamente bloccati nel gioco, e quindi bisogna iniziare a pensare veramente al problema. Ma alla fine ti consente di capire codice che altrimenti sarebbe molto difficile da capire.

Io personalmente uso TypedHolestutto il tempo e fondamentalmente come una reflex. Sono arrivato a contare così tanto su di esso in modo che in un'occasione in cui dovevo tornare a GHC 7.6 mi sentivo piuttosto a disagio (ma fortunatamente si è can emulate holes anche lì).