Hi adam,
Thanks for your answer.
2014-06-13 19:36 GMT+02:00 adam vogt
Hi Gautier,
It's possible you want:
type instance HSplit ts xs = '(xs, SndHSplit ts xs)
[xs] stands for the ordinary list type constructor applied to xs ([] xs). But ghci can tell you with ":kind []" that [] :: * -> *. Similarly, (,) in the instance stands for (,) :: * -> * -> *, while the (,) in ([k], [k]) is actually the promoted tuple data constructor '(,) :: k1 -> k2 -> '(k1, k2).
So, you mean that there is no way to fit a (* -> * -> *) or so when a (* -> *) is required? For example, this week I worked on a zipWith ($) version for HList, I have this code: data HApL :: [*] -> [*] -> * where Nil2 :: HApL '[] '[] (:**) :: (a -> b) -> HApL as bs -> HApL (a ': as) (b ': bs) infixr 5 :** zipWithHApL :: HApL xs ys -> HList xs -> HList ys zipWithHApL Nil2 HNil = HNil zipWithHApL (x :** xs) (HCons y ys) = x y `HCons` zipWithHApL xs ys It doesn't satisfy me because: 1. I had to create an ad hoc data-type to manage it, instead of [] deal with it out-of-the-box 2. There no easy way to convert HList to HApL There is no way to get HList closer than List? As for implementing hSplitV, it probably makes sense to start with:
class HSplitAt (n :: HNat) xsys xs ys | n xsys -> xs ys, xs ys -> xsys n where hSplitAt :: Proxy n -> HList xsys -> (HList xs, HList ys)
Then hSplitV can be implemented as
class HSplitV xsys xs ys | xs ys -> xsys
instance (HSplitAt n xsys xs ys, HLength xs ~ n) => HSplitV xsys xs ys where hSplitV = hSplitAt (Proxy :: Proxy n)
You can use type families here, but since "| n xsys -> xs ys, xs ys -> xsys n" stands for four superclass constraints that look like ( (xs ++ ys) ~ xsys ), that option isn't as pretty in my opinion.
Got it, but it requires to have a Length concept:/ No problem, but a little less "magic" Thanks by advance for your answers. Regards.