enforcing tag uniqueness

[joeyh]

"Each tag must be unique within a given message, though this is not currently checked or enforced."

I really like this library, but keeping the tags unique has felt like walking on eggshells when using it. Perhaps there could be some way to enforce tag uniqueness?

[NathanHowell]

Certainly would be a desirable addition. I think it can be done with Sort and a variation of Nub from either https://hackage.haskell.org/package/singletons-2.2 (in Data.Singletons.Prelude.List) or the slightly lighter https://hackage.haskell.org/package/type-level-sets. Always happy to take pull requests :-)

[joeyh]

Ah, so the Generics code has a type-level list of all the tags used? I have not dug into your implementation details.

…

-- see shy jo

[NathanHowell]

It does, sort of. The structure of the message can be traversed and field tags extracted at compile time, here's the basic idea:

{-# language DataKinds #-}
{-# language KindSignatures #-}
{-# language PolyKinds #-}
{-# language TypeFamilies #-}
{-# language TypeOperators #-}
{-# language UndecidableInstances #-}

import GHC.Generics
import GHC.TypeLits

data Field (n :: Nat) a

type family Concat (x :: [k]) (y :: [k]) :: [k] where
  Concat (x ': xs) ys = x ': Concat xs ys
  Concat '[] ys = ys

type family FieldTags (f :: * -> *) :: [Nat] where
  FieldTags (M1 i c a) = FieldTags a
  FieldTags (a :*: b) = Concat (FieldTags a) (FieldTags b)
  FieldTags (a :+: b) = Concat (FieldTags a) (FieldTags b)
  FieldTags (K1 i (Field n a)) = '[n]

Applying FieldTags to the generic representation of the message will return a type level list containing the tags. Then it's just a matter of sorting them and checking for duplicates.

Ok, modules loaded: Main.
*Main> :kind! FieldTags (Rep (Field 1 Int, Field 3 Double))
FieldTags (Rep (Field 1 Int, Field 3 Double)) :: [Nat]
= '[1, 3]