Convertir les instances de famille de types en Int

Question

J'ai ce code :

type family Id obj :: *
type instance Id Box = Int

Et je veux faire en sorte que je puisse toujours obtenir un Int de la famille de types Id.Je reconnais qu'une conversion sera nécessaire.

Je pensais que créer une classe fonctionnerait peut-être :

class IdToInt a where
  idToInt :: Id a -> Int

instance IdToInt Box where
  idToInt s = s

Et cela compile réellement.Mais quand j'essaye de l'utiliser :

testFunc :: Id a -> Int
testFunc x = idToInt x

J'obtiens l'erreur :

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

Alors, comment puis-je créer une conversion pour un identifiant de famille de types afin d'obtenir un Int ?

Sur la base de la réponse d'ehird, j'ai essayé ce qui suit mais cela ne fonctionne pas non plus :

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

Cela donne l'erreur :

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

Answer 1

Comme d'autres l'ont souligné, le problème est que le compilateur ne peut pas déterminer quel a utiliser.Les familles de données sont une solution, mais une alternative parfois plus facile à utiliser consiste à utiliser un témoin de type.

Changez votre classe en

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 question à laquelle vous devez répondre est, pour une donnée donnée Id, n'y a-t-il qu'un seul type a ça devrait apparaître avec ?Autrement dit, existe-t-il une correspondance biunivoque entre asable Id as?Si tel est le cas, les familles de données constituent la bonne approche.Sinon, vous préférerez peut-être un témoin.

Answer 2

Vous ne pouvez pas.Tu auras besoin testFunc :: (IdToInt a) => Id a -> Int.Les familles de types sont ouvertes, donc tout le monde peut déclarer

type instance Id Blah = ()

à tout moment et n'offrent aucune fonction de conversion.La meilleure chose à faire est de mettre la famille de types dans la classe :

class HasId a where
  type Id a
  idToInt :: Id a -> Int

instance IdToInt Box where
  type Id Box = Int
  idToInt s = s

Cependant, vous aurez toujours besoin du contexte.

Answer 3

Vous ne pouvez pas utiliser une fonction de type IdToInt a => Id a -> Int car il n'y a aucun moyen de déterminer quel type a est.L’exemple suivant le démontre.

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

Parce que Id () = Id Char = Int, le type de idToInt dans le contexte ci-dessus est Int -> Int, qui est égal à Id () -> Int et Id Char -> Int.N'oubliez pas que les méthodes surchargées sont choisies en fonction du type.Les deux instances de classe définissent idToInt fonctions qui ont le type Int -> Int, le vérificateur de type ne peut donc pas décider lequel utiliser.

Vous devez utiliser une famille de données au lieu d'une famille de types et déclarer de nouvelles instances de type.

data family Id a :: *
newtype instance Id () = IdUnit Int
newtype instance Id Char = IdChar Int

Avec une instance de nouveau type, Id () et Id Char sont tous deux des entiers, mais ils ont des types différents.Le type d'un Id informe le vérificateur de type quelle fonction surchargée utiliser.