使用类型族和泛型来查找Id值 [英] Using type families and Generics to find an Id value

问题描述

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

I'在这里重复问题的相关细节：假设你有一个类型 Id ：

  newtype Id = Id {_id :: Int} 
  

你想定义一个函数 getId 从至少包含一个 Id Id $ c $ value：

  class可识别的e其中
 getId :: e  - > Id 
  

现在的问题是如何在类型安全的 strong>方式，同时避免使用泛型的样板。在我的上一个问题我被指向类型族，特别是在此博客文章中描述。据我了解，这个想法是定义一个类型类 MkIdentifiable ，例如：

  class MakeIdentifiable（res :: Res）e其中
 mkGetId :: Proxy res  - > e  - > Id 
  

如果值的类型为 Res 仅当嵌套在其中的至少一个 Id 值时：

  data Crumbs = Here | L面包屑| R Crumbs 
数据Res = Found Crumbs | NotFound 
  

然后，您可以定义：

 实例MakeIdentifiable（找到e）e =>可识别的e，其中
 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（lp））（HasId（rp））
  
 $ b $ 选择就像前面提到的博客文章所定义的那样： / p> 
 
 
  type family选择ef :: Res其中
选择（找到a）b =找到（L1 a）
选择a（找到b）=找到（R1 b）
选择ab =未找到
  
但是，这不会被编译为 HasId（lp）有类型 Res ，而是预期类型。 
解决方案
您非常接近选择 typecheck。  L1 和 R1 是（：+：）的构造函数， ，而不是面包屑。还有一个类型 GHC.Generics.R :: * ，它从隐藏了 R 构造函数。 Crumbs 在类型级别，但是您可以使用'R 来消除歧义（单引号是构造函数，双引号是类型构造函数）。 
 
 
 
注释各种类型也是一种很好的做法，就像我们注释顶级函数的类型一样。
 
 
 <$ p $ （e :: Res）（f :: Res）:: Res其中
选择（找到a）b =找到（'L a）
选择（找到b）=找到（'R b）
选择NotFound NotFound = NotFound  - 我不是重叠家庭的粉丝
  

This question is related to this one, where I wanted to avoid the boilerplate of extracting an Id value from a data structure, but in a type-safe manner.

I'll repeat the relevant details of the problem here: suppose you have a type Id:

newtype Id = Id { _id :: Int }

And you want to define a function getId that extracts this Id from any structure that contains at least one Id value:

class Identifiable e where
    getId :: e -> Id

Now the problem is how to define such a class in a type-safe manner, while at the same time avoiding the boilerplate using Generics.

In my previous question I was pointed to type families, and in particular to the ideas described in this blog post. As far as I understand the idea is to define a type-class MkIdentifiable such that:

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

Where a value is of type Res only if there is at least one Id value that is nested inside of it:

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

Then, it seems, one could define:

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

Now the question is how to define a type family for Res that is associated to the types of GHC.Generics (U1, K1, :*:, :+:).

I've tried the following:

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

Where Choose would be something like what is defined in the aforementioned blog post:

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

But this won't compile as HasId (l p) has kind Res and a type is expected instead.

解决方案

You're pretty close to making Choose typecheck. L1 and R1 are constructors of (:+:), not Crumbs. There's also a type GHC.Generics.R :: * which hides the R constructor from Crumbs at the type level, but you can use 'R to disambiguate (singly-quoted names are constructors, doubly-quoted are type constructors).

It's also good practice to annotate kinds of types, much like we annotate types of toplevel functions.

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

这篇关于使用类型族和泛型来查找Id值的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！