Cartesian product of contraints

user_242189 0
Viewed 81

Using a lifted version of (,) for the cartesian product of constraint seems to work until you want to use the fact that it's cartesian, which GHC seems unaware of.

GHC seems to treat '(,) as just an monoïdal product, leading to the error

• Could not deduce: ax ~ '(a, x) arising from a use of ‘Dict’
  from the context: (a ~ Fst ax, x ~ Snd ax)

Although Fst and Snd are not just any projections, they are the cartesian one.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module SO.SO_CartesianProduct where

data Dict c = c => Dict

type family Fst (ij :: (i, j)) :: i
type instance Fst '(i, j) = i

type family Snd (ij :: (i, j)) :: j
type instance Snd '(i, j) = j

class (a ~ Fst ax, x ~ Snd ax) => IsProd ax a x where d :: Dict (ax ~ '(a, x))

instance (a ~ Fst ax, x ~ Snd ax) => IsProd ax a x where
  d = Dict -- • Could not deduce: ax ~ '(a, x) arising from a use of ‘Dict’
  --   from the context: (a ~ Fst ax, x ~ Snd ax)

An attempt to instruct GHC of that fact fails

-- Fails
instance (a ~ Fst ax, x ~ Snd ax) => (ax ~ '(a, x))

-- • Class ‘~’ does not support user-specified instances
-- • In the instance declaration for ‘(ax ~ '(a, x))’typ

Is there anyway to instruct GHC that it's actually cartesian, or to get a product recognized as cartesian by GHC in some way ?

typeclass haskell
1 Answers

If you put the pair into "canonical form" (any pair p can be written in canonical form as (fst p, snd p)), this fixes the type error:

type family Canonical p where
  Canonical p = '(Fst p, Snd p)

class (a ~ Fst ax, x ~ Snd ax) => IsProd ax a x where d :: Dict (Canonical ax ~ '(a, x))

instance (a ~ Fst ax, x ~ Snd ax) => IsProd ax a x where
  d = Dict

Incidentally, I recommend using closed type families (like how Canonical is written) where possible (when you don't need the type family to be potentially extended later on). I've found it helps with certain problems and makes things easier.

I'm not sure if this will entirely fit with the rest of your problem, though. It's possible that, even though this fixes the type error, it may still not integrate with the rest of what you want to do.

user_24767350
Related