I'm trying to fold a data with a phantom type of kind [*]. Here is simplified version of my code
{-# LANGUAGE DataKinds, KindSignatures #-}
module Stack where
import Data.HList
import Data.Foldable as F
data T (a :: [*]) = T (Tagged a String)
(!++!) :: T a -> T b -> T (HAppendList a b)
(T a) !++! (T b) = T (Tagged (untag a ++ untag b))
a = T (Tagged "1") :: T '[Int]
b = T (Tagged "-- ") :: T '[]
ab = a !++! b :: T '[Int]
I would like a fold operator
(!++*) :: (Foldable t ) => T a -> t (T '[]) -> T a
a !++* t = F.foldl (!++!) a t
But that doesn't work. The compiler that a
and HAppendList a '[]
are different, even though they are not.
Why can't the compile unify HAppendList a '[]
and a
?
(I can't do the fold manually in ghci though :t a !++! b !++! b !++! b => T '[Int]
Note the definition of HAppendList
:
type family HAppendList (l1 :: [k]) (l2 :: [k]) :: [k]
type instance HAppendList '[] l = l
type instance HAppendList (e ': l) l' = e ': HAppendList l l'
You and I know that []
is the left and right identity of ++
, but the compiler is only aware of the left identity:
happend' :: T a -> T b -> T (HAppendList a b)
happend' (T (Tagged a)) (T (Tagged b)) = (T (Tagged (a++b)))
-- Doesn't typecheck
leftIdentity' :: T a -> T '[] -> T a
leftIdentity' x y = happend' x y
rightIdentity' :: T '[] -> T a -> T a
rightIdentity' x y = happend' x y
You would need to have
type instance HAppendList '[] l = l
type instance HAppendList l '[] = l
type instance HAppendList (e ': l) l' = e ': HAppendList l l'
to have the compiler know about left and right identity; but these would be overlapping, so it doesn't type check. You can just flip the arguements, however:
(!+++!) :: T a -> T b -> T (HAppendList a b)
(!+++!) (T (Tagged x)) (T (Tagged y)) = T (Tagged (y ++ x))
(!++*) :: Foldable t => T a -> t (T '[]) -> T a
a !++* t = F.foldl (flip (!+++!)) a t
With closed type families introduced in ghc 7.8, you can fix this problem:
type family (++) (a :: [k]) (b :: [k]) :: [k] where
'[] ++ x = x
x ++ '[] = x
(x ': xs) ++ ys = x ': (xs ++ ys)
happend :: T a -> T b -> T (a ++ b)
happend (T (Tagged a)) (T (Tagged b)) = (T (Tagged (a++b)))
leftIdentity :: T a -> T '[] -> T a
leftIdentity x y = happend x y
rightIdentity :: T '[] -> T a -> T a
rightIdentity x y = happend x y