[Haskell-cafe] Splitting HList

[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).


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.

Regards,
Adam


On Fri, Jun 13, 2014 at 9:03 AM, Gautier DI FOLCO
<gautier.difolco at gmail.com> wrote:
> Hello,
>
> I want to know if it is possible to split a HList?
> I want to have a function like this:
> splitV :: HList (s ++ s') -> (HList s, HList s')
> splitV = _
>
> So I have begun by something which I thought simple:
> type family   HSplit (ts :: [k]) (xs :: [k]) :: ([k], [k])
> type instance HSplit ts xs = ([xs], SndHSplit ts xs)
>
> type family   SndHSplit (ts :: [k]) (xs :: [k]) :: [k]
> type instance SndHSplit ts '[] = ts
> type instance SndHSplit (t ': ts) (x ': xs) = SndHSplit ts xs
>
> But I get the following error:
> H.hs:133:50:
>     The second argument of ‘SndHSplit’ should have kind ‘[k0]’,
>       but ‘xs’ has kind ‘*’
>     In the type ‘([xs], SndHSplit ts xs)’
>     In the type instance declaration for ‘HSplit’
>
> I don't understand why because xs and the first element of the tuple have
> the same kind ([k]).
>
> Thanks by advance for your help/explanations.
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>