Tipos de dados algébricos de Haskell

https://stackoverflow.com/questions/16770

08-06-2019
|

Pergunta

Estou tentando entender completamente todos os conceitos de Haskell.

De que forma os tipos de dados algébricos são semelhantes aos tipos genéricos, por exemplo, em C# e Java?E como eles são diferentes?O que há de tão algébrico neles, afinal?

Estou familiarizado com a álgebra universal e seus anéis e campos, mas tenho apenas uma vaga ideia de como funcionam os tipos de Haskell.

Solução

"Tipos de dados algébricos" em suporte a Haskell polimorfismo paramétrico completo, que é o nome tecnicamente mais correto para genéricos, como um exemplo simples, o tipo de dados lista:

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

É equivalente (tanto quanto possível, e ignorando a avaliação não estrita, etc.) a

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

É claro que o sistema de tipos de Haskell permite mais ...uso interessante de parâmetros de tipo, mas este é apenas um exemplo simples.Com relação ao nome "Tipo Algébrico", honestamente, nunca tive certeza do motivo exato pelo qual eles foram nomeados assim, mas presumi que isso se deve aos fundamentos matemáticos do sistema de tipos.EU acreditar que o motivo se resume à definição teórica de um ADT como o "produto de um conjunto de construtores", porém já se passaram alguns anos desde que escapei da universidade, então não consigo mais me lembrar dos detalhes.

[Editar:Obrigado a Chris Conway por apontar meu erro tolo, ADT são, obviamente, tipos de soma, os construtores que fornecem o produto/tupla de campos]

Outras dicas

Haskell tipos de dados algébricos são assim denominados porque correspondem a um álgebra inicial na teoria das categorias, dando-nos algumas leis, algumas operações e alguns símbolos para manipular.Podemos até usar notação algébrica para descrever estruturas de dados regulares, onde:

+ representa tipos de soma (uniões disjuntas, por ex. Either).
• representa tipos de produtos (por exemplo,estruturas ou tuplas)
X para o tipo singleton (por exemplo data X a = X a)
1 para o tipo de unidade ()
e μ para o ponto menos fixo (por ex.tipos recursivos), geralmente implícitos.

com alguma notação adicional:

X² para X•X

Na verdade, você poderia dizer (seguindo Brent Yorgey) que um tipo de dados Haskell é regular se puder ser expresso em termos de 1, X, +, •, e um ponto mínimo fixo.

Com esta notação, podemos descrever concisamente muitas estruturas de dados regulares:

Unidades: data () = ()

1
Opções: data Maybe a = Nothing | Just a

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

L = 1+X•L
Árvores binárias: data BTree a = Empty | Node a (BTree a) (BTree a)

B = 1 + X•B²

Outras operações são mantidas (retiradas do artigo de Brent Yorgey, listadas nas referências):

Expansão:desdobrar o ponto fixo pode ser útil para pensar em listas. L = 1 + X + X² + X³ + ... (isto é, as listas estão vazias ou têm um elemento, ou dois elementos, ou três, ou ...)
Composição, ◦, dados tipos F e G, a composição F ◦ G é um tipo que constrói “estruturas F feitas de estruturas G” (por exemplo R = X • (L ◦ R) ,onde L é lista, é uma roseira.
Diferenciação, a derivada de um tipo de dados D (dado como D') é o tipo de estruturas D com um único “buraco”, ou seja, um local distinto que não contém nenhum dado.Isso surpreendentemente satisfaz as mesmas regras da diferenciação em cálculo:

1′ = 0

X′ = 1

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

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

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

Referências:

Espécies e Functores e Tipos, Meu Deus!, Brent A.Yorgey, Haskell'10, 30 de setembro de 2010, Baltimore, Maryland, EUA
Palhaços à minha esquerda, curingas à direita (Dissecando Estruturas de Dados), Conor McBride POPL 2008

Em álgebra universal um álgebra consiste em alguns conjuntos de elementos (pense em cada conjunto como o conjunto de valores de um tipo) e algumas operações, que mapeiam os elementos dos elementos.

Por exemplo, suponha que você tenha um tipo de "elementos da lista" e um tipo de "listas".Como operações, você tem a "lista vazia", que é uma função de 0-argumento retornando uma "lista de contras" que leva dois argumentos, um "elemento da lista" e uma lista "e produz uma" lista " ".

Neste ponto, existem muitas álgebras que se encaixam na descrição, como duas coisas indesejáveis podem acontecer:

Pode haver elementos no conjunto de "lista" que não podem ser construídos a partir da "Lista vazia" e da "operação contras", o chamado "lixo".Isso pode ser listas a partir de algum elemento que caiu do céu ou loops sem começo ou listas infinitas.
Os resultados de "contras" aplicados a diferentes argumentos podem ser iguais, por exemplo,Conseguir um elemento para uma lista não vazia pode ser igual à lista vazia.Isso às vezes é chamado de “confusão”.

Uma álgebra que não possui nenhuma dessas propriedades indesejáveis é chamadainicial, e este é o significado pretendido do tipo de dados abstrato.

O nome inicial deriva da propriedade de que existe exatamente um homomorfismo da álgebra inicial para qualquer álgebra.Essencialmente, você pode avaliar o valor de uma lista aplicando as operações na outra álgebra, e o resultado é bem definido.

Fica mais complicado para tipos polimórficos ...

Uma razão simples pela qual são chamados algébricos;existem tipos de soma (disjunção lógica) e produto (conjunção lógica).Um tipo sum é uma união discriminada, por exemplo:

data Bool = False | True

Um tipo de produto é um tipo com vários parâmetros:

data Pair a b = Pair a b

Em O'Caml, "produto" é tornado mais explícito:

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

Os tipos de dados de Haskell são chamados de "algébricos" devido à sua conexão com álgebras iniciais categóricas.Mas nesse caminho reside a loucura.

@olliej:ADTs são, na verdade, tipos de "soma".Tuplas são produtos.

@Timbo:

Você está basicamente certo sobre ser uma espécie de classe Tree abstrata com três classes derivadas (Empty, Leaf e Node), mas você também precisaria impor a garantia de que alguém usando sua classe Tree nunca poderá adicionar novas classes derivadas , já que a estratégia para usar o tipo de dados Tree é escrever código que alterna em tempo de execução com base no tipo de cada elemento na árvore (e adicionar novos tipos derivados quebraria o código existente).Você pode imaginar que isso fica desagradável em C# ou C++, mas em Haskell, ML e OCaml, isso é fundamental para o design e a sintaxe da linguagem, de modo que o estilo de codificação suporta isso de uma maneira muito mais conveniente, por meio de correspondência de padrões.

ADT (tipos de soma) também são como sindicatos marcados ou tipos de variantes em C ou C++.

pergunta antiga, mas ninguém mencionou a nulidade, que é um aspecto importante dos tipos de dados algébricos, talvez o aspecto mais importante.Como cada valor deve ser uma das alternativas, é possível uma correspondência exaustiva de padrões baseada em casos.

Para mim, o conceito de tipos de dados algébricos de Haskell sempre pareceu polimorfismo em linguagens OO como C#.

Veja o exemplo de http://en.wikipedia.org/wiki/Algebraic_data_types:

data Tree = Empty 
          | Leaf Int 
          | Node Tree Tree

Isso pode ser implementado em C# como uma classe base TreeNode, com uma classe derivada Leaf e uma classe derivada TreeNodeWithChildren, e se você quiser até mesmo uma classe derivada EmptyNode.

(OK, eu sei, ninguém jamais faria isso, mas pelo menos você poderia fazer.)

Licenciado em: CC-BY-SA com atribuição

Não afiliado a StackOverflow