Hi adam,

Thanks for your answer.

2014-06-13 19:36 GMT+02:00 adam vogt <vogt.adam@gmail.com>:

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.