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"