linguaggio basato sulla teoria delle categorie

Question

linguaggio basato sulla teoria delle categorie

#1 da (3 voti)

1

Può sembrare ingenuo, ma esiste un linguaggio di programmazione o una sua ricerca basata interamente sulla teoria delle categorie?

Intendo questo invece di incorporare concetti CT come funzionalità aggiuntiva (come per Haskell o scala).

Sarebbe troppo astratto o troppo complesso come approccio o ci sono motivi noti che lo rendono impossibile o poco pratico?

Ho solo una comprensione relativa della teoria in relazione alla programmazione, quindi per favore mi dia qualche spiegazione se la domanda non ha proprio senso

Modifica

Ciò che intendo è definire una lingua in cui le categorie sono concetti di prima classe, invece di dire tipi.

es. haskell è definito in termini di tipi e funzioni su quelli. Ha senso progettare un linguaggio in cui le entità fondamentali sono categorie e frecce ?

Da lì, per esempio, definirai le operazioni algebriche sui numeri come "intances" individuali della corretta categoria algebrica (ring, monoid, group ...) invece di partire dalle operazioni standard a intero / float e definendo il corrispondente categoriale typeclass.

Ha senso?

programming-languages theory

posta pagoda_5b 06.11.2013 - 01:42

fonte

1 risposta

Leggi altre domande sui tag programming-languages theory

Esiste un modello di progettazione che descrive la separazione di un modulo da un modello Come gestire la modifica di un file di grandi dimensioni per un utente non tecnico

score 3 · Accepted Answer

La teoria delle categorie fornisce uno strumento. Non sarebbe del tutto logico decidere "Oh hey, renderò il mio linguaggio di programmazione una categoria" tanto quanto si costruisce un kernel, e si accorge che forma una categoria, e da lì inizia ad applicare le astrazioni libere / teoremi che vengono con esso.

Un perfetto esempio di questo è semplicemente il calcolo lambda tipizzato. Questo forma una categoria cartesiana chiusa in cui i tipi sono oggetti e le funzioni sono frecce. Ora, a causa di ciò, possiamo iniziare ad applicare astrazioni comuni, come endofunctor, adjoint, sottocategorie e simili. In realtà, questo è esattamente quello che è successo in Haskell dove il sistema di tipi è radicato in STLC.

Quindi direi che cosa succede con Haskell è un grande esempio di applicazione della teoria delle categorie per costruire astrazioni. Molte librerie in Haskell, mtl, pipe, lens, void, comonads sono tutte astrazioni molto molto utili che provengono dal notare che qualcosa è una categoria e di conseguenza generalizzare e applicare i concetti.

La stessa cosa accade sul lato della ricerca delle cose. Le persone hanno questo concetto che notano avere un parallelo nella teoria delle categorie e estrapolare da lì. Ad esempio, molti problemi nella teoria dei domini sono notevolmente semplificati dai limiti nella teoria delle categorie e le implicite coercizioni sono ben modellate dalla teoria delle categorie.

Quindi direi che stai pensando a questo torto, non pensare alla teoria delle categorie come la cosa da cui hai costruito, è un po 'troppo astratto per questo, è più che usi parallelismi tra il tuo problema e la teoria delle categorie per teoremi gratuiti e astrazioni nel tuo problema.