[Haskell-cafe] Splitting HList
vogt.adam at gmail.com
Fri Jun 13 17:36:07 UTC 2014
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.
On Fri, Jun 13, 2014 at 9:03 AM, Gautier DI FOLCO
<gautier.difolco at gmail.com> wrote:
> 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:
> 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
More information about the Haskell-Cafe