Convertir instancias de familia de tipos a Int
-
14-12-2019 - |
Pregunta
Tengo este código:
type family Id obj :: *
type instance Id Box = Int
Y quiero que siempre pueda obtener un Int de la familia de tipos Id.Reconozco que será necesaria una conversión.
Pensé que tal vez crear una clase funcionaría:
class IdToInt a where
idToInt :: Id a -> Int
instance IdToInt Box where
idToInt s = s
Y eso realmente se compila.Pero cuando intento usarlo:
testFunc :: Id a -> Int
testFunc x = idToInt x
me sale error:
src/Snowfall/Spatial.hs:29:22:
Couldn't match type `Id a0' with `Id a'
NB: `Id' is a type function, and may not be injective
In the first argument of `idToInt', namely `x'
In the expression: idToInt x
In an equation for `testFunc': testFunc x = idToInt x
Entonces, ¿cómo puedo crear una conversión para un ID de familia de tipos para obtener un Int?
Según la respuesta de ehird, intenté lo siguiente pero tampoco funciona:
class IdStuff a where
type Id a :: *
idToInt :: Id a -> Int
instance IdStuff Box where
type Id Box = Int
idToInt s = s
testFunc :: (IdStuff a) => Id a -> Int
testFunc x = idToInt x
Da error:
src/Snowfall/Spatial.hs:45:22:
Could not deduce (Id a0 ~ Id a)
from the context (IdStuff a)
bound by the type signature for
testFunc :: IdStuff a => Id a -> Int
at src/Snowfall/Spatial.hs:45:1-22
NB: `Id' is a type function, and may not be injective
In the first argument of `idToInt', namely `x'
In the expression: idToInt x
In an equation for `testFunc': testFunc x = idToInt x
Solución
Como otros han señalado, el problema es que el compilador no puede determinar qué a
usar.Las familias de datos son una solución, pero una alternativa con la que a veces es más fácil trabajar es utilizar un testigo de tipo.
Cambia tu clase a
class IdToInt a where
idToInt :: a -> Id a -> Int
instance IdToInt Box where
idToInt _ s = s
-- if you use this a lot, it's sometimes useful to create type witnesses to use
box = undefined :: Box
-- you can use it like
idToInt box someId
-- or
idToInt someBox (getId someBox)
La pregunta que debes responder es, para cualquier Id
, ¿hay solo un tipo? a
debería aparecer con?Es decir, ¿existe una correspondencia uno a uno entre a
arena Id a
¿s?Si es así, las familias de datos son el enfoque correcto.Si no, quizás prefiera un testigo.
Otros consejos
no puedes.Necesitará testFunc :: (IdToInt a) => Id a -> Int
.Tipo Las familias están abiertas, por lo que cualquiera puede declarar
type instance Id Blah = ()
en cualquier momento y no ofrezca ninguna función de conversión.Lo mejor que puede hacer es poner la familia tipo en la clase:
class HasId a where
type Id a
idToInt :: Id a -> Int
instance IdToInt Box where
type Id Box = Int
idToInt s = s
Aún necesitarás el contexto, sin embargo.
No puedes usar una función de tipo IdToInt a => Id a -> Int
porque no hay manera de determinar qué tipo a
es.El siguiente ejemplo demuestra esto.
type family Id a :: *
type instance Id () = Int
type instance Id Char = Int
class IdToInt a where idToInt :: Id a -> Int
instance IdToInt () where idToInt x = x + 1
instance IdToInt Char where idToInt x = x - 1
main = print $ idToInt 1
Porque Id () = Id Char = Int
, el tipo de idToInt
en el contexto anterior es Int -> Int
, que es igual a Id () -> Int
y Id Char -> Int
.Recuerde que los métodos sobrecargados se eligen según el tipo.Ambas instancias de clase definen idToInt
funciones que tienen tipo Int -> Int
, por lo que el verificador de tipos no puede decidir cuál usar.
Debería utilizar una familia de datos en lugar de una familia de tipos y declarar instancias de nuevo tipo.
data family Id a :: *
newtype instance Id () = IdUnit Int
newtype instance Id Char = IdChar Int
Con una instancia de nuevo tipo, Id ()
y Id Char
Ambos son enteros, pero tienen diferentes tipos.El tipo de un Id
informa al verificador de tipo qué función sobrecargada usar.