Esiste un utilizzo generale del funtore (non limitato all'endofuntore) nella programmazione? [chiuso]

Question

Esiste un utilizzo generale del funtore (non limitato all'endofuntore) nella programmazione?

Capisco il motivo per cui l'endofunctor impiegato è per rendere la struttura semplice come monoide o monade.

Capisco anche, in definitiva, che tutto il valore è stabilito in una categoria di un linguaggio di programmazione (come Hask), ma quello di cui sto parlando qui è endofunctor tra la stessa categoria di stringhe, numeri, booleani o funzioni.

Domande correlate:

Tutti i funtori Haskell sono endofuntori?

Differenze tra funtori ed endofuntori

Answer 1

Primo, sì .

Ad esempio, sappiamo tutti che un monoide può essere definito come una categoria a oggetto singolo con

• frecce per essere elementi
• il singolo oggetto non ha significato
• composizione da operatore ( (<>)in Haskell)
• freccia id per essere l'identità ( memptyin Haskell).

E un omomorfismo tra due monoidi diventa un funtore tra due categorie in questo senso.

Ora, diciamo, digita Ae Bsono entrambi monoidi; Un funtore tra di loro è solo una funzione omomorfa f :: A -> Bche mappa ciascuno Aa B, preservando la composizione.

Ma, aspetta, f :: A -> Bnon è nemmeno un Functor(nota che qui uso il carattere a spaziatura fissa)!

No, non è un Functorin Haskell, ma ancora è un funtore in senso matematico.

Quindi, per sottolineare, lo ribadisco: i funtori "non endo" SONO usati nella programmazione, e probabilmente anche più spesso degli endofuntori.

Il punto qui è che la teoria delle categorie è una teoria altamente astratta : fornisce nozioni per astrarre oggetti concreti. Possiamo definire queste nozioni per significare cose diverse in contesti differenti.

E Hask (o Set , o sottocategorie di Set ) è solo una di queste infinite definizioni, il che rende

• frecce per essere funzioni
• oggetti per essere tipi (o, insiemi)
• composizione per essere composizione funzionale (.)
• freccia id per essere la idfunzione.

Confronta questa definizione di "universo categoriale" con la definizione di "monoide categoriale" sopra - congratulazioni, hai conosciuto due diverse interpretazioni delle categorie ora!

Per concludere, ricorda che la stessa teoria delle categorie è solo alcune astrazioni . Le astrazioni stesse non hanno alcun significato e non servono affatto. Li colleghiamo a cose reali e solo in questo modo possono darci comodità. Comprendere concetti astratti attraverso esempi concreti, ma MAI semplificare questi concetti stessi a qualcosa di concreto (come, mai semplificare i funtori semplicemente ai funtori tra "universi categoriali" (ad esempio Hask , Set , ecc.)!).

PS Se chiedi "C'è un funtore che invia Hask a un'altra categoria in Haskell?" allora la risposta può essere sì o no . Ad esempio, è possibile definire una categoria Hask * Hask per contenere qualsiasi prodotto cartesiano di due tipi e un funtore data Diag a = Diag a a, fmap f x = Diag (f x) (f x)che invia ogni tipo Aal proprio quadrato A * A. Tuttavia, Hask * Hask è ancora una sottocategoria di Hask , quindi possiamo dire che anche questo è un endofunctor.

Answer 2

La risposta breve: sì, ci sono categorie "più piccole" in Haskell e puoi definire funtori (non solo endofuntori) tra di loro. Se sono utili è un'altra domanda.

Questo è qualcosa su cui mi chiedevo da anni. La presente domanda mi ha spinto a provarci. Attualmente sto attraversando la teoria delle categorie per programmatori di Bartosz Milewski per la terza volta. Non sono sicuro di aver capito bene quanto segue, quindi apprezzerei il feedback.

Hask

Se lo capisco correttamente, Hask è essenzialmente la categoria di tipi (~ categoria di insiemi ) con il fondo (⊥) inserito per rappresentare il calcolo non terminante. Ecco un tentativo di illustrarlo:

Ogni oggetto in Hask è un tipo come Int, Bool, String, o il vostro propri tipi personalizzati come Reservation, Orderecc Un tipo può essere visto come un insieme ; eg Boolè l'insieme che contiene Truee False, Stringè l'insieme di tutte le stringhe, ecc. Chiaramente, molti di questi insiemi (come String) sono infiniti.

Inoltre, c'è anche lo speciale oggetto inferiore.

Puoi mappare i tipi su altri tipi, ma non puoi mappare su qualcosa al di fuori di Hask perché Hask comprende tutti i tipi e le espressioni:

Qui ho illustrato le mappature da Hask a Hask duplicando Hask , ma in realtà le due categorie sono solo due immagini identiche.

Un funtore è una mappatura che non mappa solo oggetti, ma anche morfismi tra oggetti. Molto è già stato detto su questo, quindi l'unico punto che farò qui è che, poiché i funtori tra Hask e Hask non lasciano la categoria, sono funtori all'interno di Hask , e quindi endofuntori . Questa è la Functorclasse tipo in Haskell.

Categoria di unità

La domanda, quindi, è: ci sono categorie "più piccole" all'interno di Hask ?

Per quanto ne so: sì, infinitamente tanti.

Una delle categorie più semplici esistenti è una categoria con un unico oggetto e nessun altro morfismo oltre al morfismo dell'identità:

In Haskell, questa potrebbe essere un'immagine del tipo unit ( ()). Sebbene faccia() parte di Hask , puoi anche vederlo come una categoria a sé stante. Chiamiamolo Unità .

Categorie libere

La categoria di unità di cui sopra è solo un esempio di una categoria libera . Una categoria libera è una categoria costruita da un grafico diretto. Ecco un altro grafico:

Questo ha due vertici e due bordi. Possiamo costruire una categoria da questo grafo interpretando i vertici come oggetti e gli spigoli come morfismi. Dobbiamo anche aggiungere morfismi di identità per ogni oggetto, così come la composizione dei morfismi.

In programmazione, un insieme con due oggetti equivale a un tipo con solo due abitanti. Puoi dare a questi valori vari nomi, ma un tale tipo è sempre isomorfo a Bool.

Functor

Possiamo definire una mappatura tra le due categorie precedenti?

Sì, possiamo farlo incorporando Unità nella categoria "più grande". Lo facciamo scegliendo arbitrariamente uno degli oggetti:

Esiste un altro funtore che sceglie l'altro oggetto.

Questa è chiaramente una mappatura tra categorie, quindi non è un endofunctor. È un funtore appropriato, però?

Per essere un funtore, la mappatura non deve solo mappare gli oggetti agli oggetti, ma anche i morfismi ai morfismi. Questo è anche il caso qui, perché Unit ha solo il morfismo dell'identità. Quindi, mappiamo anche il morfismo dell'identità al morfismo dell'identità sull'oggetto target che abbiamo scelto. Le uniche composizioni possibili in Unità è id ∘ id, id ∘ id ∘ ide così via. Tutti questi vengono mappati su id ∘ id, id ∘ id ∘ idecc. Sull'oggetto di destinazione.

Mi diletto con la teoria delle categorie solo da alcuni anni, ma penso che questo sia un funtore appropriato.

La classe del tipo di categoria Haskell

Haskell definisce una classe di tipo chiamata Category . Non si adatta perfettamente alla categoria Unità di cui sopra , o all'esempio di categoria libera sopra, perché presume che Categorysia un tipo di tipo superiore (cioè che coinvolga tipi ) in Hask . Tuttavia, vediamo se riusciamo a calzare le unità e la categoria libera di cui sopra Category, oltre a farne un funtore.

Unità comeCategory

Le istanze di Categorydevono essere di tipo superiore (cioè cat a b), quindi non possiamo trasformarci ()in Categoryun'istanza. Possiamo, tuttavia, definire un tipo di tipo superiore isomorfo ad esso:

data U a b = U deriving (Eq, Show)

Come il funtore Const , questo tipo definisce variabili di tipo che poi ignora. Proprio come (), il Utipo ha un solo valore, chiamato anche U. (Esercizio: mostra che Ue ()sono isomorfi.)

Possiamo fare Uun Categoryesempio:

instance Category U where
  id = U
  U . U = U

È una categoria corretta, però? Obbedisce alle leggi?

Possiamo usare il ragionamento equazionale per dimostrare che lo fa:

Identità giusta

  U . id
= { definition of (.) }
  U

Identità sinistra

  id . U
= { definition of (.) }
  U

Associatività

  U . (U . U)
= { definition of (.) }
  U . U
= { redundant brackets }
  (U . U)
= { definition of (.) }
  (U . U) . U

Mi sembra vada bene.

L'esempio di categoria libera come Category

Che ne dici dell'esempio sopra di una categoria libera? Come il Utipo precedente , questa piccola categoria non può essere parametricamente polimorfa, ma ancora una volta possiamo definire un tipo fantasma:

data Bendo a b = Bendo { runB :: Bool -> Bool }

other :: Bendo a b
other = Bendo not

Ho chiamato il tipo Bendoper endomorfismo booleano , perché è quello che risulta essere. I bordi tra i due oggetti ( Truee False) corrispondono alla selezione dell'altro oggetto, che è equivalente alla notfunzione incorporata.

Per modellare la categoria in questione, gli unici morfismi consentiti sono othere id, quindi altre funzioni Bool -> Bool(come \_ -> True) dovrebbero essere disabilitate. Pertanto, un modulo che definisce Bendonon dovrebbe esportare il costruttore di dati.

Possiamo fare Bendoun Categoryesempio?

instance Category Bendo where
  id = Bendo id
  (Bendo f) . (Bendo g) = Bendo (f . g)

In effetti, questo è possibile. Non ho intenzione di dimostrare che questa è una categoria, perché in realtà è solo l' ->istanza di categoria specializzata (->) Bool Bool.

Functor

Definiamo ora un funtore tra Ue Bendo. A tale scopo, possiamo utilizzare la definizione più generale di Functordata in Control.Categorical.Functor . Per far funzionare tutto questo, poi, ho dovuto nascondere le solite definizioni date in Prelude:

import Control.Category
import Control.Categorical.Functor
import Prelude hiding (id, (.), Functor(..))

Avremo anche bisogno di supportare MultiParamTypeClasses:

{-#LANGUAGE MultiParamTypeClasses #-}

Per implementare quella Functorclasse di tipo più generale , abbiamo bisogno di un tipo di tipo superiore. Di nuovo, produciamo un altro tipo fantasma per lo scopo:

data Embed a = Embed deriving (Eq, Show)

Questo è sufficiente per definire l'istanza:

instance Functor Embed U Bendo where
  fmap U = Bendo id

Questo corrisponde Ual morhismo dell'identità in Bendo.

È un po 'scomodo da usare, ma è possibile:

> (runB $ (fmap U :: Bendo (Embed a) (Embed b))) False False > (runB $ (fmap U :: Bendo (Embed a) (Embed b))) True
True

Haskell non riesce a capire che tipo fmap Usarà, quindi devi dirlo. Una volta detto che il risultato dovrebbe avere il tipo Bendo (Embed a) (Embed b), viene fmapmappato Ual morfismo dell'identità, che puoi verificare applicando runBsu Trueo False.

Conclusione

Esistono funtori (non solo endofuntori) nella programmazione? Si lo fanno.

Sono utili? Mi sembra che se strizzi un po 'gli occhi, quei funtori sono solo un sottoinsieme delle funzioni "normali". Una versione semplificata del funtore sopra è solo:

uToBendo :: () -> Bool -> Bool
uToBendo () = id

Questa è solo una normale funzione.

Devo pensare di più se esiste un'applicazione più utile se vista in questo modo.