4

这个问题与这个问题有关，我想避免Id从数据结构中提取值的样板，但以类型安全的方式。

我将在这里重复问题的相关细节：假设您有一个类型Id：

newtype Id = Id { _id :: Int }

并且您想定义一个函数，该函数从任何包含至少一个值的结构getId中提取它：IdId

class Identifiable e where
    getId :: e -> Id

现在的问题是如何以类型安全的方式定义这样的类，同时避免使用泛型的样板。

在我之前的问题中，我提到了类型系列，特别是这篇博文中描述的想法。据我了解，这个想法是定义一个类型类MkIdentifiable，以便：

class MakeIdentifiable (res :: Res) e where
    mkGetId :: Proxy res -> e -> Id

一个值只有在其中嵌套Res了至少一个值时才属于类型：Id

data Crumbs = Here | L Crumbs | R Crumbs
data Res = Found Crumbs | NotFound

然后，似乎可以定义：

instance MakeIdentifiable (Found e) e => Identifiable e where
    getId = mkGetId (Proxy :: Proxy (Found e))

现在的问题是如何定义Res与 GHC.Generics ( U1, K1, :*:, :+:) 的类型相关联的类型族。

我尝试了以下方法：

type family HasId e :: Res where
    HasId Id = Found Here
    HasId ((l :+: r) p) = Choose (HasId (l p)) (HasId (r p))

哪里Choose会像上述博客文章中定义的那样：

type family Choose e f :: Res where
    Choose (Found a) b = Found (L1 a)
    Choose a (Found b) = Found (R1 b)
    Choose a b = NotFound

但这不会像HasId (l p)has kind那样编译，Res而是需要一个类型。

4

1 回答 1

2

你非常接近进行Choose类型检查。L1并且R1是 的构造函数(:+:)，而不是Crumbs。还有一种类型在类型级别GHC.Generics.R :: *隐藏R构造函数，但您可以使用它来消除歧义（单引号名称是构造函数，双引号是类型构造函数）。Crumbs'R

注释类型也是一种很好的做法，就像我们注释顶级函数的类型一样。

type family Choose (e :: Res) (f :: Res) :: Res where
  Choose (Found a) b = Found ('L a)
  Choose a (Found b) = Found ('R b)
  Choose NotFound NotFound = NotFound  -- I'm not a fan of overlapping families
于 2017-12-05T13:10:52.287 回答