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.