Material para aprender Gadt

Question

Comecei a ler sobre Gadt em Haskell Wiki, mas não me senti muito confortável em entender. Você recomenda um capítulo de livro específico ou uma postagem de blog explicando Gadt para um iniciante Haskell?

Answer 1

Apfelmus fez Tutorial em vídeo para Gadts o que pode ser útil.

Answer 2

Eu gosto do exemplo no Manual do GHC. É simples e ilustra alguns pontos -chave:

• Gadts permitem que você use o sistema de tipo Haskell para modelar o sistema de tipo de um idioma que você está implementando (a "linguagem do objeto")

• Isso permite que a verificação estática de Haskell afirme que o seu "compilador passa" ou o que não é o tipo preservando. As funções que assumem termos de linguagem de objetos podem assumir que esses termos estão bem tocados. Funções que retornam termos em língua de objetos são necessários para produzir termos bem tocados.

• A correspondência de padrões de um construtor GADT causa refinamento do tipo. eval tem tipo Term a -> a no geral, mas o lado direito para eval (Lit i) tem tipo Int, porque o construtor esquerdo tinha tipo Term Int.

• O sistema Haskell não se importa com quais tipos você fornece aos seus construtores GADT. Poderíamos facilmente tornar todos os construtores em data Term a dê um resultado de tipo Term a, ou Term Bool, e as data A definição ainda passaria. Mas não poderíamos escrever eval :: Term a -> a. Você escolhe o Gadt "Tags" para modelar sua Problema, para que as funções úteis que você deseja escrever sejam bem tocadas.

Answer 3

Outros links:

• http://www.haskell.org/haskellwiki/generalised_algebraic_datatype
• http://www.comlab.ox.ac.uk/people/ralf.hinze/talks/fop.pdf

Answer 4

O wiki de Haskell Gadts para manequins é a melhor explicação que já vi.

O problema que eu (e suspeito que os outros) tenham com a maioria das apresentações é que eles mostram exemplos de Gadts em termos de sintaxe que não são óbvios Até que você entenda os Gadts. Isso torna os exemplos mais simples nos quais tudo é construído especialmente difícil de entender - você pode adivinhar o que muitos dos padrões estão fazendo, mas entender o papel exato de cada afirmação é desafiador.

O post "For Dummies" disseca e cria o significado da sintaxe ao longo do caminho para explicar seus próprios exemplos básicos, o que o torna um ponto de partida muito mais útil. Eu recomendo.