4

最近，我想出了一个想法，即可以在 Haskell 中模拟“交叉类型”。具体来说，我的意思是“接口”的交集，因为它们通常是用 OOP 语言构思的。例如，对具有接口和交集类型的语言使用一些伪代码来了解我的意思：

interface HasName {
    val name: String
}

interface HasAge {
    val age: Int
}

-- An object of type HasName & HasAge can call the methods of both
type HasNameAndAge = HasName & HasAge

-- For example:
val myObject: HasNameAndAge = ...
val example = "My name is: ${myObject.name}. My age is ${myObject.age}"

我希望用 Haskell 类型类做类似的事情。我的方法是用* -> ConstraintHaskell 中的元素替换接口（例如，单参数类型类）：

class HasName a where
  name :: a -> String

class HasAge a where
  age :: a -> Int

现在，给定这样的类型类，想法是表单exists a. C a => a（where c :: * -> Constraint）类型的元素对应于“接口”的实现C。给定这样的标识，我们可以通过附加约束轻松构造非匿名交集类型，例如：

{-# LANGUAGE ExistentialQuantification, RankNTypes #-}

-- The intersection of HasName and HasAge:
data HasNameAndAge = forall a. HasNameAndAge ((HasName a, HasAge a) => a)

-- Example:
data Person = Person {
    personName :: String,
    personAge  :: Int
}

instance HasName Person where
    name = personName
instance HasAge Person where
    age = personAge

myObject :: HasNameAndAge
myObject = HasNameAndAge (Person "Nathan" 27)

问题是，试图概括这一点并使其在[* -> Constraint]“对象”实现的接口列表中通用，我无法让 GHC 推断出它需要什么才能使其正常工作。这是我最近的尝试：

{-# LANGUAGE
   ConstraintKinds, 
   KindSignatures, 
   ExistentialQuantification,
   DataKinds,
   TypeFamilies,
   TypeOperators,
   RankNTypes,
   AllowAmbiguousTypes,
   TypeSynonymInstances,
   FlexibleInstances,
   MultiParamTypeClasses,
   FlexibleContexts,
   UndecidableInstances
#-}

import Data.Kind

class Elem (x :: * -> Constraint) (xs :: [* -> Constraint]) where
instance Elem x (x ': xs) where
instance Elem x xs => Elem x (y ': xs) where

type family All (cs :: [* -> Constraint]) a :: Constraint where
  All '[] x = ()
  All (c ': cs) x = (c x, All cs x)

-- The type of "objects" implementing all interfaces cs.
data AbstractType (cs :: [* -> Constraint]) 
    = forall a. All cs a => AbstractType a

-- An example object of type HasName & HasAge.
myObject :: AbstractType '[HasName, HasAge]
myObject = AbstractType $ Person "Nathan" 27

-- Instances needed for every "interface" to get this to work.
instance Elem HasName cs => HasString (AbstractType cs) where
  name (AbstractType x) = name x
instance Elem HasAge cs => HasAge (AbstractType cs) where
  age (AbstractType x) = age x

-- Example:
myObject :: AbstractType '[HasName, HasAge]
myObject = AbstractType $ Person "Nathan" 27

example = do
  print $ age myObject
  putStrLn $ name myObject

看来我需要做更多的刺激才能让 GHC 在这里最后接受我想要的实例。当我尝试编译上述内容时，出现如下错误：

* Could not deduce (HasName a) arising from a use of `name'
      from the context: Elem HasName cs

直观地说，只要是 in就HasName应该成立，因为它是具有约束的存在类型。例如，但是，我不确定如何让 GHC 类型检查器相信这一事实。AbstractType csHasNamecsAbstractType csAll cs aAll '[HasName, HasAge] a = (HasName a, HasAge a)

我也收到如下错误：

* No instance for (Elem HasName '[HasName, HasAge])
    arising from a use of `name'

因此，看来我的类型级别的实现elem不正确，或者 GHC 无法测试 kind 术语之间的相等性* -> Constraint，所以我不确定当前版本的 GHC 是否可行。

4

2 回答 2

3
于 2021-06-17T07:09:50.937 回答
2

仅仅拥有一个带有实例的类c是cs不够的。GHC 实际上需要访问与这些约束相关联的字典才能对它们进行任何计算，但是您编写的类没有提供这些。您需要做的是使用捕获此上下文的函数来扩展该类。像这样的东西：

{-# LANGUAGE TypeApplications #-}

class Elem (c :: * -> Constraint) (cs :: [* -> Constraint]) where
  withC :: All cs a => (c a => a -> x) -> a -> x

instance {-# OVERLAPS #-} Elem x (x ': xs) where
  withC f a = f a

instance Elem x xs => Elem x (y ': xs) where
  withC = withC @x @xs

（编辑说明：奇怪的是，GHC 不需要我们在OVERLAPS此处输入 pragma，但如果我们不包含它，那么我们将永远无法实际使用此类型类。感谢评论中的@dfeuer 解决了这个问题！ )

该withC函数表示，如果我们知道cs某些约束满足其中的所有约束a，那么肯定满足此特定c条件。因此，如果我们有一个a -> x需要约束的函数c a，那么我们可以将 an 转换a为 an x。

有了这个，我们就可以编写你想要的HasName和实例：HasAge

instance Elem HasName cs => HasName (AbstractType cs) where
  name (AbstractType x) = withC @HasName @cs name x

instance Elem HasAge cs => HasAge (AbstractType cs) where
  age (AbstractType x) = withC @HasAge @cs age x

这都是类型检查（尽管我们必须做一些显式的类型注释有点烦人）。

正如@dfeuer 在评论中指出的那样，我们可以通过如下Elem更改类型来使该类更加通用：withC

{-# LANGUAGE AllowAmbiguousTypes #-}

class Elem (c :: * -> Constraint) (cs :: [* -> Constraint]) where
  withC :: forall a r. All cs a => (c a => r) -> r

instance {-# OVERLAPS #-} Elem x (x ': xs) where
  withC r = r

instance Elem x xs => Elem x (y ': xs) where
  withC = withC @x @xs

请注意，要进行类型检查，我们需要启用AllowAmbiguousTypes，因为此时GHC 无法推断出a类型。withC

这看起来很棒，而且肯定更通用（我们可以通过简单地考虑r作为函数类型的规范来恢复旧的行为a -> x），但是必须指定类型a有点麻烦。考虑我们的新实例AbstractType：

instance Elem HasName cs => HasName (AbstractType cs) where
  name (AbstractType (x :: a)) = withC @HasName @cs @a name x

instance Elem HasAge cs => HasAge (AbstractType cs) where
  age (AbstractType (x :: a)) = withC @HasAge @cs @a age x

我们现在需要捕获x模式中的类型，以便我们可以将其提供给withC.

于 2021-06-17T03:43:00.437 回答