haskell - 使用类型族和泛型查找 Id 值

Question

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

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

newtype Id = Id { _id :: Int }

并且您想要定义一个函数 getId，从至少包含一个 Id 值的任何结构中提取此 Id:

class Identifiable e where
    getId :: e -> Id

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

在我的previous question有人向我指出了类型家庭，特别是 described in this blog post 的想法。 。据我了解，这个想法是定义一个类型类 MkIdentABLE ，这样:

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

仅当其中至少嵌套有一个 Id 值时，该值才属于 Res 类型:

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))

其中选择类似于上述博客文章中定义的内容:

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) 具有 Res 类型，并且需要一个类型。

Answer 1

您已经非常接近进行Choose 类型检查了。 L1 和 R1 是 (:+:) 的构造函数，而不是 Crumbs。还有一个类型 GHC.Generics.R::* ，它在类型级别隐藏 Crumbs 的 R 构造函数，但您可以使用 '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