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.
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
Hi adam,
Thanks for your answer.
2014-06-13 19:36 GMT+02:00 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).
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.
Hi Gautier,
So, you mean that there is no way to fit a (* -> * -> *) or so when a (* -> *) is required?
No.If you decide on a kind signature ([k], [k]), you have to use '(,) not (,) when making types for that kind. Similarly if you have a type [xs], the kind of that is * which doesn't match the kind [k] you specify.
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?
I'm not sure. With the HList library on hackage, you can do the equivalent of zipWithDollar xs ys = map ($) (zip xs ys) by defining: data Dollar = Dollar instance (fx ~ (x -> y, x)) => ApplyAB Dollar fx y where applyAB _ (f,x) = f x hZipWithDollar xs ys = hMap Dollar (hZip xs ys) It works like:
hZipWithDollar (hBuild (+1) tail) (hBuild 3 "ab") H[4, "b"]
But in more complicated cases there is a tendency to need -XAllowAmbiguousTypes, which means writing type signatures (with -XScopedTypeVariables) that should be unnecessary. Regards, Adam
Hi adam,
Thanks for your answer.
2014-06-13 21:44 GMT+02:00 adam vogt
No.If you decide on a kind signature ([k], [k]), you have to use '(,) not (,) when making types for that kind. Similarly if you have a type [xs], the kind of that is * which doesn't match the kind [k] you specify.
ok, I was confused, thanks.
I'm not sure. With the HList library on hackage, you can do the equivalent of
zipWithDollar xs ys = map ($) (zip xs ys)
by defining:
data Dollar = Dollar instance (fx ~ (x -> y, x)) => ApplyAB Dollar fx y where applyAB _ (f,x) = f x
hZipWithDollar xs ys = hMap Dollar (hZip xs ys)
It works like:
hZipWithDollar (hBuild (+1) tail) (hBuild 3 "ab") H[4, "b"]
But in more complicated cases there is a tendency to need -XAllowAmbiguousTypes, which means writing type signatures (with -XScopedTypeVariables) that should be unnecessary.
ok, that's clear, thanks. Regards.
participants (2)
-
adam vogt -
Gautier DI FOLCO