Una descripción matemática (categórica) de las clases de tipos.

Un lenguaje funcional puede verse como una categoría donde sus objetos son tipos y las funciones de morfismos entre ellos.

¿Cómo encajan las clases de tipos en este modelo?

Supongo que solo deberíamos considerar aquellas implementaciones que satisfacen la restricción que tienen la mayoría de las clases de tipos, pero que no se expresan en Haskell. Por ejemplo, solo debemos considerar las implementaciones de Functorfor which fmap id ≡ idy fmap f . fmap g ≡ fmap (f . g).

¿O hay otros fundamentos teóricos para las clases de tipos (por ejemplo, basados ​​en cálculos lambda mecanografiados)?

¿Cómo encajan las clases de tipos en este modelo?

La respuesta corta es: no lo hacen.

Cada vez que introduce coacciones, clases de tipos u otros mecanismos para el polimorfismo ad-hoc en un lenguaje, el principal problema de diseño que enfrenta es la coherencia .

Básicamente, debe asegurarse de que la resolución de la clase de tipos sea determinista, de modo que un programa bien tipado tenga una única interpretación. Por ejemplo, si pudiera dar varias instancias para el mismo tipo en el mismo ámbito, podría escribir programas ambiguos 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"?

Dependiendo de la elección de instancia que haga el compilador, blah vpodría ser igual a "Hello"o "Goodbye". Por lo tanto, el significado de un programa no estaría completamente determinado por la sintaxis del programa, sino que podría verse influenciado por elecciones arbitrarias que realiza el compilador.

La solución de Haskell a este problema es requerir que cada tipo tenga como máximo una instancia para cada clase de tipo. Para garantizar esto, permite declaraciones de instancia solo en el nivel superior y, además, hace que todas las declaraciones sean visibles globalmente. De esa manera, el compilador siempre puede señalar un error si se hace una declaración de instancia ambigua.

Sin embargo, hacer declaraciones globalmente visibles rompe la composicionalidad de la semántica. Lo que puede hacer para recuperarse es proporcionar una semántica de elaboración para el lenguaje de programación, es decir, puede mostrar cómo traducir los programas de Haskell a un lenguaje más compositivo y de mejor comportamiento.

En realidad, esto también le brinda una forma de compilar clases de tipos: generalmente se llama "traducción de evidencia" o "transformación de pasar diccionario" en los círculos de Haskell, y es una de las primeras etapas de la mayoría de los compiladores de Haskell.

Las clases de tipos también son un buen ejemplo de cómo el diseño del lenguaje de programación difiere de la teoría de tipos pura. Las clases de tipos son una característica del lenguaje realmente impresionante, pero se comportan bastante mal desde un punto de vista teórico de la prueba. (Esta es la razón por la cual Agda no tiene clases de tipos en absoluto, y por qué Coq los hace parte de su infraestructura de inferencia heurística).