Uma descrição matemática (categórica) das classes de tipos

14

Uma linguagem funcional pode ser vista como uma categoria em que seus objetos são tipos e funções de morfismos entre eles.

Como as classes de tipo se encaixam nesse modelo?

Suponho que devemos considerar apenas as implementações que satisfazem a restrição que a maioria das classes de tipo possui, mas que não são expressas em Haskell. Por exemplo, devemos considerar apenas as implementações Functorpara as quais fmap id ≡ ide fmap f . fmap g ≡ fmap (f . g).

Ou existem outros fundamentos teóricos para classes de tipos (por exemplo, com base em cálculos lambda digitados)?

Petr Pudlák
fonte
1
Você pode ser mais explícito sobre exatamente para o que deseja um modelo. Se você deseja algo que possa descrever rigorosamente a suposição do mundo aberto, o comportamento da resolução de instâncias, a interação de várias extensões do GHC, etc., isso é um pouco mais complicado do que uma versão idealizada. Da mesma forma, observe que os fundos são frequentemente ignorados ao discutir o Hask.
CA McCann
4
As classes de tipo podem ser consideradas assinaturas (no sentido universal da álgebra). A coleção de todas as entidades que compartilham a mesma assinatura (elementos da mesma classe de tipo) é uma variedade .
Dave Clarke
1
@DaveClarke: Não é imediatamente óbvio para mim como descrever classes de tipos em tipos superiores dessa maneira, mas eu não estou muito familiarizado com álgebra universal e pode estar entendendo mal a correspondência que você tem em mente ...
CA McCann
1
@camccann: Não sei até que ponto a correspondência vai. Certamente parecia um bom ponto de partida.
Dave Clarke
2
@camccann: Basta alterar a categoria base sobre a qual você está definindo sua álgebra: classes de tipo básicas como num são assinaturas sobre a categoria de tipos de haskell (ou objetos da categoria Hsk), classes de tipo sobre construtores de tipo são álgebras sobre a categoria de functores de Hask para Hask. Observe que a álgebra universal é completamente subsumida pela noção de álgebra na teoria das categorias. Também: Dave: você deve transformar seu comentário em uma resposta.
Cody

Respostas:

18

Como as classes de tipo se encaixam nesse modelo?

A resposta curta é: eles não.

Sempre que você introduz coerções, classes de tipo ou outros mecanismos de polimorfismo ad-hoc em um idioma, o principal problema de design que você enfrenta é a coerência .

Basicamente, você precisa garantir que a resolução da classe de tipo seja determinística, para que um programa bem digitado tenha uma única interpretação. Por exemplo, se você pudesse fornecer várias instâncias para o mesmo tipo no mesmo escopo, poderia escrever programas ambíguos como este:

class Blah a where
   blah : a -> String 

instance Blah T where
   blah _ = "Hello"

instance Blah T where
   blah _ = "Goodbye"

v :: T = ...

main :: IO ()
main = print (blah v)  -- does this print "Hello" or "Goodbye"?

Dependendo da escolha da instância que o compilador faz, blah vpode ser igual a "Hello"ou "Goodbye". Portanto, o significado de um programa não seria completamente determinado pela sintaxe do programa, mas poderia ser influenciado por escolhas arbitrárias que o compilador faz.

A solução de Haskell para esse problema é exigir que cada tipo tenha no máximo uma instância para cada classe de tipo. Para garantir isso, ele permite declarações de instância apenas no nível superior e além disso torna todas as declarações globalmente visíveis. Dessa forma, o compilador sempre pode sinalizar um erro se uma declaração de instância ambígua for feita.

No entanto, tornar as declarações globalmente visíveis quebra a composicionalidade da semântica. O que você pode fazer para recuperar é fornecer uma semântica de elaboração para a linguagem de programação - ou seja, você pode mostrar como traduzir os programas Haskell em uma linguagem mais comportamental e de composição.

Na verdade, isso também oferece uma maneira de compilar classes de tipos - geralmente é chamada de "tradução de evidências" ou "transformação de passagem de dicionário" nos círculos Haskell e é um dos estágios iniciais da maioria dos compiladores Haskell.

As classes tipográficas também são um bom exemplo de como o design da linguagem de programação difere da teoria pura do tipo. As classes de tipo são um recurso de linguagem realmente impressionante, mas são muito mal-comportadas do ponto de vista da teoria da prova. (É por isso que a Agda não possui classes tipográficas e a Coq as faz parte de sua infraestrutura de inferência heurística.)

Neel Krishnaswami
fonte
o que é o vice-campeão candidato que não tem semântica denotacional iyswim?
Oade Kammar
1
Eu não tenho ideia, infelizmente.
Neel Krishnaswami
Isso merece uma pergunta adicional?
Oade Kammar
@NeelKrishnaswami: Você tem alguma idéia de como os módulos ML se encaixam nisso? E quanto aos módulos Agda (que alguém me mencionou como sendo de "primeira classe")?
Lii
1
@Lii: Os módulos ML e os registros Agda são muito mais bem comportados, mas é muito complicado explicar em um comentário - faça uma pergunta sobre eles e eu (ou outra pessoa) explicarei.
Neel Krishnaswami