Tipi di dati algebrici di Haskell

https://stackoverflow.com/questions/16770

08-06-2019
|

Domanda

Sto cercando di comprendere appieno tutti i concetti di Haskell.

In che modo i tipi di dati algebrici sono simili ai tipi generici, ad esempio in C# e Java?E in cosa differiscono?Comunque, cosa c'è di così algebrico in loro?

Ho familiarità con l'algebra universale e i suoi anelli e campi, ma ho solo una vaga idea di come funzionano i tipi di Haskell.

Soluzione

"Tipi di dati algebrici" nel supporto Haskell polimorfismo parametrico completo, che è il nome tecnicamente più corretto per i generici, come semplice esempio il tipo di dati list:

 data List a = Cons a (List a) | Nil

È equivalente (per quanto possibile, ignorando la valutazione non rigorosa, ecc.) a

 class List<a> {
     class Cons : List<a> {
         a head;
         List<a> tail;
     }
     class Nil : List<a> {}
 }

Ovviamente il sistema di tipi di Haskell consente di più...uso interessante dei parametri di tipo ma questo è solo un semplice esempio.Per quanto riguarda il nome "Tipo algebrico", onestamente non sono mai stato del tutto sicuro del motivo esatto per cui sono stati chiamati così, ma ho ipotizzato che sia dovuto alle basi matematiche del sistema di tipi.IO credere che il motivo si riduce alla definizione teorica di un ADT come "prodotto di un insieme di costruttori", tuttavia sono passati un paio d'anni da quando sono scappato dall'università quindi non riesco più a ricordare le specifiche.

[Modificare:Grazie a Chris Conway per aver sottolineato il mio stupido errore, gli ADT sono ovviamente tipi di somma, i costruttori che forniscono il prodotto/tupla dei campi]

Altri suggerimenti

Quello di Haskell tipi di dati algebrici sono chiamati così poiché corrispondono ad an algebra iniziale nella teoria delle categorie, dandoci alcune leggi, alcune operazioni e alcuni simboli da manipolare.Possiamo anche usare la notazione algebrica per descrivere strutture di dati regolari, dove:

+ rappresenta i tipi di somma (unioni disgiunte, ad es. Either).
• rappresenta i tipi di prodotto (ad es.strutture o tuple)
X per il tipo singleton (es. data X a = X a)
1 per il tipo di unità ()
E μ per il punto minimo fisso (es.tipi ricorsivi), solitamente impliciti.

con qualche notazione aggiuntiva:

X² per X•X

In effetti, potresti dire (seguendo Brent Yorgey) che un tipo di dati Haskell è regolare se può essere espresso in termini di 1, X, +, •, e un punto meno fisso.

Con questa notazione possiamo descrivere in modo conciso molte strutture dati regolari:

Unità: data () = ()

1
Opzioni: data Maybe a = Nothing | Just a

1 + X
Elenchi: data [a] = [] | a : [a]

L = 1+X•L
Alberi binari: data BTree a = Empty | Node a (BTree a) (BTree a)

B = 1 + X•B²

Altre operazioni valgono (tratte dall'articolo di Brent Yorgey, elencate nei riferimenti):

Espansione:spiegare il punto fisso può essere utile per pensare agli elenchi. L = 1 + X + X² + X³ + ... (ovvero, le liste o sono vuote, oppure hanno un elemento, o due elementi, o tre, o ...)
Composizione, ◦, dati tipi F E G, la composizione F ◦ G è un tipo che costruisce "strutture F realizzate con strutture G" (ad es. R = X • (L ◦ R) ,Dove L è una lista, è un albero di rose.
La differenziazione, la derivata di un tipo di dati D (indicato come D') è il tipo di strutture D con un singolo "buco", cioè una posizione distinta che non contiene dati.Ciò sorprendentemente soddisfa le stesse regole della differenziazione nel calcolo infinitesimale:

1′ = 0

X′ = 1

(F + G)′ = F' + G′

(F • G)′ = F • G′ + F′ • G

(F ◦ G)′ = (F′ ◦ G) • G′

Riferimenti:

Specie, funtori e tipi, Oh mio Dio!, Brent A.Yorgey, Haskell'10, 30 settembre 2010, Baltimora, Maryland, Stati Uniti
Clown alla mia sinistra, jolly a destra (Dissezione di strutture di dati), Conor McBride POPL 2008

In algebra universale UN algebra è costituito da alcuni insiemi di elementi (pensa a ciascun insieme come l'insieme di valori di un tipo) e alcune operazioni, che mappano gli elementi su elementi.

Ad esempio, supponiamo di avere un tipo di "elementi elenchi" e un tipo di "elenchi".Come operazioni hai "Elenco vuoto", che è una funzione di 0-Argument che restituisce un "elenco" e una funzione "contro" che prende due argomenti, un "elemento elenco" e un "elenco" e produce un elenco " ".

A questo punto ci sono molte algebre che si adattano alla descrizione, poiché possono accadere due cose indesiderabili:

Potrebbero esserci elementi nel set "Elenco" che non possono essere costruiti dall'elenco "vuoto" e dall'operazione "Contro", cosiddetto "spazzatura".Questi potrebbero essere elenchi a partire da alcuni elementi che cadevano dal cielo, o loop senza inizio o liste infinite.
I risultati dei "contro" applicati a argomenti diversi potrebbero essere uguali, ad esempioI controlli di un elemento a un elenco non vuoto potrebbero essere uguali all'elenco vuoto.Questo a volte viene chiamato "confusione".

Viene chiamata un'algebra che non ha nessuna di queste proprietà indesiderabiliiniziale, e questo è il significato previsto del tipo di dati astratto.

Il nome iniziale deriva dalla proprietà che esiste esattamente un omomorfismo dall'algebra iniziale a ogni algebra.In sostanza è possibile valutare il valore di un elenco applicando le operazioni nell'altra algebra e il risultato è ben definito.

Diventa più complicato per i tipi polimorfici...

Un semplice motivo per cui sono chiamati algebrici;esistono sia tipi di somma (disgiunzione logica) che di prodotto (congiunzione logica).Un tipo di somma è un'unione discriminata, ad esempio:

data Bool = False | True

Un tipo di prodotto è un tipo con più parametri:

data Pair a b = Pair a b

In O'Caml il "prodotto" è reso più esplicito:

type 'a 'b pair = Pair of 'a * 'b

I tipi di dati di Haskell sono chiamati "algebrici" a causa della loro connessione a algebre iniziali categoriche.Ma in questo modo sta la follia.

@olliej:Gli ADT sono in realtà tipi "somma".Le tuple sono prodotti.

@Timbo:

Fondamentalmente hai ragione nel dire che è una specie di classe Tree astratta con tre classi derivate (Empty, Leaf e Node), ma dovresti anche garantire che qualcuno che usa la tua classe Tree non possa mai aggiungere nuove classi derivate , poiché la strategia per utilizzare il tipo Tree datat è scrivere codice che cambia in fase di esecuzione in base al tipo di ciascun elemento nell'albero (e l'aggiunta di nuovi tipi derivati interromperebbe il codice esistente).Puoi immaginare che questo diventi brutto in C# o C++, ma in Haskell, ML e OCaml, questo è fondamentale per la progettazione e la sintassi del linguaggio, quindi lo stile di codifica lo supporta in un modo molto più conveniente, tramite la corrispondenza dei modelli.

Anche gli ADT (tipi di somma) sono simili sindacati contrassegnati O tipi di varianti in C o C++.

vecchia domanda, ma nessuno ha menzionato l'annullamento, che è un aspetto importante dei tipi di dati algebrici, forse l'aspetto più importante.Poiché ciascun valore rappresenta per lo più una delle alternative, è possibile una corrispondenza esaustiva del modello basata sui casi.

Per me, il concetto dei tipi di dati algebrici di Haskell è sempre sembrato un polimorfismo nei linguaggi OO come C#.

Guarda l'esempio da http://en.wikipedia.org/wiki/Algebraic_data_types:

data Tree = Empty 
          | Leaf Int 
          | Node Tree Tree

Questo potrebbe essere implementato in C# come classe base TreeNode, con una classe Leaf derivata e una classe derivata TreeNodeWithChildren e, se si desidera, anche una classe derivata VuotoNode.

(OK, lo so, nessuno lo farebbe mai, ma almeno potresti farlo tu.)

Autorizzato sotto: CC-BY-SA insieme a attribuzione

Non affiliato a StackOverflow