module Data.HList where import Prelude hiding (curry, uncurry) infixr 5 :. data List as where Nil :: List '[] (:.) :: a -> List as -> List (a ': as) instance Eq (List '[]) where Nil == :: List '[] -> List '[] -> Bool == Nil = Bool True instance (Eq a, Eq (List as)) => Eq (List (a ': as)) where x :: a x:.xs :: List as xs == :: List (a : as) -> List (a : as) -> Bool == y :: a y:.ys :: List as ys = a x a -> a -> Bool forall a. Eq a => a -> a -> Bool == a a y Bool -> Bool -> Bool && List as xs List as -> List as -> Bool forall a. Eq a => a -> a -> Bool == List as List as ys instance Ord (List '[]) where Nil compare :: List '[] -> List '[] -> Ordering `compare` Nil = Ordering EQ instance (Ord a, Ord (List as)) => Ord (List (a ': as)) where (x :: a x:.xs :: List as xs) compare :: List (a : as) -> List (a : as) -> Ordering `compare` (y :: a y:.ys :: List as ys) = a x a -> a -> Ordering forall a. Ord a => a -> a -> Ordering `compare` a a y Ordering -> Ordering -> Ordering forall a. Semigroup a => a -> a -> a <> List as xs List as -> List as -> Ordering forall a. Ord a => a -> a -> Ordering `compare` List as List as ys type family Foldr f z xs where Foldr f z '[] = z Foldr f z (x ': xs) = f x (Foldr f z xs) class Curry as where uncurry :: Foldr (->) b as -> List as -> b curry :: (List as -> b) -> Foldr (->) b as instance Curry '[] where uncurry :: Foldr (->) b '[] -> List '[] -> b uncurry f :: Foldr (->) b '[] f _ = b Foldr (->) b '[] f curry :: (List '[] -> b) -> Foldr (->) b '[] curry f :: List '[] -> b f = List '[] -> b f List '[] Nil instance Curry as => Curry (a ': as) where uncurry :: Foldr (->) b (a : as) -> List (a : as) -> b uncurry f :: Foldr (->) b (a : as) f (x :: a x:.xs :: List as xs) = Foldr (->) b as -> List as -> b forall (as :: [*]) b. Curry as => Foldr (->) b as -> List as -> b uncurry (Foldr (->) b (a : as) a -> Foldr (->) b as f a x) List as xs curry :: (List (a : as) -> b) -> Foldr (->) b (a : as) curry f :: List (a : as) -> b f x :: a x = (List as -> b) -> Foldr (->) b as forall (as :: [*]) b. Curry as => (List as -> b) -> Foldr (->) b as curry ((List as -> b) -> Foldr (->) b as) -> (List as -> b) -> Foldr (->) b as forall a b. (a -> b) -> a -> b $ List (a : as) -> b f (List (a : as) -> b) -> (List as -> List (a : as)) -> List as -> b forall b c a. (b -> c) -> (a -> b) -> a -> c . (a xa -> List as -> List (a : as) forall a (as :: [*]). a -> List as -> List (a : as) :.)