L'utente 'singpolyma' asked on reddit se ci fosse qualche struttura generale sottostante:Posso modellare un elenco di successi con errori di cortocircuito tramite la composizione di funtori applicativi?
data FailList a e = Done | Next a (FailList a e) | Fail e
una monade libera è stato suggerito, ma mi chiedevo se questo potrebbe essere modellato più in generale tramite funtori applicative. In Abstracting with Applicatives, Bazerman ci mostra che la somma di due funtori applicativi è anche un funtore applicativo, con distorsione a sinistra/a destra, a condizione che abbiamo una trasformazione naturale nella direzione del bias. Sembra che sia ciò di cui abbiamo bisogno! Così, ho iniziato la mia proposta, ma poi ho incontrato rapidamente problemi. Qualcuno può vedere soluzioni a questi problemi ?:
In primo luogo, iniziamo con la definizione della somma di due funtori. Ho iniziato qui perché vogliamo modellare i tipi di somma: successi o successi e un fallimento.
data Sum f g a = InL (f a) | InR (g a)
E i due funtori che vogliamo lavorare con sono:
data Success a = Success [a]
data Failure e a = Failure e [a]
Success
è semplice - è essenzialmente Const [a]
. Tuttavia, Failure e
non ne sono così sicuro. Non è un functor applicativo, perché pure
non ha alcuna definizione. E ', tuttavia, un'istanza di Apply:
instance Functor Success where
fmap f (Success a) = Success a
instance Functor (Failure e) where
fmap f (Failure e a) = Failure e a
instance Apply (Failure e) where
(Failure e a) <.> (Failure _ b) = Failure e a
instance Apply Success where
(Success a) <.> (Success b) = Success (a <> b)
instance Applicative Success where
pure = const (Success [])
a <*> b = a <.> b
Avanti, possiamo definire la somma di questi funtori, con una trasformazione naturale da destra a sinistra (quindi una polarizzazione sinistra):
instance (Apply f, Apply g, Applicative g, Natural g f) => Applicative (Sum f g) where
pure x = InR $ pure x
(InL f) <*> (InL x) = InL (f <*> x)
(InR g) <*> (InR y) = InR (g <*> y)
(InL f) <*> (InR x) = InL (f <.> eta x)
(InR g) <*> (InL x) = InL (eta g <.> x)
E l'unica cosa che dobbiamo fare ora è definire la nostra trasformazione naturale, ed è qui che tutto viene a crollare.
instance Natural Success (Failure e) where
eta (Success a) = Failure ???? a
L'incapacità di creare un Failure
sembra essere il problema. Inoltre, anche l'hacky e l'uso di ⊥ non sono un'opzione, perché questo sarà valutato, nel caso in cui si disponga di InR (Success ...) <*> InL (Failure ...)
.
Mi sento come se mi mancasse qualcosa, ma non ho idea di cosa sia.
Questo può essere fatto?
La condizione di naturalita 'forall (f :: a -> b). eta. fmap f == fmap f. eta' suggerisce fortemente che la componente di errore deve essere costante. Questo mi fa venir voglia di scrivere un 'Default e => Applicativo (Failure e) '. –
Inoltre, le istanze 'Apply' /' Applicative' sono strane. Ho sistemato le teste in modo che controllassero gentilmente, ma in genere non controllano anche il tipo! 'Success a' non è realmente isomorfico a' Constant [a] ', anche se, perlomeno, ha bisogno di più indici di tipi! –
@tel - 'Predefinito' sembra possibile, non riesco a vedere quale sarebbe un" messaggio di errore predefinito "sensato. Inoltre, le tue modifiche sono state rifiutate da altri editor SO, sebbene siano valide. Li applicherò io stesso. – ocharles