Преобразовать экземпляры семейства типов в Int

Question

У меня есть этот код:

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

И я хочу сделать это так, чтобы я всегда мог получить Int из семейства типов Id.Я признаю, что потребуется преобразование.

Я подумал, что, возможно, создание класса сработает:

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

instance IdToInt Box where
  idToInt s = s

И это действительно компилируется.Но когда я пытаюсь им воспользоваться:

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

Я получаю сообщение об ошибке:

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

Итак, как я могу создать преобразование для идентификатора семейства типов, чтобы получить Int?

Основываясь на ответе ehird, я попробовал следующее, но это тоже не работает:

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

Это выдает ошибку:

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

Как отмечали другие, проблема в том, что компилятор не может определить, какой именно 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)

Вопрос, на который вам нужно ответить, заключается в том, что для любого данного Id, существует ли только один тип a это должно появиться с помощью?То есть, существует ли взаимно однозначное соответствие между aы и Id aс?Если это так, то правильным подходом являются семейства данных.Если нет, то вы, возможно, предпочтете свидетеля.

Answer 2

Вы не можете.Вам понадобится генеракодицетагкод.Тип семейства открыты, поэтому любой может объявить

type instance Id Blah = ()

.

в любое время, и предложить никакой функции преобразования.Лучшее, что нужно сделать, это поставить тип семейства в классе:

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

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

.

Вам еще понадобится контекст.

Answer 3

Вы не можете использовать функцию типа IdToInt a => Id a -> Int потому что нет никакого способа определить, какой тип a является.Следующий пример демонстрирует это.

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

Потому что Id () = Id Char = Int, тип idToInt в приведенном выше контексте это Int -> Int, который равен Id () -> Int и Id Char -> Int.Помните, что перегруженные методы выбираются в зависимости от типа.Оба экземпляра класса определяют idToInt функции, имеющие тип Int -> Int, поэтому средство проверки типов не может решить, какой из них использовать.

Вы должны использовать семейство данных вместо семейства типов и объявлять экземпляры newtype.

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

С экземпляром newtype, Id () и Id Char оба являются целыми числами, но у них разные типы.Тип объекта Id сообщает средству проверки типов, какую перегруженную функцию использовать.