Deriving instances for GADT containing Nat fields

Learn
#1

I have a multi-index type (i.e. a value together with a tuple of natural numbers), and I would like to give it e.g. an Ord instance to use its values within a data structure. I understand having Nat in there is a complication but I can’t understand why.

data Multi :: [Nat] -> * -> * where
  MVal :: a -> Multi '[] a
  (:*) :: KnownNat n => Proxy n -> Multi ns a -> Multi (n ': ns) a

-- >>> (Proxy :: Proxy 32) :* (Proxy :: Proxy 16) :* (MVal pi)
--  :: Floating a => Multi '[32, 16] a

The instance (Eq a, Ord a) => Ord (Multi '[] a) case (corresponding to the MVal constructor) is straightforward but I can’t wrap my head around the other one. I’d be happy to pull in a library for this, as long as its dependency footprint is reasonably small.

Thank you in advance for any help and/or pointers.

1 Like
#2

I’m not sure I understand the question. Why isn’t it enough to do this?

deriving instance Ord a => Ord (Multi ns a)

If you are writing it explicitly, the type indices mean that you only need to compare MVal with MVal or :* with :*, because the other cases are ruled out by the types. Moreover all the statically-determined Nats must be equal for the comparison to be well-typed. So ultimately all you end up comparing is the value under the MVal.

1 Like
#3

Ah, I hadn’t thought it would work with StandaloneDeriving . Thank you!

#4

Generally speaking when deriving instances for GADTs you often need StandaloneDeriving, in order to specify the instance contexts explicitly. It works by generating the derived instances and then type-checking them, so if it doesn’t work it isn’t always obvious why, but for simple cases it is rather useful.

1 Like