<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">Hi adam,<br><br>Thanks for your answer.<br><br>2014-06-13 19:36 GMT+02:00 adam vogt <span dir="ltr"><<a href="mailto:vogt.adam@gmail.com" target="_blank">vogt.adam@gmail.com</a>></span>:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Gautier,<br>
<br>
It's possible you want:<br>
<br>
type instance HSplit ts xs = '(xs, SndHSplit ts xs)<br>
<br>
[xs] stands for the ordinary list type constructor applied to xs ([]<br>
xs). But ghci can tell you with ":kind []" that [] :: * -> *.<br>
Similarly, (,) in the instance stands for (,) :: * -> * -> *, while<br>
the (,) in ([k], [k]) is actually the promoted tuple data constructor<br>
'(,) :: k1 -> k2 -> '(k1, k2).<br></blockquote><div><br>So, you mean that there is no way to fit a (* -> * -> *) or so when a (* -> *) is required?<br><br>For example, this week I worked on a zipWith ($) version for HList, I have this code:<br>
<div style="margin-left:40px">data HApL :: [*] -> [*] -> * where<br>  Nil2  :: HApL '[] '[]<br>  (:**) :: (a -> b) -> HApL as bs -> HApL (a ': as) (b ': bs)<br><br>infixr 5 :**<br><br>zipWithHApL :: HApL xs ys -> HList xs -> HList ys<br>
zipWithHApL Nil2       HNil      = HNil<br>zipWithHApL (x :** xs) (HCons y ys) = x y `HCons` zipWithHApL xs ys<br></div> <br>It doesn't satisfy me because:<br>  1. I had to create an ad hoc data-type to manage it, instead of [] deal with it out-of-the-box<br>
  2. There no easy way to convert HList to HApL<br><br>There is no way to get HList closer than List?<br><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">

As for implementing hSplitV, it probably makes sense to start with:<br>
<br>
class HSplitAt (n :: HNat) xsys xs ys | n xsys -> xs ys, xs ys -> xsys n<br>
  where hSplitAt :: Proxy n -> HList xsys -> (HList xs, HList ys)<br>
<br>
Then hSplitV can be implemented as<br>
<br>
class HSplitV xsys xs ys | xs ys -> xsys<br>
<br>
instance (HSplitAt n xsys xs ys,<br>
          HLength xs ~ n) =><br>
   HSplitV xsys xs ys<br>
 where hSplitV = hSplitAt (Proxy :: Proxy n)<br>
<br>
<br>
You can use type families here, but since "| n xsys -> xs ys, xs ys -><br>
xsys n" stands for four superclass constraints that look like ( (xs ++<br>
ys) ~ xsys ), that option isn't as pretty in my opinion.<br></blockquote></div><br>Got it, but it requires to have a Length concept:/<br>No problem, but a little less "magic"<br><br>Thanks by advance for your answers.<br>
<br></div><div class="gmail_extra">Regards.<br></div></div>