Haskell:类型族的实例定义

Cli*_*ton 2 haskell type-families

可以说我们有以下代码:

class C t where
  g :: t

instance C Int where
  g = 42
Run Code Online (Sandbox Code Playgroud)

简单.我们也可以在Int上定义函数,如下所示:

f1 :: Int -> Int
f1 x = x * x
Run Code Online (Sandbox Code Playgroud)

我一直在使用类型系列,特别是因为Data.Has使用它们,我想将它们插入到IxSet.

但在这里,我将提出一个简化的例子.让我们说我们想要定义一个X类似于Int 的新类型.我们可以这样做:

type family X
type instance X = Int
Run Code Online (Sandbox Code Playgroud)

然后我们可以X像这样定义函数:

f2 :: X -> X
f2 x = x * x + 1
Run Code Online (Sandbox Code Playgroud)

到目前为止没问题.现在让我们尝试定义一个实例C X,就像我们为C Int:

instance C X where
  g = 43
Run Code Online (Sandbox Code Playgroud)

哦,现在我们有以下错误:

实例中的非法类型同义词族应用程序:X
在实例声明中'C X'

现在让我们尝试一些不同的东西:

newtype NewX = NewX X

instance C NewX where
  g = 43
Run Code Online (Sandbox Code Playgroud)

现在我们又遇到了另一个错误,即:

没有(Num NewX)
文字引起的实例'43'

似乎该newtype关键字消除了有关前一类所属的类的任何信息.但是,我似乎无法避免newtype,因为我无法在实例定义中使用类型系列.

有没有更好的方法来做到这一点,而不必用额外的显式实例重写实例定义,否则将被推断?


背景资料:

我需要这个工作的原因如下:

import Data.Has
import Data.IxSet

data Col1 = Col1; type instance TypeOf Col1 = Text
data Col2 = Col2; type instance TypeOf Col2 = Text

type Row = FieldOf Col1 :&: FieldOf Col2;

instance Indexable Row where
  empty = ixSet [ixFun $ (\x -> [ Col1 ^. x ]) ] -- Maybe add some more indexes later
Run Code Online (Sandbox Code Playgroud)

这失败了:

实例中的非法类型同义词族应用程序:Row
在实例声明中'Indexable Row'

制作Row一个newtype导致以下错误:

使用"^"时没有(Contains(Labeled Col1 Text)Row)的实例.可能的解决方法:为(Contains(Labeled Col1 Text)Row添加实例声明)

我可以解决这个问题的唯一方法是添加一个long derinding子句,如下所示:

newtype Row = Row (FieldOf Col1 :&: FieldOf Col2)
  deriving 
  (
    Contains (Labelled Col1 Text), -- Add this for every column
    Contains (Labelled Col2 Text)  -- ...
  )
Run Code Online (Sandbox Code Playgroud)

即使是一些,让我"的typedef" Contains (Labelled x (TypeOf x))HasCol x将是有益的.

Dan*_*ner 5

以下文件在此处编译:

{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies #-}

class C a where g :: a
type family X
type instance X = Int
newtype NewX = NewX X deriving Num
instance C NewX where g = 43
Run Code Online (Sandbox Code Playgroud)