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)
:.)