转换型家庭实例来诠释

Question

我有这样的代码：

type family Id obj :: * 
type instance Id Box = 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 

所以，我怎样才能创建一个类型系列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 s和Id a s之间是否存在一对一的对应关系？如果是这样，数据族是正确的方法。如果没有，你可能更喜欢见证人。

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