{-# LANGUAGE BangPatterns #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- | Heterogeneous lists -- -- Intended for qualified import module Ouroboros.Consensus.Util.HList ( -- * Basic definitions All , HList (..) -- * Folding , collapse , foldMap , foldl , foldlM , foldr , repeatedly , repeatedlyM -- * Singletons , IsList (..) , SList -- * n-ary functions , Fn , afterFn , applyFn ) where import Data.Kind (Constraint, Type) import Data.Proxy import Prelude hiding (foldMap, foldl, foldr) {------------------------------------------------------------------------------- Basic definitions -------------------------------------------------------------------------------} data HList :: [Type] -> Type where Nil :: HList '[] (:*) :: a -> HList as -> HList (a ': as) infixr :* type family All c as :: Constraint where All c '[] = () All c (a ': as) = (c a, All c as) instance All Show as => Show (HList as) where show :: HList as -> String show = [String] -> String forall a. Show a => a -> String show ([String] -> String) -> (HList as -> [String]) -> HList as -> String forall b c a. (b -> c) -> (a -> b) -> a -> c . Proxy Show -> (forall a. Show a => a -> String) -> HList as -> [String] forall (c :: * -> Constraint) (as :: [*]) b (proxy :: (* -> Constraint) -> *). All c as => proxy c -> (forall a. c a => a -> b) -> HList as -> [b] collapse (Proxy Show forall k (t :: k). Proxy t Proxy @Show) forall a. Show a => a -> String show instance (IsList as, All Eq as) => Eq (HList as) where == :: HList as -> HList as -> Bool (==) = SList as -> HList as -> HList as -> Bool forall (bs :: [*]). All Eq bs => SList bs -> HList bs -> HList bs -> Bool eq SList as forall (xs :: [*]). IsList xs => SList xs isList where eq :: All Eq bs => SList bs -> HList bs -> HList bs -> Bool eq :: SList bs -> HList bs -> HList bs -> Bool eq SList bs SNil HList bs _ HList bs _ = Bool True eq (SCons SList as s) (a x :* HList as xs) (a y :* HList as ys) = a x a -> a -> Bool forall a. Eq a => a -> a -> Bool == a a y Bool -> Bool -> Bool && SList as -> HList as -> HList as -> Bool forall (bs :: [*]). All Eq bs => SList bs -> HList bs -> HList bs -> Bool eq SList as s HList as HList as xs HList as HList as ys instance (IsList as, All Eq as, All Ord as) => Ord (HList as) where compare :: HList as -> HList as -> Ordering compare = SList as -> HList as -> HList as -> Ordering forall (bs :: [*]). All Ord bs => SList bs -> HList bs -> HList bs -> Ordering cmp SList as forall (xs :: [*]). IsList xs => SList xs isList where cmp :: All Ord bs => SList bs -> HList bs -> HList bs -> Ordering cmp :: SList bs -> HList bs -> HList bs -> Ordering cmp SList bs SNil HList bs _ HList bs _ = Ordering EQ cmp (SCons SList as s) (a x :* HList as xs) (a y :* HList as ys) = a -> a -> Ordering forall a. Ord a => a -> a -> Ordering compare a x a a y Ordering -> Ordering -> Ordering forall a. Semigroup a => a -> a -> a <> SList as -> HList as -> HList as -> Ordering forall (bs :: [*]). All Ord bs => SList bs -> HList bs -> HList bs -> Ordering cmp SList as s HList as HList as xs HList as HList as ys {------------------------------------------------------------------------------- Folding -------------------------------------------------------------------------------} foldl :: forall c as b proxy. All c as => proxy c -> (forall a. c a => b -> a -> b) -> b -> HList as -> b foldl :: proxy c -> (forall a. c a => b -> a -> b) -> b -> HList as -> b foldl proxy c _ forall a. c a => b -> a -> b f = b -> HList as -> b forall (as' :: [*]). All c as' => b -> HList as' -> b go where go :: All c as' => b -> HList as' -> b go :: b -> HList as' -> b go !b acc HList as' Nil = b acc go !b acc (a a :* HList as as) = b -> HList as -> b forall (as' :: [*]). All c as' => b -> HList as' -> b go (b -> a -> b forall a. c a => b -> a -> b f b acc a a) HList as as foldlM :: forall c as m b proxy. (All c as, Monad m) => proxy c -> (forall a. c a => b -> a -> m b) -> b -> HList as -> m b foldlM :: proxy c -> (forall a. c a => b -> a -> m b) -> b -> HList as -> m b foldlM proxy c _ forall a. c a => b -> a -> m b f = b -> HList as -> m b forall (as' :: [*]). All c as' => b -> HList as' -> m b go where go :: All c as' => b -> HList as' -> m b go :: b -> HList as' -> m b go !b acc HList as' Nil = b -> m b forall (m :: * -> *) a. Monad m => a -> m a return b acc go !b acc (a a :* HList as as) = b -> a -> m b forall a. c a => b -> a -> m b f b acc a a m b -> (b -> m b) -> m b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= \b acc' -> b -> HList as -> m b forall (as' :: [*]). All c as' => b -> HList as' -> m b go b acc' HList as as foldr :: forall c as b proxy. All c as => proxy c -> (forall a. c a => a -> b -> b) -> b -> HList as -> b foldr :: proxy c -> (forall a. c a => a -> b -> b) -> b -> HList as -> b foldr proxy c _ forall a. c a => a -> b -> b f b e = HList as -> b forall (as' :: [*]). All c as' => HList as' -> b go where go :: All c as' => HList as' -> b go :: HList as' -> b go HList as' Nil = b e go (a a :* HList as as) = a -> b -> b forall a. c a => a -> b -> b f a a (HList as -> b forall (as' :: [*]). All c as' => HList as' -> b go HList as as) foldMap :: forall c as b proxy. (All c as, Monoid b) => proxy c -> (forall a. c a => a -> b) -> HList as -> b foldMap :: proxy c -> (forall a. c a => a -> b) -> HList as -> b foldMap proxy c p forall a. c a => a -> b f = proxy c -> (forall a. c a => b -> a -> b) -> b -> HList as -> b forall (c :: * -> Constraint) (as :: [*]) b (proxy :: (* -> Constraint) -> *). All c as => proxy c -> (forall a. c a => b -> a -> b) -> b -> HList as -> b foldl proxy c p (\b b a a -> b b b -> b -> b forall a. Semigroup a => a -> a -> a <> a -> b forall a. c a => a -> b f a a) b forall a. Monoid a => a mempty -- | Apply function repeatedly for all elements of the list -- -- > repeatedly p = flip . foldl p . flip repeatedly :: forall c as b proxy. All c as => proxy c -> (forall a. c a => a -> b -> b) -> (HList as -> b -> b) repeatedly :: proxy c -> (forall a. c a => a -> b -> b) -> HList as -> b -> b repeatedly proxy c p forall a. c a => a -> b -> b f HList as as b e = proxy c -> (forall a. c a => b -> a -> b) -> b -> HList as -> b forall (c :: * -> Constraint) (as :: [*]) b (proxy :: (* -> Constraint) -> *). All c as => proxy c -> (forall a. c a => b -> a -> b) -> b -> HList as -> b foldl proxy c p (\b b a a -> a -> b -> b forall a. c a => a -> b -> b f a a b b) b e HList as as repeatedlyM :: forall c as b proxy m. (Monad m, All c as) => proxy c -> (forall a. c a => a -> b -> m b) -> (HList as -> b -> m b) repeatedlyM :: proxy c -> (forall a. c a => a -> b -> m b) -> HList as -> b -> m b repeatedlyM proxy c p forall a. c a => a -> b -> m b f HList as as b e = proxy c -> (forall a. c a => b -> a -> m b) -> b -> HList as -> m b forall (c :: * -> Constraint) (as :: [*]) (m :: * -> *) b (proxy :: (* -> Constraint) -> *). (All c as, Monad m) => proxy c -> (forall a. c a => b -> a -> m b) -> b -> HList as -> m b foldlM proxy c p (\b b a a -> a -> b -> m b forall a. c a => a -> b -> m b f a a b b) b e HList as as collapse :: forall c as b proxy. All c as => proxy c -> (forall a. c a => a -> b) -> HList as -> [b] collapse :: proxy c -> (forall a. c a => a -> b) -> HList as -> [b] collapse proxy c _ forall a. c a => a -> b f = HList as -> [b] forall (as' :: [*]). All c as' => HList as' -> [b] go where go :: All c as' => HList as' -> [b] go :: HList as' -> [b] go HList as' Nil = [] go (a a :* HList as as) = a -> b forall a. c a => a -> b f a a b -> [b] -> [b] forall a. a -> [a] -> [a] : HList as -> [b] forall (as' :: [*]). All c as' => HList as' -> [b] go HList as as {------------------------------------------------------------------------------- Singleton for HList -------------------------------------------------------------------------------} data SList :: [Type] -> Type where SNil :: SList '[] SCons :: SList as -> SList (a ': as) class IsList (xs :: [Type]) where isList :: SList xs instance IsList '[] where isList :: SList '[] isList = SList '[] SNil instance IsList as => IsList (a ': as) where isList :: SList (a : as) isList = SList as -> SList (a : as) forall (as :: [*]) a. SList as -> SList (a : as) SCons SList as forall (xs :: [*]). IsList xs => SList xs isList {------------------------------------------------------------------------------- n-ary functions -------------------------------------------------------------------------------} type family Fn as b where Fn '[] b = b Fn (a ': as) b = a -> Fn as b withArgs :: HList as -> Fn as b -> b withArgs :: HList as -> Fn as b -> b withArgs HList as Nil Fn as b b = b Fn as b b withArgs (a a :* HList as as) Fn as b f = HList as -> Fn as b -> b forall (as :: [*]) b. HList as -> Fn as b -> b withArgs HList as as (Fn as b a -> Fn as b f a a) applyFn :: Fn as b -> HList as -> b applyFn :: Fn as b -> HList as -> b applyFn = (HList as -> Fn as b -> b) -> Fn as b -> HList as -> b forall a b c. (a -> b -> c) -> b -> a -> c flip HList as -> Fn as b -> b forall (as :: [*]) b. HList as -> Fn as b -> b withArgs afterFn :: SList as -> (b -> c) -> Fn as b -> Fn as c afterFn :: SList as -> (b -> c) -> Fn as b -> Fn as c afterFn SList as SNil b -> c g Fn as b b = b -> c g b Fn as b b afterFn (SCons SList as ss) b -> c g Fn as b f = SList as -> (b -> c) -> Fn as b -> Fn as c forall (as :: [*]) b c. SList as -> (b -> c) -> Fn as b -> Fn as c afterFn SList as ss b -> c g (Fn as b -> Fn as c) -> (a -> Fn as b) -> a -> Fn as c forall b c a. (b -> c) -> (a -> b) -> a -> c . Fn as b a -> Fn as b f