Scrivendo la monade identità in termini di libera

Question

In "Tipi di dati alla carte" Swierstra scrive che dato Free (che egli chiama Term) e Zero è possibile implementare la monade Identità:

data Term f a = Pure a 
       | Impure (f (Term f a)) 
data Zero a 

Term Zero è ora il Identità monade Capisco perché questo è. Il problema è che non riesco mai a usare Term Zero come Monade a causa del fastidioso Functor f => vincolo:

instance Functor f => Monad (Term f) where 
    return x = Pure x 
    (Pure x) >>= f = f x 
    (Impure f) >>= t = Impure (fmap (>>=f) t) 

Come faccio Zero un funtore?

instance Functor Zero where 
    fmap f z = ??? 

Sembra che ci sia un trucco qui: Dal momento che non ci sono Zero costruttori, Impure non può essere utilizzato, e così il Impure caso di >>= non viene mai chiamato. Questo significa fmap non è mai chiamato, quindi non c'è un senso in cui questo è ok:

instance Functor Zero where 
    fmap f z = undefined 

Il problema è, questo si sente come barare. Cosa mi manca? Zero è in realtà un Functional? O forse Zero non è un Functor, e questo è un difetto di come esprimiamo Free in Haskell?

Answer 1

Se si accende DeriveFunctor, è possibile scrivere

data Zero a deriving Functor 

ma si potrebbe considerare che barare. Se volete scrivere voi stessi, è possibile attivare EmptyCase, invece, quindi scrivere il

instance Functor Zero where 
    fmap f z = case z of 

Answer 2

Un modo funky-cercando di andare su questo è quello di utilizzare Data.Void invece di un data dichiarazione di vuoto, in questo modo:

import Data.Void 

-- `Zero a` is isomorphic to `Void` 
newtype Zero a = Zero Void 

instance Functor Zero where 
    -- You can promise anything if the precondition is that 
    -- somebody's gotta give you an `x :: Void`. 
    fmap f (Zero x) = absurd x 

Vedi this question per alcuni davvero grande spiegazioni di ciò che è utile per Void. Ma l'idea chiave è che la funzione absurd :: Void -> a ti consente di passare dall'impossibilità x :: Void a qualsiasi tipo che ti piace.

Answer 3

Un modo intelligente per definire Zero a è il seguente.

newtype Zero a = Zero (Zero a) 

In altre parole, si codifica il tipo di sciocco, dichiarazione un po 'non-ovvio che v'è in realtà un modo per ottenere un valore di Zero a: è necessario avere già uno!

Con questa definizione, absurd :: Zero a -> b è definibile in modo "naturale"

absurd :: Zero a -> b 
absurd (Zero z) = absurd z 

In un certo senso queste definizioni sono tutti legali perché sottolineano esattamente come non sono possibili istanziare. Nessun valore di Zero a può essere costruito a meno che qualcun altro non "imbrogli" per primo.

instance Functor Zero where 
    fmap f = absurd 

Answer 4

Un altro giro su Luis Casillas di answer è quello di costruire il vostro tipo del tutto a magazzino parti:

type Id = Free (Const Void) 

L'istanza Functor per Const x funzionerà come si desidera (la sua fmap non fa nulla, che va bene), e avrete solo bisogno di prendersi cura durante il disimballaggio:

runId (Pure x) = x 
runId (Free (Const ab)) = absurd ab 

Tutte queste cose, di Ovviamente, sono solo "moralmente" equivalenti a Identity, perché tutti introducono valori extra. In particolare, siamo in grado di distinguere tra

bottom 
Pure bottom 
Free bottom