Remove heterogenous list length function

This commit is contained in:
George Thomas 2026-01-05 15:19:18 +00:00
parent 7bacf5efc4
commit 24a21e3807
2 changed files with 1 additions and 11 deletions

View File

@ -47,7 +47,7 @@ main =
mapHListF (\(Fanout (f, Op o)) -> (o &&& id) $ f input) parts mapHListF (\(Fanout (f, Op o)) -> (o &&& id) $ f input) parts
in pure (input, rs, os) in pure (input, rs, os)
) )
$ ( flip map ([0 :: Int .. hlistfLength parts - 1]) $ $ ( flip map ([0 :: Int .. foldHListF0 (const succ) 0 parts - 1]) $
\n@(show . succ -> nt) -> \n@(show . succ -> nt) ->
TestTree TestTree
(mkTestName nt) (mkTestName nt)

View File

@ -40,12 +40,10 @@ module Pre (
adjacentPairs, adjacentPairs,
sortPair, sortPair,
HList (..), HList (..),
hlistLength,
HListF (..), HListF (..),
foldHListF, foldHListF,
foldHListF0, foldHListF0,
mapHListF, mapHListF,
hlistfLength,
(/\), (/\),
(/\\), (/\\),
nil, nil,
@ -160,10 +158,6 @@ data HList (as :: List Type) :: Type where
a -> a ->
HList as -> HList as ->
HList (a ': as) HList (a ': as)
hlistLength :: HList r -> Int
hlistLength = \case
HNil -> 0
HCons _ l -> 1 + hlistLength l
data HListF (f :: Type -> Type) (as :: List Type) :: Type where data HListF (f :: Type -> Type) (as :: List Type) :: Type where
HNilF :: HListF f '[] HNilF :: HListF f '[]
@ -181,10 +175,6 @@ foldHListF0 f e = \case
HConsF x xs -> f x $ foldHListF0 f e xs HConsF x xs -> f x $ foldHListF0 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
hlistfLength :: HListF f r -> Int
hlistfLength = \case
HNilF -> 0
HConsF _ l -> 1 + hlistfLength l
newtype Fanout f g a = Fanout (f a, g a) newtype Fanout f g a = Fanout (f a, g a)