This commit is contained in:
George Thomas 2026-01-04 02:40:52 +00:00
parent c4b85eac71
commit 2180af71ad

View File

@ -146,12 +146,10 @@ data HListF (f :: Type -> Type) (as :: List Type) :: Type where
f a -> f a ->
HListF f as -> HListF f as ->
HListF f (a ': as) HListF f (a ': as)
foldHListF :: (forall x xs. f x -> r xs -> r (x ': xs)) -> r '[] -> HListF f as -> r as foldHListF :: (forall x xs. f x -> r xs -> r (x ': xs)) -> r '[] -> HListF f as -> r as
foldHListF f e = \case foldHListF f e = \case
HNilF -> e HNilF -> e
HConsF x xs -> f x $ foldHListF f e xs HConsF x xs -> f x $ foldHListF f e xs
mapHListF :: (forall a. f a -> g a) -> HListF f as -> HListF g as mapHListF :: (forall a. f a -> g a) -> HListF f as -> HListF g as
mapHListF t = foldHListF (\x r -> HConsF (t x) $ r) HNilF mapHListF t = foldHListF (\x r -> HConsF (t x) $ r) HNilF