Trying to develop a recursive type-level function to derive function input and output

Question

The following definitons are kind of required to understand what I'm asking:

data Param = PA | PB | PC

data R p a where
  A :: S a -> R PA (S a)
  B :: S a -> R PB (S a)

data S a where
  Prim :: a -> S a
  HO   :: R pa a -> R pb b -> S ((R pa a) -> (R pb b))
  Pair :: R pa a -> R pb b -> S ((R pa a), (R pb b))

data Box r a = Box r a  

I would like to write a function using these definitions that works as follows:

trans :: t -> TransIn t -> TransOut t

where

TransIn (R 'PA (S a)) = a
TransIn (R 'PB (S a)) = a
TransIn (R 'PA (S (r1, r2))) = (TransIn r1, TransIn r2)
TransIn (R 'PA (S (r1, r2))) = (TransIn r1, TransIn r2)
TransIn (R 'PA (S (r1 -> r2))) = Error
TransIn (R 'PB (S (r1 -> r2))) = TransOut r1 -> TransIn r2

and

TransOut (R 'PA (S a)) = Box (R 'PA (S a)) a
TransOut (R 'PB (S a)) = Box (R 'PB (S a)) a
TransOut (R 'PA (S (r1, r2))) = (TransOut r1, TransOut r2)
TransOut (R 'PA (S ((R p (S a)), R p (S b))))) = (Box (R p (S a)) a, Box (R p (S b)) b)
TransOut (R 'PA (S (r1 -> r2))) = Error
TransOut (R 'PB (S (r1 -> r2))) = TransIn r1 -> TransOut r2

The basic idea is to accept different shapes of input and produce different shapes of output based on the constructor used for S and the parameter chosen when building R. I've been trying to do this using classes with data kinds, but I'm getting kind mis-match errors. I was wondering if there was an intuitive, clean way to encode this type of thing.

The current attempt I have is as follows:

class Transform t a where
  data TransIn t a:: *
  data TransOut t a:: *
  trans :: t -> TransIn t a -> TransOut t a

instance Transform (R Param (S a)) a where
  data TransIn (A (S a)) a :: a
  data TransOut (A (S a)) a :: Box (R Param (S a)) a
  trans t a = Box t a

instance Transform (R Param (S (a -> b))) a where
  data TransIn (A (S (a -> b))) (a -> b) :: TransIn a -> TransIn b
  data TransOut (A (S (a -> b))) (a -> b) :: TransOut a -> TransOut b
  trans _ _ = undefined

This approach complains that the first argument of R should have kind Param but Param has kind *, and I'm not sure how to correct this. When adding a constraint and using a variable, I got here:

instance (p :: Param) => Transform (R p (S a)) a where
  data TransIn (R p (S a))) a :: a
  data TransOut (R p (S a)) a :: Box (R p (S a)) a
  trans t a = Box t a

Of course, Haskell has refused to let me use a Kind as a constraint. I'm pretty lost, and I'm not sure where to go with this. Any help or guidance would be invaluable.

Answer 1

I would start with a single-parameter type class with two associated type families for TransIn and TransOut.

class Transform t where
  type TransIn t
  type TransOut t
  trans :: t -> TransIn t -> TransOut t

Now you need six instances for the six equations for TypeIn and TypeOut. Here is the first one.

instance Transform (R PA (S a)) where
  type TransIn (R PA (S a)) = a
  type TransOut (R PA (S a)) = Box (R PA (S a)) a
  trans t a = error "implement me!"

Note that the definitions for TransIn and TransOut are literally the equations from the question.