Che cos'è la definizione del Functional applicativo dalla teoria delle categorie POV?

Question

sono stato in grado di mappare la definizione di Functor dalla teoria di categoria alla definizione di Haskell nel modo seguente: dato che gli oggetti di Hask sono tipi, il funtore F

• Mappe ogni tipo a di Hask al nuovo tipo F a da, più o meno dicendo, anteponendo "F" ad esso.
• mappe ogni morfismo a -> b di Hask al nuovo morfismo F a -> F b utilizzando fmap :: (a -> b) -> (f a -> f b).

Fin qui, tutto bene. Ora arrivo allo Applicative e non riesco a trovare alcuna menzione di un simile concetto nei libri di testo. Osservando ciò che aggiunge a Functor, ap :: f (a -> b) -> f a -> f b, ho cercato di venire con la mia definizione.

Innanzitutto, ho notato che dal (->) è anche un tipo, i morfismi di Hask sono anch'essi oggetti di questo tipo. Alla luce di ciò, ho suggerito che il funtore applicativo è un funtore che può anche mappare "freccia" - oggetti della categoria sorgente in morfismi di quello di destinazione.

È una giusta intuizione? Puoi fornire una definizione più formale e rigorosa?

Answer 1

La chiave per comprendere funtori applicative è capire quale struttura preservano.

I funtori regolari conservano la struttura categoriale di base: mappano gli oggetti e i morfismi tra le categorie e conservano le leggi della categoria (associatività e identità).

Ma una categoria può avere più struttura. Ad esempio, può consentire la definizione di mappature simili ai morfismi, ma assumere più argomenti. Tali mappature sono definite da curry: ad esempio, una funzione di due argomenti è definita come una funzione di un argomento che restituisce un'altra funzione. Questo è possibile se è possibile definire un oggetto che rappresenta un tipo di funzione. In generale, questo oggetto è chiamato esponenziale (in Haskell, è solo il tipo b->c). Possiamo quindi avere morfismi da un oggetto a un esponenziale e chiamarlo morfismo a due argomenti.

La definizione tradizionale di un funtore applicativo in Haskell si basa sull'idea di funzioni di mapping di più argomenti. Ma esiste una definizione equivalente che divide la funzione a più argomenti lungo un confine diverso. È possibile visualizzare una funzione come una mappatura di un prodotto (una coppia, in Haskell) in un altro tipo (in questo caso, c).

a -> (b -> c) ~ (a, b) -> c 

che ci permette di guardare al funtori applicative come funtori che preservano il prodotto. Ma un prodotto è solo un esempio di ciò che viene chiamato una struttura monoidale.

In generale, una categoria monoidale è una categoria equipaggiata con un prodotto tensoriale e un oggetto unitario. In Haskell, questo potrebbe essere, ad esempio, il prodotto cartesiano (una coppia) e il tipo di unità (). Si noti, tuttavia, che le leggi monoidali (associatività e leggi di unità) sono valide solo fino a un isomorfismo. Ad esempio:

Un funtore applicativo può quindi essere definito come un funtore che conserva la struttura monoidale. In particolare, dovrebbe preservare l'unità e il prodotto. Non dovrebbe importare se facciamo la "moltiplicazione" prima o dopo l'applicazione del funtore. I risultati dovrebbero essere isomorfi.

Tuttavia, non abbiamo davvero bisogno di un funtore monoidale in piena regola. Tutto ciò di cui abbiamo bisogno sono due morfismi (al contrario degli isomorfismi): uno per la moltiplicazione e uno per l'unità. Tale funtore che preserva a metà la struttura monoidale è chiamato un lassista monoidale. Da qui la definizione alternativa:

class Functor f => Monoidal f where 
    unit :: f() 
    (**) :: f a -> f b -> f (a, b) 

È facile dimostrare che Monoidal è equivalente a Applicative. Per esempio, possiamo ottenere pure da unit e viceversa:

pure x = fmap (const x) unit 
unit = pure() 

Le leggi applicative seguono semplicemente dalla preservazione delle leggi monoid (leggi associativita e Unit).

Nella categoria teoria, la conservazione della struttura monoidale è relativo a forza tensoriale, quindi un funtore applicativo è anche conosciuto come un forte lassa functor monoidale. Tuttavia, in Hask, ogni functor ha una resistenza canonica rispetto al prodotto, quindi questa proprietà non aggiunge nulla alla definizione.

Ora, se si ha familiarità con la definizione di monade come monoide nella categoria di endofuntor, si potrebbe essere interessati a sapere che gli applicativi sono, allo stesso modo, monoidi nella categoria di endofunatori in cui il prodotto tensoriale è il Convoluzione del giorno. Ma è molto più difficile da spiegare.

Answer 2

Hai ragione, Applicative si traduce meno direttamente di Functor o Monad. Ma in sostanza, è la classe di monoidal functors:

class Functor f => Monoidal f where 
    pureUnit :: f() 
    fzip :: f a -> f b -> f (a,b) 

Da che è possibile definire – entro Hask –

pure x = fmap (const x) pureUnit 

e

fs <*> xs = fmap (uncurry ($)) $ fzip fs xs