Familias de tipo cerrado e inferencia de tipo en Haskell

types ghc

Question

En GHC-7.7 (y 7.8) se introdujeron familias de tipo cerrado:

Una familia de tipo cerrado tiene todas sus ecuaciones definidas en un solo lugar y no se puede ampliar, mientras que una familia abierta puede tener instancias repartidas entre módulos. La ventaja de una familia cerrada es que sus ecuaciones se intentan en orden, similar a una definición de función de nivel de término

Quiero preguntarte, ¿por qué el siguiente código no se compila? GHC debería poder inferir todos los tipos: GetTheType se define solo para el tipo X y si comentamos la línea marcada, el código se compila.

¿Se trata de un error en GHC o las familias de tipo cerrado no tienen tales optimizaciones AÚN?

código:

{-# LANGUAGE TypeFamilies #-}
data X = X
type family GetTheType a where
GetTheType X = X
class TC a where
tc :: GetTheType a -> Int
instance TC X where
tc X = 5
main = do
-- if we comment out the following line, the code compiles
let x = tc X
print "hello"

Y el error es:

Couldn''t match expected type ‛GetTheType a0’ with actual type ‛X’
The type variable ‛a0’ is ambiguous
In the first argument of ‛tc’, namely ‛X’
In the expression: tc X

Answer 1

No hay nada malo con las familias de tipo cerrado. El problema es que las funciones tipográficas no son inyectivas.

Digamos, usted podría tener esta función de tipo cerrado:

data X = X
data Y = Y
type family GetTheType a where
GetTheType X = X
GetTheType Y = X

no se puede inferir el tipo de argumento del tipo de resultado X

Las familias de datos son inyectivas, pero no cerradas:

{-# LANGUAGE TypeFamilies #-}
data X = X
data family GetTheType a
data instance GetTheType X = RX
class TC a where
tc :: (GetTheType a) -> Int
instance TC X where
tc RX = 5
main = do
let x = tc RX
print "hello"