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

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)?

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.)