将类型族实例转换为 Int

Question

我有这个代码：

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

我想要做到这一点，这样我总能从 Id 类型系列中获得一个 Int。我认识到需要进行转换。

我想也许创建一个类会起作用：

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

那么，如何为类型族 Id 创建转换以获得 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

你不能。您需要testFunc :: (IdToInt a) => Id a -> Int。类型的家庭是开放的，所以任何人都可以声明

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 通知类型检查器要使用哪个重载函数。