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
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe