Использование семейства типов и Generics для поиска значения Id

Question

Этот вопрос относится к этому вопросу, где я хотел избежать шаблон извлечения Id значение из структуры данных, но типобезопасным способом.

Я повторю соответствующие детали проблемы здесь: предположим, у вас есть тип Id:

newtype Id = Id { _id :: Int }

И вы хотите определить функцию getId что извлекает это Id из любой структуры, которая содержит хотя бы один Id значение:

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) имеет вид Res и тип ожидается вместо этого.

Answer 1

Ты довольно близок к тому, чтобы Choose typecheck. 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