{- |
   The HList library

   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke

   Basic declarations for typeful heterogeneous lists.

 -}

module Data.HList.HList where

import Data.HList.FakePrelude
import Data.HList.HListPrelude

import Text.ParserCombinators.ReadP
import Data.List

import LensDefs

import Data.Array (Ix)
import Data.Semigroup

-- --------------------------------------------------------------------------
-- * Heterogeneous type sequences
{- $note

There are three sensible ways to define HLists:

@
data HList (l::[*]) where
    HNil  :: HList '[]
    HCons :: e -> HList l -> HList (e ': l)
@

This ensures that sequences can only be formed with Nil
and Cons. The argument to HList is a promoted lists (kind @[*]@),
which has a more attractive syntax.


Earlier versions of HList used an algebraic data type:

@
data HCons a b = HCons a b
data HNil = HNil
@

Disadvantages:

* values with types like @HCons Int Double@ to be created,
  which are nonsense to the functions in HList

* some recursive functions do not need a class with the GADT. For example:

  @
    hInit :: HListGADT (x ': xs) -> HListGADT (HInit (x ': xs))
    hInit (HCons x xs@(HCons _ _)) = HCons x (hInit xs)
    hInit (HCons _ HNil) = HNil

    type family HInit (xs :: [k]) :: [k]
  @

  but without the GADT, 'hInit' is written as in a class,
  which complicates inferred types


Advantages

* lazy pattern matches are allowed, so lazy pattern matching
  on a value @undefined :: HList [a,b,c]@ can create the
  spine of the list. 'hProxies' avoids the use of 'undefined',
  but a slightly more complicated class context has to be written
  or inferred.

* type inference is better if you want to directly pattern match
<http://stackoverflow.com/questions/19077037/is-there-any-deeper-type-theoretic-reason-ghc-cant-infer-this-type see stackoverflow post here>

* better pattern exhaustiveness checking (as of ghc-7.8)

* standalone deriving works

* Data.Coerce.coerce works because the parameters have role representational,
  not nominal as they are for the GADT and data family. Probably the GADT/type
  family actually do have a representational role:
  <http://stackoverflow.com/questions/24222552/does-this-gadt-actually-have-type-role-representational>



The data family version (currently used) gives the same type constructor
@HList :: [*] -> *@ as the GADT, while pattern matching behaves
like the algebraic data type. Furthermore, nonsense values like
@HCons 1 2 :: HCons Int Int@ cannot be written with the data family.

A variation on the data family version is

> data instance HList '[] = HNil
> newtype instance HList (x ': xs) = HCons1 (x, HList xs)
> pattern HCons x xs = HCons1 (x, xs)

This allows HList to have a nominal role, but on the other
hand the PatternSynonym is not supported with ghc-7.6 and
exhaustiveness checking is not as good (warnings for _ being
unmatched)

-}


data family HList (l::[*])

data instance HList '[] = HNil
data instance HList (x ': xs) = x `HCons` HList xs

deriving instance Eq (HList '[])
deriving instance (Eq x, Eq (HList xs)) => Eq (HList (x ': xs))

deriving instance Ord (HList '[])
deriving instance (Ord x, Ord (HList xs)) => Ord (HList (x ': xs))

deriving instance Ix (HList '[])
deriving instance (Ix x, Ix (HList xs)) => Ix (HList (x ': xs))

deriving instance Bounded (HList '[])
deriving instance (Bounded x, Bounded (HList xs)) => Bounded (HList (x ': xs))


-- Enum cannot be derived


-- | creates a HList of Proxies

class HProxiesFD (xs :: [*]) pxs | pxs -> xs -- DropProxy pxs ~ xs
                      , xs -> pxs -- AddProxy xs ~ pxs
      where hProxies :: HList pxs

{- Ideally we could write:

> class DropProxy (AddProxy xs) ~ xs => HProxies xs where
>     hProxies :: HList (AddProxy xs)

See https://ghc.haskell.org/trac/ghc/ticket/10009 -}
type HProxies xs = HProxiesFD xs (AddProxy xs)


{- | Add 'Proxy' to a type

>>> let x = undefined :: HList (AddProxy [Char,Int])
>>> :t x
x :: HList '[Proxy Char, Proxy Int]


-}
type family AddProxy (xs :: k) :: k
type instance AddProxy '[] = '[]
type instance AddProxy (x ': xs) = AddProxy x ': AddProxy xs
type instance AddProxy (x :: *) = Proxy x

-- | inverse of 'AddProxy'
type family DropProxy (xs :: k) :: k
type instance DropProxy (x ': xs) = DropProxy x ': DropProxy xs
type instance DropProxy '[] = '[]
type instance DropProxy (Proxy x) = x

instance HProxiesFD '[] '[] where
    hProxies :: HList '[]
hProxies = HList '[]
HNil

instance (HProxiesFD xs pxs) => HProxiesFD (x ': xs) (Proxy x ': pxs) where
    hProxies :: HList (Proxy x : pxs)
hProxies = forall {k} (t :: k). Proxy t
Proxy forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall (xs :: [*]) (pxs :: [*]). HProxiesFD xs pxs => HList pxs
hProxies



instance Show (HList '[]) where
    show :: HList '[] -> String
show HList '[]
_ = String
"H[]"

instance (Show e, Show (HList l)) => Show (HList (e ': l)) where
    show :: HList (e : l) -> String
show (HCons e
x HList l
l) = let Char
'H':Char
'[':String
s = forall a. Show a => a -> String
show HList l
l
                       in String
"H[" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show e
x forall a. [a] -> [a] -> [a]
++
                                  (if String
s forall a. Eq a => a -> a -> Bool
== String
"]" then String
s else String
"," forall a. [a] -> [a] -> [a]
++ String
s)


instance Read (HList '[]) where
    readsPrec :: Int -> ReadS (HList '[])
readsPrec Int
_ String
str = case forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
"H[]" String
str of
                        Maybe String
Nothing -> []
                        Just String
rest -> [(HList '[]
HNil, String
rest)]

instance
   (HProxies l, Read e,
    HSequence ReadP (ReadP e ': readP_l) (e ': l),
    HMapCxt HList ReadElement (AddProxy l) readP_l)  =>
      Read (HList (e ': l)) where
  readsPrec :: Int -> ReadS (HList (e : l))
readsPrec Int
_ = forall a. ReadP a -> ReadS a
readP_to_S forall a b. (a -> b) -> a -> b
$ do
    String
_ <- String -> ReadP String
string String
"H["
    HList (AddProxy l)
l <- forall (m :: * -> *) a. Monad m => a -> m a
return (forall (xs :: [*]) (pxs :: [*]). HProxiesFD xs pxs => HList pxs
hProxies :: HList (AddProxy l))
    let parsers :: HList (ReadP e : readP_l)
parsers = forall a. ReadS a -> ReadP a
readS_to_P forall a. Read a => ReadS a
reads forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {f}.
(SameLength' a b, SameLength' b a, HMapAux r f a b) =>
f -> r a -> r b
hMap ReadElement
ReadElement HList (AddProxy l)
l
    HList (e : l)
hlist <- forall (m :: * -> *) (a :: [*]) (b :: [*]).
HSequence m a b =>
HList a -> m (HList b)
hSequence HList (ReadP e : readP_l)
parsers
    String
_ <- String -> ReadP String
string String
"]"
    forall (m :: * -> *) a. Monad m => a -> m a
return HList (e : l)
hlist


-- similar to ReadComponent used to define instance Read Record
data ReadElement = ReadElement

instance (y ~ ReadP x, Read x) => ApplyAB ReadElement (Proxy x) y where
    applyAB :: ReadElement -> Proxy x -> y
applyAB ReadElement
ReadElement Proxy x
_ = do
      String
_ <- String -> ReadP String
string String
","
      forall a. ReadS a -> ReadP a
readS_to_P forall a. Read a => ReadS a
reads


infixr 2 `HCons`


-- --------------------------------------------------------------------------
-- * Basic list functions

-- | 'head'
hHead :: HList (e ': l) -> e
hHead :: forall e (l :: [*]). HList (e : l) -> e
hHead (HCons e
x HList l
_) = e
x

-- | 'tail'
hTail :: HList (e ': l) -> HList l
hTail :: forall e (l :: [*]). HList (e : l) -> HList l
hTail (HCons e
_ HList l
l) = HList l
l

-- | 'last'
hLast :: HList l1 -> e
hLast HList l1
xs = forall e (l :: [*]). HList (e : l) -> e
hHead (forall {l1 :: [*]} {l3 :: [*]}.
HRevApp l1 '[] l3 =>
HList l1 -> HList l3
hReverse_ HList l1
xs)


class HInit xs where
    type HInitR xs :: [*]
    hInit :: HList xs -> HList (HInitR xs)

instance HInit '[x] where
    type HInitR '[x] = '[]
    hInit :: HList '[x] -> HList (HInitR '[x])
hInit HList '[x]
_ = HList '[]
HNil

instance HInit (b ': c) => HInit (a ': b ': c) where
    type HInitR (a ': b ': c) = a ': HInitR (b ': c)
    hInit :: HList (a : b : c) -> HList (HInitR (a : b : c))
hInit (a
a `HCons` HList (b : c)
bc) = a
a forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall (xs :: [*]). HInit xs => HList xs -> HList (HInitR xs)
hInit HList (b : c)
bc


-- | Length, but see 'HLengthEq' instead
type family HLength (x :: [k]) :: HNat
type instance HLength '[] = HZero
type instance HLength (x ': xs) = HSucc (HLength xs)

hLength   :: HLengthEq l n => HList l -> Proxy n
hLength :: forall (l :: [*]) (n :: HNat). HLengthEq l n => HList l -> Proxy n
hLength HList l
_ =  forall {k} (t :: k). Proxy t
Proxy

-- ** Append
instance HExtend e (HList l) where
  type HExtendR e (HList l) = HList (e ': l)
  .*. :: e -> HList l -> HExtendR e (HList l)
(.*.) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons

instance HAppendList l1 l2 => HAppend (HList l1) (HList l2) where
  hAppend :: HList l1 -> HList l2 -> HAppendR (HList l1) (HList l2)
hAppend = forall (l1 :: [*]) (l2 :: [*]).
HAppendList l1 l2 =>
HList l1 -> HList l2 -> HList (HAppendListR l1 l2)
hAppendList
type instance HAppendR (HList l1) (HList l2) = HList (HAppendListR l1 l2)

type family HAppendListR (l1 :: [k]) (l2 :: [k]) :: [k]
type instance HAppendListR '[] l = l
type instance HAppendListR (e ': l) l' = e ': HAppendListR l l'


class HAppendList l1 l2 where
  -- | the same as 'hAppend'
  hAppendList :: HList l1 -> HList l2 -> HList (HAppendListR l1 l2)

instance HAppendList '[] l2 where
  hAppendList :: HList '[] -> HList l2 -> HList (HAppendListR '[] l2)
hAppendList HList '[]
R:HList[]
HNil HList l2
l = HList l2
l

instance HAppendList l l' => HAppendList (x ': l) l' where
  hAppendList :: HList (x : l) -> HList l' -> HList (HAppendListR (x : l) l')
hAppendList (HCons x
x HList l
l) HList l'
l' = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons x
x (forall (l1 :: [*]) (l2 :: [*]).
HAppendList l1 l2 =>
HList l1 -> HList l2 -> HList (HAppendListR l1 l2)
hAppendList HList l
l HList l'
l')

-- --------------------------------------------------------------------------

-- ** Alternative append


-- | 'hAppend'' below is implemented using the same idea
append' :: [a] -> [a] -> [a]
append' :: forall a. [a] -> [a] -> [a]
append' [a]
l [a]
l' = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (:) [a]
l' [a]
l

-- | Alternative implementation of 'hAppend'. Demonstrates 'HFoldr'
hAppend' :: (HFoldr FHCons v l r) => HList l -> v -> r
hAppend' :: forall v (l :: [*]) r. HFoldr FHCons v l r => HList l -> v -> r
hAppend' HList l
l v
l' = forall f v (l :: [*]) r. HFoldr f v l r => f -> v -> HList l -> r
hFoldr FHCons
FHCons v
l' HList l
l

data FHCons = FHCons

instance ( x ~ (e,HList l), y ~ (HList (e ': l))) => ApplyAB FHCons x y  where
    applyAB :: FHCons -> x -> y
applyAB FHCons
_ (e
e,HList l
l) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e HList l
l


-- ** Historical append

{- $

The original HList code is included below. In both cases
we had to program the algorithm twice, at the term and the type levels.

[@The class HAppend@]

> class HAppend l l' l'' | l l' -> l''
>  where
>   hAppend :: l -> l' -> l''
>

[@The instance following the normal append@]

> instance HList l => HAppend HNil l l
>  where
>   hAppend HNil l = l
>
> instance (HList l, HAppend l l' l'')
>       => HAppend (HCons x l) l' (HCons x l'')
>  where
>   hAppend (HCons x l) l' = HCons x (hAppend l l')

-}

-- --------------------------------------------------------------------------
-- * Reversing HLists

-- Append the reversed l1 to l2
type family HRevAppR (l1 :: [k]) (l2 :: [k]) :: [k]
type instance HRevAppR '[] l = l
type instance HRevAppR (e ': l) l' = HRevAppR l (e ': l')


class HRevApp l1 l2 l3 | l1 l2 -> l3 where
    hRevApp :: HList l1 -> HList l2 -> HList l3

instance HRevApp '[] l2 l2 where
    hRevApp :: HList '[] -> HList l2 -> HList l2
hRevApp HList '[]
_ HList l2
l = HList l2
l

instance HRevApp l (x ': l') z => HRevApp (x ': l) l' z where
    hRevApp :: HList (x : l) -> HList l' -> HList z
hRevApp (HCons x
x HList l
l) HList l'
l' = forall (l1 :: [*]) (l2 :: [*]) (l3 :: [*]).
HRevApp l1 l2 l3 =>
HList l1 -> HList l2 -> HList l3
hRevApp HList l
l (forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons x
x HList l'
l')



class HReverse xs sx | xs -> sx, sx -> xs where
    hReverse :: HList xs -> HList sx

instance (HRevApp xs '[] sx,
          HRevApp sx '[] xs) => HReverse xs sx where
    hReverse :: HList xs -> HList sx
hReverse HList xs
l = forall (l1 :: [*]) (l2 :: [*]) (l3 :: [*]).
HRevApp l1 l2 l3 =>
HList l1 -> HList l2 -> HList l3
hRevApp HList xs
l HList '[]
HNil

-- | a version of 'hReverse' that does not allow the type
-- information to flow backwards
hReverse_ :: HList l1 -> HList l3
hReverse_ HList l1
l = forall (l1 :: [*]) (l2 :: [*]) (l3 :: [*]).
HRevApp l1 l2 l3 =>
HList l1 -> HList l2 -> HList l3
hRevApp HList l1
l HList '[]
HNil

-- --------------------------------------------------------------------------

--
-- * A nicer notation for lists
--


-- | List termination
hEnd :: HList l -> HList l
hEnd :: forall (l :: [*]). HList l -> HList l
hEnd = forall a. a -> a
id

{- ^
   Note:

        [@x :: HList a@] means: @forall a. x :: HList a@

        [@hEnd x@] means: @exists a. x :: HList a@
-}


-- |  Building lists

hBuild :: (HBuild' '[] r) => r
hBuild :: forall r. HBuild' '[] r => r
hBuild =  forall (l :: [*]) r. HBuild' l r => HList l -> r
hBuild' HList '[]
HNil

class HBuild' l r where
    hBuild' :: HList l -> r

instance HReverse l l'
      => HBuild' l (HList l') where
  hBuild' :: HList l -> HList l'
hBuild' HList l
l = forall (l :: [*]) (l' :: [*]). HReverse l l' => HList l -> HList l'
hReverse HList l
l

instance HBuild' (a ': l) r
      => HBuild' l (a->r) where
  hBuild' :: HList l -> a -> r
hBuild' HList l
l a
x = forall (l :: [*]) r. HBuild' l r => HList l -> r
hBuild' (forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons a
x HList l
l)

-- ** examples
{- $examplesNote

The classes above allow the third (shortest) way to make a list
(containing a,b,c) in this case

> list = a `HCons` b `HCons` c `HCons` HNil
> list = a .*. b .*. c .*. HNil
> list = hEnd $ hBuild a b c

>>> let x = hBuild True in hEnd x
H[True]

>>> let x = hBuild True 'a' in hEnd x
H[True,'a']

>>> let x = hBuild True 'a' "ok" in hEnd x
H[True,'a',"ok"]

hBuild can also produce a Record, such that

> hBuild x y ^. from unlabeled

can also be produced using

@
'hEndR' $ hBuild x y
@

-}

-- *** historical
{- $hbuild the show instance has since changed, but these uses of
'hBuild'/'hEnd' still work

> HList> let x = hBuild True in hEnd x
> HCons True HNil

> HList> let x = hBuild True 'a' in hEnd x
> HCons True (HCons 'a' HNil)

> HList> let x = hBuild True 'a' "ok" in hEnd x
> HCons True (HCons 'a' (HCons "ok" HNil))

> HList> hEnd (hBuild (Key 42) (Name "Angus") Cow (Price 75.5))
> HCons (Key 42) (HCons (Name "Angus") (HCons Cow (HCons (Price 75.5) HNil)))

> HList> hEnd (hBuild (Key 42) (Name "Angus") Cow (Price 75.5)) == angus
> True

-}

-- --------------------------------------------------------------------------

-- * folds
-- ** foldr
-- $foldNote  Consume a heterogenous list.


class HFoldr f v (l :: [*]) r where
    hFoldr :: f -> v -> HList l -> r

instance (v ~ v') => HFoldr f v '[] v' where
    hFoldr :: f -> v -> HList '[] -> v'
hFoldr       f
_ v
v HList '[]
_   = v
v

-- | uses 'ApplyAB' not 'Apply'
instance (ApplyAB f (e, r) r', HFoldr f v l r)
    => HFoldr f v (e ': l) r' where
    hFoldr :: f -> v -> HList (e : l) -> r'
hFoldr f
f v
v (HCons e
x HList l
l)    = forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f (e
x, forall f v (l :: [*]) r. HFoldr f v l r => f -> v -> HList l -> r
hFoldr f
f v
v HList l
l :: r)


class HScanr f z ls rs where
    hScanr :: f -> z -> HList ls -> HList rs

instance lz ~ '[z] => HScanr f z '[] lz where
    hScanr :: f -> z -> HList '[] -> HList lz
hScanr f
_ z
z HList '[]
_ = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons z
z HList '[]
HNil

instance (ApplyAB f (x,r) s, HScanr f z xs (r ': rs),
          srrs ~ (s ': r ': rs)) => HScanr f z (x ': xs) srrs where
    hScanr :: f -> z -> HList (x : xs) -> HList srrs
hScanr f
f z
z (HCons x
x HList xs
xs) =
        case forall f z (ls :: [*]) (rs :: [*]).
HScanr f z ls rs =>
f -> z -> HList ls -> HList rs
hScanr f
f z
z HList xs
xs :: HList (r ': rs) of
            HCons r
r HList rs
rs -> (forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f (x
x,r
r) :: s) forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` r
r forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList rs
rs

class HFoldr1 f (l :: [*]) r where
    hFoldr1 :: f -> HList l -> r

instance (v ~ v') => HFoldr1 f '[v] v' where
    hFoldr1 :: f -> HList '[v] -> v'
hFoldr1      f
_ (HCons v
v HList '[]
_)  = v
v

-- | uses 'ApplyAB' not 'Apply'
instance (ApplyAB f (e, r) r', HFoldr1 f (e' ': l) r)
    => HFoldr1 f (e ': e' ': l) r' where
    hFoldr1 :: f -> HList (e : e' : l) -> r'
hFoldr1 f
f (HCons e
x HList (e' : l)
l)    = forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f (e
x, forall f (l :: [*]) r. HFoldr1 f l r => f -> HList l -> r
hFoldr1 f
f HList (e' : l)
l :: r)


-- ** foldl

{- | like 'foldl'


>>> hFoldl (uncurry $ flip (:)) [] (1 `HCons` 2 `HCons` HNil)
[2,1]


-}
class HFoldl f (z :: *) xs (r :: *) where
    hFoldl :: f -> z -> HList xs -> r

instance (zx ~ (z,x), ApplyAB f zx z', HFoldl f z' xs r)
    => HFoldl f z (x ': xs) r where
    hFoldl :: f -> z -> HList (x : xs) -> r
hFoldl f
f z
z (x
x `HCons` HList xs
xs) = forall f z (xs :: [*]) r.
HFoldl f z xs r =>
f -> z -> HList xs -> r
hFoldl f
f (forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f (z
z,x
x) :: z') HList xs
xs

instance (z ~ z') => HFoldl f z '[] z' where
    hFoldl :: f -> z -> HList '[] -> z'
hFoldl f
_ z
z HList '[]
_ = z
z





-- * unfolds

-- ** unfold
-- $unfoldNote Produce a heterogenous list. Uses the more limited
-- 'Apply' instead of 'App' since that's all that is needed for uses of this
-- function downstream. Those could in principle be re-written.

-- hUnfold :: (Apply p s, HUnfold' p s) => p -> s -> HList (HUnfold p s)
hUnfold :: f -> a -> HList z
hUnfold f
p a
s = forall p res (z :: [*]). HUnfoldFD p res z => p -> res -> HList z
hUnfold' f
p (forall f a. Apply f a => f -> a -> ApplyR f a
apply f
p a
s)

type HUnfold p s = HUnfoldR p (ApplyR p s)

type family HUnfoldR p res :: [*]
type instance HUnfoldR p HNothing = '[]
type instance HUnfoldR p (HJust (e,s)) = e ': HUnfoldR p (ApplyR p s)

type HUnfold' p res = HUnfoldFD p (ApplyR p res) (HUnfold p res)

class HUnfoldFD p res z | p res -> z where
    hUnfold' :: p -> res -> HList z

instance HUnfoldFD p HNothing '[] where
    hUnfold' :: p -> HNothing -> HList '[]
hUnfold' p
_ HNothing
_ = HList '[]
HNil

instance (Apply p s, HUnfoldFD p (ApplyR p s) z) => HUnfoldFD p (HJust (e,s)) (e ': z) where
    hUnfold' :: p -> HJust (e, s) -> HList (e : z)
hUnfold' p
p (HJust (e
e,s
s)) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e (forall {f} {a} {z :: [*]}.
(HUnfoldFD f (ApplyR f a) z, Apply f a) =>
f -> a -> HList z
hUnfold p
p s
s)


-- ** replicate

{- |

Sometimes the result type can fix the type of the
first argument:

>>> hReplicate Proxy () :: HList '[ (), (), () ]
H[(),(),()]

However, with HReplicate all elements must have the same type, so it may be
easier to use 'HList2List':

>>> list2HList (repeat 3) :: Maybe (HList [Int, Int, Int])
Just H[3,3,3]

-}
class HLengthEq es n => HReplicateFD (n :: HNat) e es
          | n e -> es, es -> n where
    hReplicate :: Proxy n -> e -> HList es

instance HReplicateFD HZero e '[] where
    hReplicate :: Proxy 'HZero -> e -> HList '[]
hReplicate Proxy 'HZero
_ e
_ = HList '[]
HNil

instance (HReplicateFD n e es, e ~ e') => HReplicateFD (HSucc n) e (e' ': es) where
    hReplicate :: Proxy ('HSucc n) -> e -> HList (e' : es)
hReplicate Proxy ('HSucc n)
n e
e = e
e forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall (n :: HNat) e (es :: [*]).
HReplicateFD n e es =>
Proxy n -> e -> HList es
hReplicate (forall (n :: HNat). Proxy ('HSucc n) -> Proxy n
hPred Proxy ('HSucc n)
n) e
e

type HReplicate n e = HReplicateFD n e (HReplicateR n e)

-- | would be associated with 'HReplicate' except we want
-- it to work with `e` of any kind, not just `*` that you can
-- put into a HList. An \"inverse\" of 'HLength'
type family HReplicateR (n :: HNat) (e :: k) :: [k]
type instance HReplicateR HZero e = '[]
type instance HReplicateR (HSucc n) e = e ': HReplicateR n e

{- | HReplicate produces lists that can be converted to ordinary
lists

>>> let two = hSucc (hSucc hZero)
>>> let f = Fun' fromInteger :: Fun' Num Integer

>>> :t applyAB f
applyAB f :: Num b => Integer -> b

>>> hReplicateF two f 3
H[3,3]

>>> hReplicateF Proxy f 3 :: HList [Int, Double, Integer]
H[3,3.0,3]

-}
class HLengthEq r n => HReplicateF (n :: HNat) f z r | r -> n where
    hReplicateF :: HLengthEq r n => Proxy n -> f -> z -> HList r

instance HReplicateF HZero f z '[] where
    hReplicateF :: HLengthEq '[] 'HZero => Proxy 'HZero -> f -> z -> HList '[]
hReplicateF Proxy 'HZero
_ f
_ z
_ = HList '[]
HNil

instance (ApplyAB f z fz,
          HReplicateF n f z r')
  => HReplicateF (HSucc n) f z (fz ': r') where
    hReplicateF :: HLengthEq (fz : r') ('HSucc n) =>
Proxy ('HSucc n) -> f -> z -> HList (fz : r')
hReplicateF Proxy ('HSucc n)
n f
f z
z = forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f z
z forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall (n :: HNat) f z (r :: [*]).
(HReplicateF n f z r, HLengthEq r n) =>
Proxy n -> f -> z -> HList r
hReplicateF (forall (n :: HNat). Proxy ('HSucc n) -> Proxy n
hPred Proxy ('HSucc n)
n) f
f z
z

-- ** iterate
{- |

This function behaves like 'iterate', with an extra
argument to help figure out the result length

>>> let three = hSucc (hSucc (hSucc hZero))
>>> let f = Fun Just :: Fun '() Maybe

>>> :t applyAB f
applyAB f :: a -> Maybe a

f is applied to different types:

>>> hIterate three f ()
H[(),Just (),Just (Just ())]

It is also possible to specify the length later on,
as done with Prelude.'iterate'

>>> let take3 x | _ <- hLength x `asTypeOf` three = x
>>> take3 $ hIterate Proxy f ()
H[(),Just (),Just (Just ())]

-}
class HLengthEq r n => HIterate n f z r where
    hIterate :: HLengthEq r n => Proxy n -> f -> z -> HList r

instance HIterate HZero f z '[] where
    hIterate :: HLengthEq '[] 'HZero => Proxy 'HZero -> f -> z -> HList '[]
hIterate Proxy 'HZero
_ f
_ z
_ = HList '[]
HNil

instance (ApplyAB f z z',
      HIterate n f z' r',
      z ~ z_)
     => HIterate (HSucc n) f z (z_ ': r') where
    hIterate :: HLengthEq (z_ : r') ('HSucc n) =>
Proxy ('HSucc n) -> f -> z -> HList (z_ : r')
hIterate Proxy ('HSucc n)
n f
f z
z = z
z forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall (n :: HNat) f z (r :: [*]).
(HIterate n f z r, HLengthEq r n) =>
Proxy n -> f -> z -> HList r
hIterate (forall (n :: HNat). Proxy ('HSucc n) -> Proxy n
hPred Proxy ('HSucc n)
n) f
f (forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f z
z :: z')

-- * concat

{- |

Like 'concat' but for HLists of HLists.

Works in ghci... puzzling as what is different in doctest (it isn't
@-XExtendedDefaultRules@)

>>> let a = hEnd $ hBuild 1 2 3
>>> let b = hEnd $ hBuild 'a' "abc"
>>> hConcat $ hBuild a b
H[1,2,3,'a',"abc"]

-}
type HConcat xs = HConcatFD xs (HConcatR xs)

hConcat :: HConcat xs => HList xs -> HList (HConcatR xs)
hConcat :: forall (xs :: [*]). HConcat xs => HList xs -> HList (HConcatR xs)
hConcat HList xs
x = forall (xxs :: [*]) (xs :: [*]).
HConcatFD xxs xs =>
HList xxs -> HList xs
hConcatFD HList xs
x

type family HConcatR (a :: [*]) :: [*]
type instance HConcatR '[] = '[]
type instance HConcatR (x ': xs) = HAppendListR (UnHList x) (HConcatR xs)

type family UnHList a :: [*]
type instance UnHList (HList a) = a

-- for the benefit of ghc-7.10.1
class HConcatFD xxs xs | xxs -> xs
    where hConcatFD :: HList xxs -> HList xs

instance HConcatFD '[] '[] where
    hConcatFD :: HList '[] -> HList '[]
hConcatFD HList '[]
_ = HList '[]
HNil

instance (HConcatFD as bs, HAppendFD a bs cs) => HConcatFD (HList a ': as) cs where
    hConcatFD :: HList (HList a : as) -> HList cs
hConcatFD (HCons HList a
x HList as
xs) = HList a
x forall (a :: [*]) (b :: [*]) (ab :: [*]).
HAppendFD a b ab =>
HList a -> HList b -> HList ab
`hAppendFD` forall (xxs :: [*]) (xs :: [*]).
HConcatFD xxs xs =>
HList xxs -> HList xs
hConcatFD HList as
xs

class HAppendFD a b ab | a b -> ab where
    hAppendFD :: HList a -> HList b -> HList ab

instance HAppendFD '[] b b where
    hAppendFD :: HList '[] -> HList b -> HList b
hAppendFD HList '[]
_ HList b
b = HList b
b

instance HAppendFD as bs cs => HAppendFD (a ': as) bs (a ': cs) where
    hAppendFD :: HList (a : as) -> HList bs -> HList (a : cs)
hAppendFD (HCons a
a HList as
as) HList bs
bs = a
a forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall (a :: [*]) (b :: [*]) (ab :: [*]).
HAppendFD a b ab =>
HList a -> HList b -> HList ab
hAppendFD HList as
as HList bs
bs


-- --------------------------------------------------------------------------
-- * traversing HLists

-- ** producing HList
-- *** map
-- $mapNote It could be implemented with 'hFoldr', as we show further below

{- | hMap is written such that the length of the result list
can be determined from the length of the argument list (and
the other way around). Similarly, the type of the elements
of the list is propagated in both directions too.

>>> :set -XNoMonomorphismRestriction
>>> let xs = 1 .*. 'c' .*. HNil
>>> :t hMap (HJust ()) xs
hMap (HJust ()) xs :: Num y => HList '[HJust y, HJust Char]


These 4 examples show that the constraint on the length (2 in this case)
can be applied before or after the 'hMap'. That inference is independent of the
direction that type information is propagated for the individual elements.


>>> let asLen2 xs = xs `asTypeOf` (undefined :: HList '[a,b])

>>> let lr xs = asLen2 (applyAB (HMap HRead) xs)
>>> let ls xs = asLen2 (applyAB (HMap HShow) xs)
>>> let rl xs = applyAB (HMap HRead) (asLen2 xs)
>>> let sl xs = applyAB (HMap HShow) (asLen2 xs)


>>> :t lr
lr
  :: (Read ..., Read ...) => HList '[String, String] -> HList '[..., ...]

>>> :t rl
rl
  :: (Read ..., Read ...) => HList '[String, String] -> HList '[..., ...]


>>> :t ls
ls
  :: (Show ..., Show ...) => HList '[..., ...] -> HList '[String, String]

>>> :t sl
sl
  :: (Show ..., Show ...) => HList '[..., ...] -> HList '[String, String]

-}

newtype HMap f = HMap f

hMap :: f -> r a -> r b
hMap f
f r a
xs = forall f a b. ApplyAB f a b => f -> a -> b
applyAB (forall f. f -> HMap f
HMap f
f) r a
xs

instance (HMapCxt r f a b, as ~ r a, bs ~ r b)
    => ApplyAB (HMap f) as bs where
    applyAB :: HMap f -> as -> bs
applyAB (HMap f
f) = forall (r :: [*] -> *) f (x :: [*]) (y :: [*]).
(HMapAux r f x y, SameLength x y) =>
f -> r x -> r y
hMapAux f
f


-- | hMap constrained to HList
hMapL :: f -> HList a -> HList b
hMapL f
f HList a
xs = forall f a b. ApplyAB f a b => f -> a -> b
applyAB (forall f. f -> HMapL f
HMapL f
f) HList a
xs

newtype HMapL f = HMapL f

instance (HMapCxt HList f a b, as ~ HList a, bs ~ HList b) => ApplyAB (HMapL f) as bs where
    applyAB :: HMapL f -> as -> bs
applyAB (HMapL f
f) = forall (r :: [*] -> *) f (x :: [*]) (y :: [*]).
(HMapAux r f x y, SameLength x y) =>
f -> r x -> r y
hMapAux f
f


class (SameLength a b, HMapAux r f a b) => HMapCxt r f a b

instance (SameLength a b, HMapAux r f a b) => HMapCxt r f a b



class HMapAux (r :: [*] -> *) f (x :: [*]) (y :: [*]) where
  hMapAux :: SameLength x y => f -> r x -> r y

instance HMapAux HList f '[] '[] where
  hMapAux :: SameLength '[] '[] => f -> HList '[] -> HList '[]
hMapAux       f
_  HList '[]
_  = HList '[]
HNil

instance (ApplyAB f e e', HMapAux HList f l l', SameLength l l')
    => HMapAux HList f (e ': l) (e' ': l') where
  hMapAux :: SameLength (e : l) (e' : l') =>
f -> HList (e : l) -> HList (e' : l')
hMapAux f
f (HCons e
x HList l
l)    = forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f e
x forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall (r :: [*] -> *) f (x :: [*]) (y :: [*]).
(HMapAux r f x y, SameLength x y) =>
f -> r x -> r y
hMapAux f
f HList l
l




-- --------------------------------------------------------------------------

-- **** alternative implementation
-- $note currently broken

newtype MapCar f = MapCar f

-- | Same as 'hMap' only a different implementation.
hMapMapCar :: (HFoldr (MapCar f) (HList '[]) l l') =>
    f -> HList l -> l'
hMapMapCar :: forall f (l :: [*]) l'.
HFoldr (MapCar f) (HList '[]) l l' =>
f -> HList l -> l'
hMapMapCar f
f = forall f v (l :: [*]) r. HFoldr f v l r => f -> v -> HList l -> r
hFoldr (forall f. f -> MapCar f
MapCar f
f) HList '[]
HNil

instance ApplyAB f e e' => ApplyAB (MapCar f) (e,HList l) (HList (e' ': l)) where
    applyAB :: MapCar f -> (e, HList l) -> HList (e' : l)
applyAB (MapCar f
f) (e
e,HList l
l) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons (forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f e
e) HList l
l


-- --------------------------------------------------------------------------

-- *** @appEndo . mconcat . map Endo@
{- |

>>> let xs = length .*. (+1) .*. (*2) .*. HNil
>>> hComposeList xs "abc"
8


-}
hComposeList
  :: (HFoldr Comp (a -> a) l (t -> a)) => HList l -> t -> a
hComposeList :: forall a (l :: [*]) t.
HFoldr Comp (a -> a) l (t -> a) =>
HList l -> t -> a
hComposeList HList l
fs t
v0 = let r :: a
r = forall f v (l :: [*]) r. HFoldr f v l r => f -> v -> HList l -> r
hFoldr (Comp
Comp :: Comp) (\a
x -> a
x forall a. a -> a -> a
`asTypeOf` a
r) HList l
fs t
v0 in a
r


-- --------------------------------------------------------------------------

-- *** sequence
{- |
   A heterogeneous version of

   > sequenceA :: (Applicative m) => [m a] -> m [a]

   Only now we operate on heterogeneous lists, where different elements
   may have different types 'a'.
   In the argument list of monadic values (m a_i),
   although a_i may differ, the monad 'm' must be the same for all
   elements. That's why we needed "Data.HList.TypeCastGeneric2" (currently (~)).
   The typechecker will complain
   if we attempt to use hSequence on a HList of monadic values with different
   monads.

   The 'hSequence' problem was posed by Matthias Fischmann
   in his message on the Haskell-Cafe list on Oct 8, 2006

   <http://www.haskell.org/pipermail/haskell-cafe/2006-October/018708.html>

   <http://www.haskell.org/pipermail/haskell-cafe/2006-October/018784.html>
 -}

class (Applicative m, SameLength a b) => HSequence m a b | a -> b, m b -> a where
    hSequence :: HList a -> m (HList b)
{- ^

[@Maybe@]

>>> hSequence $ Just (1 :: Integer) `HCons` (Just 'c') `HCons` HNil
Just H[1,'c']

>>> hSequence $  return 1 `HCons` Just  'c' `HCons` HNil
Just H[1,'c']


[@List@]

>>> hSequence $ [1] `HCons` ['c'] `HCons` HNil
[H[1,'c']]


-}

instance Applicative m => HSequence m '[] '[] where
    hSequence :: HList '[] -> m (HList '[])
hSequence HList '[]
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure HList '[]
HNil

instance (m1 ~ m, Applicative m, HSequence m as bs) =>
    HSequence m (m1 a ': as) (a ': bs) where
    hSequence :: HList (m1 a : as) -> m (HList (a : bs))
hSequence (HCons m1 a
a HList as
b) = forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons m1 a
a (forall (m :: * -> *) (a :: [*]) (b :: [*]).
HSequence m a b =>
HList a -> m (HList b)
hSequence HList as
b)

-- **** alternative implementation

-- | 'hSequence2' is not recommended over 'hSequence' since it possibly doesn't
-- allow inferring argument types from the result types. Otherwise this version
-- should do exactly the same thing.
--
-- The DataKinds version needs a little help to find the type of the
-- return HNil, unlike the original version, which worked just fine as
--
--  > hSequence l = hFoldr ConsM (return HNil) l

hSequence2 :: HList l -> f a
hSequence2 HList l
l =
    let rHNil :: f (HList '[])
rHNil = forall (f :: * -> *) a. Applicative f => a -> f a
pure HList '[]
HNil forall a. a -> a -> a
`asTypeOf` (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HasCallStack => a
undefined f a
x)
        x :: f a
x = forall f v (l :: [*]) r. HFoldr f v l r => f -> v -> HList l -> r
hFoldr (forall f. f -> LiftA2 f
LiftA2 FHCons
FHCons) f (HList '[])
rHNil HList l
l
    in f a
x



-- --------------------------------------------------------------------------


-- --------------------------------------------------------------------------
-- ** producing homogenous lists

-- *** map (no sequencing)
-- $mapOut This one we implement via hFoldr

newtype Mapcar f = Mapcar f

instance (l ~ [e'], ApplyAB f e e', el ~ (e,l)) => ApplyAB (Mapcar f) el l where
    applyAB :: Mapcar f -> el -> l
applyAB (Mapcar f
f) (e
e, [e']
l) = forall f a b. ApplyAB f a b => f -> a -> b
applyAB f
f e
e forall a. a -> [a] -> [a]
: [e']
l

-- A synonym for the complex constraint
type HMapOut f l e = (HFoldr (Mapcar f) [e] l [e])

-- | compare @hMapOut f@ with @'hList2List' . 'hMap' f@
hMapOut :: forall f e l. HMapOut f l e => f -> HList l -> [e]
hMapOut :: forall f e (l :: [*]). HMapOut f l e => f -> HList l -> [e]
hMapOut f
f HList l
l = forall f v (l :: [*]) r. HFoldr f v l r => f -> v -> HList l -> r
hFoldr (forall f. f -> Mapcar f
Mapcar f
f) ([] :: [e]) HList l
l


-- --------------------------------------------------------------------------
-- *** mapM

-- |
--
-- > mapM :: forall b m a. (Monad m) => (a -> m b) -> [a] -> m [b]
--
-- Likewise for 'mapM_'.
--
-- See 'hSequence' if the result list should also be heterogenous.

hMapM   :: (Monad m, HMapOut f l (m e)) => f -> HList l -> [m e]
hMapM :: forall (m :: * -> *) f (l :: [*]) e.
(Monad m, HMapOut f l (m e)) =>
f -> HList l -> [m e]
hMapM f
f =  forall f e (l :: [*]). HMapOut f l e => f -> HList l -> [e]
hMapOut f
f

-- | GHC doesn't like its own type.
--
-- > hMapM_ :: forall m a f e. (Monad m, HMapOut f a (m e)) => f -> a -> m ()
--
-- Without explicit type signature, it's Ok. Sigh.
-- Anyway, Hugs does insist on a better type. So we restrict as follows:
--
hMapM_   :: (Monad m, HMapOut f l (m ())) => f -> HList l -> m ()
hMapM_ :: forall (m :: * -> *) f (l :: [*]).
(Monad m, HMapOut f l (m ())) =>
f -> HList l -> m ()
hMapM_ f
f =  forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall (q :: * -> *). [q ()] -> [q ()]
disambiguate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) f (l :: [*]) e.
(Monad m, HMapOut f l (m e)) =>
f -> HList l -> [m e]
hMapM f
f
 where
  disambiguate :: [q ()] -> [q ()]
  disambiguate :: forall (q :: * -> *). [q ()] -> [q ()]
disambiguate =  forall a. a -> a
id





-- --------------------------------------------------------------------------
-- * Ensure a list to contain HNats only
-- | We do so constructively, converting the HList whose elements
-- are Proxy HNat to [HNat]. The latter kind is unpopulated and
-- is present only at the type level.

type family HNats (l :: [*]) :: [HNat]
type instance HNats '[] = '[]
type instance HNats (Proxy n ': l) = n ': HNats l

hNats :: HList l -> Proxy (HNats l)
hNats :: forall (l :: [*]). HList l -> Proxy (HNats l)
hNats HList l
_ = forall {k} (t :: k). Proxy t
Proxy


-- --------------------------------------------------------------------------
-- * Membership tests

-- | Check to see if an HList contains an element with a given type
-- This is a type-level only test

class HMember (e1 :: k) (l :: [k]) (b :: Bool) | e1 l -> b
instance HMember e1 '[] False
instance (HEq e1 e b, HMember' b e1 l br) => HMember  e1 (e ': l) br
class HMember' (b0 :: Bool) (e1 :: k) (l :: [k]) (b :: Bool) | b0 e1 l -> b
instance HMember' True e1 l True
instance (HMember e1 l br) => HMember' False e1 l br

-- | The following is a similar type-only membership test
-- It uses the user-supplied curried type equality predicate pred
type family HMemberP pred e1 (l :: [*]) :: Bool
type instance HMemberP pred e1 '[] = False
type instance HMemberP pred e1 (e ': l) = HMemberP' pred e1 l (ApplyR pred (e1,e))

type family HMemberP' pred e1 (l :: [*]) pb :: Bool
type instance HMemberP' pred e1 l (Proxy True) = True
type instance HMemberP' pred e1 l (Proxy False) = HMemberP pred e1 l


hMember :: HMember e l b => Proxy e -> Proxy l -> Proxy b
hMember :: forall {k} (e :: k) (l :: [k]) (b :: Bool).
HMember e l b =>
Proxy e -> Proxy l -> Proxy b
hMember Proxy e
_ Proxy l
_ = forall {k} (t :: k). Proxy t
Proxy

-- ** Another type-level membership test
--
-- | Check to see if an element e occurs in a list l
-- If not, return 'Nothing
-- If the element does occur, return 'Just l1
-- where l1 is a type-level list without e
class HMemberM (e1 :: k) (l :: [k]) (r :: Maybe [k]) | e1 l -> r
instance HMemberM e1 '[] 'Nothing
instance (HEq e1 e b, HMemberM1 b e1 (e ': l) res)
      =>  HMemberM e1 (e ': l) res

class HMemberM1 (b::Bool) (e1 :: k) (l :: [k]) (r::Maybe [k]) | b e1 l -> r
instance HMemberM1 True e1 (e ': l) ('Just l)
instance (HMemberM e1 l r, HMemberM2 r e1 (e ': l) res)
    => HMemberM1 False e1 (e ': l) res

class HMemberM2 (b::Maybe [k]) (e1 :: k) (l :: [k]) (r::Maybe [k]) | b e1 l -> r
instance HMemberM2 Nothing e1 l Nothing
instance HMemberM2 (Just l1) e1 (e ': l) (Just (e ': l1))

-- --------------------------------------------------------------------------

-- * Staged equality for lists
-- $note removed. use Typeable instead


{-
-- * Static set property based on HEq
class HSet l
instance HSet HNil
instance (HMember e l HFalse, HSet l) => HSet (HCons e l)
-}

-- * Find an element in a set based on HEq
-- | It is a pure type-level operation
class HFind1 e l l n => HFind (e :: k) (l :: [k]) (n :: HNat) | e l -> n
instance HFind1 e l l n => HFind e l n

class HFind1 (e :: k) (l :: [k]) (l0 :: [k]) (n :: HNat) | e l -> n

instance (HEq e1 e2 b, HFind2 b e1 l l0 n) => HFind1 e1 (e2 ': l) l0 n
instance Fail (FieldNotFound e1 l0) => HFind1 e1 '[] l0 HZero

class HFind2 (b::Bool) (e :: k) (l::[k]) (l0::[k]) (n:: HNat) | b e l -> n
instance HFind2 True e l l0 HZero
instance HFind1 e l l0 n => HFind2 False e l l0 (HSucc n)



-- ** Membership test based on type equality

-- | could be an associated type if HEq had one
class HTMember e (l :: [*]) (b :: Bool) | e l -> b
instance HTMember e '[] False
instance (HEq e e' b, HTMember e l b', HOr b b' ~ b'')
      =>  HTMember e (e' ': l) b''

hTMember :: HTMember e l b => e -> HList l -> Proxy b
hTMember :: forall e (l :: [*]) (b :: Bool).
HTMember e l b =>
e -> HList l -> Proxy b
hTMember e
_ HList l
_ = forall {k} (t :: k). Proxy t
Proxy


-- * Intersection based on HTMember

class HTIntersect l1 l2 l3 | l1 l2 -> l3
 where
  -- | Like 'Data.List.intersect'
  hTIntersect :: HList l1 -> HList l2 -> HList l3

instance HTIntersect '[] l '[]
 where
  hTIntersect :: HList '[] -> HList l -> HList '[]
hTIntersect HList '[]
_ HList l
_ = HList '[]
HNil

instance ( HTMember h l1 b
         , HTIntersectBool b h t l1 l2
         )
         => HTIntersect (h ': t) l1 l2
 where
  hTIntersect :: HList (h : t) -> HList l1 -> HList l2
hTIntersect (HCons h
h HList t
t) HList l1
l1 = forall (b :: Bool) h (t :: [*]) (l1 :: [*]) (l2 :: [*]).
HTIntersectBool b h t l1 l2 =>
Proxy b -> h -> HList t -> HList l1 -> HList l2
hTIntersectBool Proxy b
b h
h HList t
t HList l1
l1
   where
    b :: Proxy b
b = forall e (l :: [*]) (b :: Bool).
HTMember e l b =>
e -> HList l -> Proxy b
hTMember h
h HList l1
l1

class HTIntersectBool (b :: Bool) h t l1 l2 | b h t l1 -> l2
 where
 hTIntersectBool :: Proxy b -> h -> HList t -> HList l1 -> HList l2

instance HTIntersect t l1 l2
      => HTIntersectBool True h t l1 (h ': l2)
 where
  hTIntersectBool :: Proxy 'True -> h -> HList t -> HList l1 -> HList (h : l2)
hTIntersectBool Proxy 'True
_ h
h HList t
t HList l1
l1 = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons h
h (forall (l1 :: [*]) (l2 :: [*]) (l3 :: [*]).
HTIntersect l1 l2 l3 =>
HList l1 -> HList l2 -> HList l3
hTIntersect HList t
t HList l1
l1)

instance HTIntersect t l1 l2
      => HTIntersectBool False h t l1 l2
 where
  hTIntersectBool :: Proxy 'False -> h -> HList t -> HList l1 -> HList l2
hTIntersectBool Proxy 'False
_ h
_ HList t
t HList l1
l1 = forall (l1 :: [*]) (l2 :: [*]) (l3 :: [*]).
HTIntersect l1 l2 l3 =>
HList l1 -> HList l2 -> HList l3
hTIntersect HList t
t HList l1
l1


-- * Convert between heterogeneous lists and homogeneous ones

-- | @hMapOut id@ is similar, except this function is restricted
-- to HLists that actually contain a value (so the list produced
-- will be nonempty). This restriction allows adding a functional
-- dependency, which means that less type annotations can be necessary.
class HList2List l e | l -> e
 where
  hList2List :: HList l -> [e]
  list2HListSuffix :: [e] -> Maybe (HList l, [e])


list2HList :: HList2List l e => [e] -> Maybe (HList l)
list2HList :: forall (l :: [*]) e. HList2List l e => [e] -> Maybe (HList l)
list2HList = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (l :: [*]) e. HList2List l e => [e] -> Maybe (HList l, [e])
list2HListSuffix


instance HList2List '[e] e
 where
  hList2List :: HList '[e] -> [e]
hList2List (HCons e
e HList '[]
R:HList[]
HNil) = [e
e]

  list2HListSuffix :: [e] -> Maybe (HList '[e], [e])
list2HListSuffix (e
e : [e]
es) = forall a. a -> Maybe a
Just (forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e HList '[]
HNil, [e]
es)
  list2HListSuffix [] = forall a. Maybe a
Nothing


instance HList2List (e' ': l) e
      => HList2List (e ': e' ': l) e
 where
  hList2List :: HList (e : e' : l) -> [e]
hList2List (HCons e
e HList (e' : l)
l) = e
eforall a. a -> [a] -> [a]
:forall (l :: [*]) e. HList2List l e => HList l -> [e]
hList2List HList (e' : l)
l

  list2HListSuffix :: [e] -> Maybe (HList (e : e' : l), [e])
list2HListSuffix (e
e : [e]
es) = (\(HList (e' : l)
hl,[e]
rest) -> (forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e HList (e' : l)
hl, [e]
rest))
                                  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (l :: [*]) e. HList2List l e => [e] -> Maybe (HList l, [e])
list2HListSuffix [e]
es
  list2HListSuffix [] = forall a. Maybe a
Nothing

-- | @Prism [s] [t] (HList s) (HList t)@
listAsHList :: p (HList l) (f (HList l)) -> p [e] (f [e])
listAsHList p (HList l) (f (HList l))
x = forall b t s a.
(b -> t)
-> (s -> Either t a)
-> forall (p :: * -> * -> *) (f :: * -> *).
   (Choice p, Applicative f) =>
   p a (f b) -> p s (f t)
prism forall (l :: [*]) e. HList2List l e => HList l -> [e]
hList2List (\[e]
l -> case forall (l :: [*]) e. HList2List l e => [e] -> Maybe (HList l, [e])
list2HListSuffix [e]
l of
                                 Just (HList l
hl,[])  -> forall a b. b -> Either a b
Right HList l
hl
                                 Maybe (HList l, [e])
_ -> forall a b. a -> Either a b
Left []) p (HList l) (f (HList l))
x

-- | @Prism' [a] (HList s)@
--
-- where @s ~ HReplicateR n a@
listAsHList' :: p (HList l) (f (HList l)) -> p [e] (f [e])
listAsHList' p (HList l) (f (HList l))
x = forall {k1} {k2} optic (p :: k1 -> k2 -> *) (a :: k1)
       (f :: k1 -> k2) (s :: k1).
(optic ~ (p a (f a) -> p s (f s))) =>
optic -> optic
isSimple forall {p :: * -> * -> *} {f :: * -> *} {l :: [*]} {e} {l :: [*]}
       {e}.
(Choice p, Applicative f, HList2List l e, HList2List l e) =>
p (HList l) (f (HList l)) -> p [e] (f [e])
listAsHList p (HList l) (f (HList l))
x


-- --------------------------------------------------------------------------
-- * With 'HMaybe'

-- ** Turn list in a list of justs
-- | the same as @map Just@
--
-- >>> toHJust (2 .*. 'a' .*. HNil)
-- H[HJust 2,HJust 'a']
--
-- >>> toHJust2 (2 .*. 'a' .*. HNil)
-- H[HJust 2,HJust 'a']

class FromHJustR (ToHJustR l) ~ l => ToHJust l
 where
  type ToHJustR l :: [*]
  toHJust :: HList l -> HList (ToHJustR l)

instance ToHJust '[]
 where
  type ToHJustR '[] = '[]
  toHJust :: HList '[] -> HList (ToHJustR '[])
toHJust HList '[]
R:HList[]
HNil = HList '[]
HNil

instance ToHJust l => ToHJust (e ': l)
 where
  type ToHJustR (e ': l) = HJust e ': ToHJustR l
  toHJust :: HList (e : l) -> HList (ToHJustR (e : l))
toHJust (HCons e
e HList l
l) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons (forall x. x -> HJust x
HJust e
e) (forall (l :: [*]). ToHJust l => HList l -> HList (ToHJustR l)
toHJust HList l
l)

-- | alternative implementation. The Apply instance is in "Data.HList.FakePrelude".
-- A longer type could be inferred.
toHJust2 :: (HMapCxt r (HJust ()) a b,
             ToHJust a, b ~ ToHJustR a -- added to get equivalent inference
             ) => r a -> r b
toHJust2 :: forall (r :: [*] -> *) (a :: [*]) (b :: [*]).
(HMapCxt r (HJust ()) a b, ToHJust a, b ~ ToHJustR a) =>
r a -> r b
toHJust2 r a
xs = forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {f}.
(SameLength' a b, SameLength' b a, HMapAux r f a b) =>
f -> r a -> r b
hMap (forall x. x -> HJust x
HJust ()) r a
xs

-- --------------------------------------------------------------------------
-- ** Extract justs from list of maybes
--
-- >>> let xs = 2 .*. 'a' .*. HNil
-- >>> fromHJust (toHJust xs) == xs
-- True

class (FromHJustR (ToHJustR l) ~ l) => FromHJust l
 where
  type FromHJustR l :: [*]
  fromHJust :: HList l -> HList (FromHJustR l)

instance FromHJust '[]
 where
  type FromHJustR '[] = '[]
  fromHJust :: HList '[] -> HList (FromHJustR '[])
fromHJust HList '[]
R:HList[]
HNil = HList '[]
HNil

instance FromHJust l => FromHJust (HNothing ': l)
 where
  type FromHJustR (HNothing ': l) = FromHJustR l
  fromHJust :: HList (HNothing : l) -> HList (FromHJustR (HNothing : l))
fromHJust (HCons HNothing
_ HList l
l) = forall (l :: [*]). FromHJust l => HList l -> HList (FromHJustR l)
fromHJust HList l
l

instance FromHJust l => FromHJust (HJust e ': l)
 where
  type FromHJustR (HJust e ': l) = e ': FromHJustR l
  fromHJust :: HList (HJust e : l) -> HList (FromHJustR (HJust e : l))
fromHJust (HCons (HJust e
e) HList l
l) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e (forall (l :: [*]). FromHJust l => HList l -> HList (FromHJustR l)
fromHJust HList l
l)

-- *** alternative implementation

-- | This implementation is shorter.
fromHJust2 :: (HMapCxt r HFromJust a b) => r a -> r b
fromHJust2 :: forall (r :: [*] -> *) (a :: [*]) (b :: [*]).
HMapCxt r HFromJust a b =>
r a -> r b
fromHJust2 r a
xs = forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {f}.
(SameLength' a b, SameLength' b a, HMapAux r f a b) =>
f -> r a -> r b
hMap HFromJust
HFromJust r a
xs

data HFromJust = HFromJust
instance (hJustA ~ HJust a) => ApplyAB HFromJust hJustA a where
    applyAB :: HFromJust -> hJustA -> a
applyAB HFromJust
_ (HJust a
a) = a
a


-- --------------------------------------------------------------------------
-- * Annotated lists

data HAddTag t = HAddTag t
data HRmTag    = HRmTag

-- hAddTag :: HMapCxt (HAddTag t) l r => t -> HList l -> HList r
hAddTag :: t -> r a -> r b
hAddTag t
t r a
l = forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {f}.
(SameLength' a b, SameLength' b a, HMapAux r f a b) =>
f -> r a -> r b
hMap (forall t. t -> HAddTag t
HAddTag t
t) r a
l

-- hRmTag ::  HMapCxt HRmTag l => HList l -> HList (HMapR HRmTag l)
hRmTag :: r a -> r b
hRmTag r a
l    = forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {f}.
(SameLength' a b, SameLength' b a, HMapAux r f a b) =>
f -> r a -> r b
hMap HRmTag
HRmTag r a
l

instance (et ~ (e,t)) => ApplyAB (HAddTag t) e et
 where
  applyAB :: HAddTag t -> e -> et
applyAB (HAddTag t
t) e
e = (e
e,t
t)


instance (e' ~ e) => ApplyAB HRmTag (e,t) e'
 where
  applyAB :: HRmTag -> (e, t) -> e'
applyAB HRmTag
_ (e
e,t
_) = e
e


-- | Annotate list with a type-level Boolean
--
-- > hFlag :: HMapCxt (HAddTag (Proxy True)) l r => HList l -> HList r
hFlag :: r a -> r b
hFlag r a
l = forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {t}.
(SameLength' a b, SameLength' b a, HMapAux r (HAddTag t) a b) =>
t -> r a -> r b
hAddTag Proxy 'True
hTrue r a
l


-- --------------------------------------------------------------------------
-- * Splitting by HTrue and HFalse

-- | Analogus to Data.List.'Data.List.partition' 'snd'. See also 'HPartition'
--
-- >>> let (.=.) :: p x -> y -> Tagged x y; _ .=. y = Tagged y
-- >>> hSplit $ hTrue .=. 2 .*. hTrue .=. 3 .*. hFalse .=. 1 .*. HNil
-- (H[2,3],H[1])
--
-- it might make more sense to instead have @LVPair Bool e@
-- instead of @(e, Proxy Bool)@ since the former has the same
-- runtime representation as @e@

class HSplit l
 where
  type HSplitT l :: [*]
  type HSplitF l :: [*]
  hSplit :: HList l -> (HList (HSplitT l), HList (HSplitF l))

instance HSplit '[]
 where
  type HSplitT '[] = '[]
  type HSplitF '[] = '[]
  hSplit :: HList '[] -> (HList (HSplitT '[]), HList (HSplitF '[]))
hSplit HList '[]
R:HList[]
HNil = (HList '[]
HNil,HList '[]
HNil)

instance HSplit l => HSplit ((e, Proxy True) ': l)
 where

  type HSplitT ((e,Proxy True) ': l) = e ': HSplitT l
  type HSplitF ((e,Proxy True) ': l) = HSplitF l

  hSplit :: HList ((e, Proxy 'True) : l)
-> (HList (HSplitT ((e, Proxy 'True) : l)),
    HList (HSplitF ((e, Proxy 'True) : l)))
hSplit (HCons (e
e,Proxy 'True
_) HList l
l) = (forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e HList (HSplitT l)
l',HList (HSplitF l)
l'')
   where
    (HList (HSplitT l)
l',HList (HSplitF l)
l'') = forall (l :: [*]).
HSplit l =>
HList l -> (HList (HSplitT l), HList (HSplitF l))
hSplit HList l
l

instance HSplit l => HSplit ((e,Proxy False) ': l)
 where
  type HSplitT ((e,Proxy False) ': l) = HSplitT l
  type HSplitF ((e,Proxy False) ': l) = e ': HSplitF l

  hSplit :: HList ((e, Proxy 'False) : l)
-> (HList (HSplitT ((e, Proxy 'False) : l)),
    HList (HSplitF ((e, Proxy 'False) : l)))
hSplit (HCons (e
e,Proxy 'False
_) HList l
l) = (HList (HSplitT l)
l',forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e HList (HSplitF l)
l'')
   where
    (HList (HSplitT l)
l',HList (HSplitF l)
l'') = forall (l :: [*]).
HSplit l =>
HList l -> (HList (HSplitT l), HList (HSplitF l))
hSplit HList l
l


instance HSplit l => HSplit (Tagged True e ': l)
 where

  type HSplitT (Tagged True e ': l) = e ': HSplitT l
  type HSplitF (Tagged True e ': l) = HSplitF l

  hSplit :: HList (Tagged 'True e : l)
-> (HList (HSplitT (Tagged 'True e : l)),
    HList (HSplitF (Tagged 'True e : l)))
hSplit (HCons (Tagged e
e) HList l
l) = (forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e HList (HSplitT l)
l',HList (HSplitF l)
l'')
   where
    (HList (HSplitT l)
l',HList (HSplitF l)
l'') = forall (l :: [*]).
HSplit l =>
HList l -> (HList (HSplitT l), HList (HSplitF l))
hSplit HList l
l

instance HSplit l => HSplit (Tagged False e ': l)
 where
  type HSplitT (Tagged False e ': l) = HSplitT l
  type HSplitF (Tagged False e ': l) = e ': HSplitF l

  hSplit :: HList (Tagged 'False e : l)
-> (HList (HSplitT (Tagged 'False e : l)),
    HList (HSplitF (Tagged 'False e : l)))
hSplit (HCons (Tagged e
e) HList l
l) = (HList (HSplitT l)
l',forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e HList (HSplitF l)
l'')
   where
    (HList (HSplitT l)
l',HList (HSplitF l)
l'') = forall (l :: [*]).
HSplit l =>
HList l -> (HList (HSplitT l), HList (HSplitF l))
hSplit HList l
l
{-

Let expansion makes a difference to Hugs:

HListPrelude> let x = (hFlag (HCons "1" HNil)) in hSplit x
(HCons "1" HNil,HNil)
HListPrelude> hSplit (hFlag (HCons "1" HNil))
ERROR - Unresolved overloading
*** Type       : HSplit (HCons ([Char],HTrue) HNil) a b => (a,b)
*** Expression : hSplit (hFlag (HCons "1" HNil))


-}

-- --------------------------------------------------------------------------
-- * Splitting by Length

{- | 'splitAt'

setup

>>> let two = hSucc (hSucc hZero)
>>> let xsys = hEnd $ hBuild 1 2 3 4

If a length is explicitly provided, the resulting lists are inferred

>>> hSplitAt two xsys
(H[1,2],H[3,4])

>>> let sameLength_ :: SameLength a b => r a -> r b -> r a; sameLength_ = const
>>> let len2 x = x `sameLength_` HCons () (HCons () HNil)

If the first chunk of the list (a) has to be a certain length, the type of the
Proxy argument can be inferred.

>>> case hSplitAt Proxy xsys of (a,b) -> (len2 a, b)
(H[1,2],H[3,4])

-}
class (HLengthEq xs n,
       HAppendList1 xs ys xsys
       )
      => HSplitAt (n :: HNat) xsys xs ys
                   | n xsys -> xs ys
                      , xs ys -> xsys
                      , xs -> n
                     where
    hSplitAt :: Proxy n -> HList xsys -> (HList xs, HList ys)

instance (HSplitAt1 '[] n xsys xs ys,
          HAppendList1 xs ys xsys,
          HLengthEq xs n) =>
    HSplitAt n xsys xs ys where
      hSplitAt :: Proxy n -> HList xsys -> (HList xs, HList ys)
hSplitAt Proxy n
n HList xsys
xsys = forall (accum :: [*]) (n :: HNat) (xsys :: [*]) (xs :: [*])
       (ys :: [*]).
HSplitAt1 accum n xsys xs ys =>
HList accum -> Proxy n -> HList xsys -> (HList xs, HList ys)
hSplitAt1 HList '[]
HNil Proxy n
n HList xsys
xsys

-- | helper for 'HSplitAt'
class HSplitAt1 accum (n :: HNat) xsys xs ys | accum n xsys -> xs ys where
    hSplitAt1 :: HList accum -> Proxy n -> HList xsys -> (HList xs, HList ys)

instance HRevApp accum '[] xs => HSplitAt1 accum HZero ys xs ys where
    hSplitAt1 :: HList accum -> Proxy 'HZero -> HList ys -> (HList xs, HList ys)
hSplitAt1 HList accum
xs Proxy 'HZero
_zero HList ys
ys = (forall {l1 :: [*]} {l3 :: [*]}.
HRevApp l1 '[] l3 =>
HList l1 -> HList l3
hReverse_ HList accum
xs, HList ys
ys)

instance HSplitAt1 (b ': accum) n bs xs ys
    => HSplitAt1 accum (HSucc n) (b ': bs) xs ys where
    hSplitAt1 :: HList accum
-> Proxy ('HSucc n) -> HList (b : bs) -> (HList xs, HList ys)
hSplitAt1 HList accum
accum Proxy ('HSucc n)
n (HCons b
b HList bs
bs) = forall (accum :: [*]) (n :: HNat) (xsys :: [*]) (xs :: [*])
       (ys :: [*]).
HSplitAt1 accum n xsys xs ys =>
HList accum -> Proxy n -> HList xsys -> (HList xs, HList ys)
hSplitAt1 (forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons b
b HList accum
accum) (forall (n :: HNat). Proxy ('HSucc n) -> Proxy n
hPred Proxy ('HSucc n)
n) HList bs
bs

{- | a better way to write @HLength xs ~ n@ because:

1. it works properly with ghc-7.10 (probably another example of ghc bug #10009)

2. it works backwards a bit in that if @n@ is known, then @xs@ can be
   refined:

>>> undefined :: HLengthEq xs HZero => HList xs
H[]

-}
class (SameLength' (HReplicateR n ()) xs,
        HLengthEq1 xs n, HLengthEq2 xs n) => HLengthEq (xs :: [*]) (n :: HNat) | xs -> n

instance (SameLength' (HReplicateR n ()) xs,
          HLengthEq1 xs n, HLengthEq2 xs n) => HLengthEq xs n

class HLengthEq1 (xs :: [*]) n -- pick the instance based on n's constructor
instance (HLengthEq xs n, xxs ~ (x ': xs)) => HLengthEq1 xxs (HSucc n)
instance (xxs ~ '[]) => HLengthEq1 xxs HZero

class HLengthEq2 (xs :: [*]) n | xs -> n -- pick the instance based on xs' constructor
instance (HLengthEq xs n, sn ~ HSucc n) => HLengthEq2 (x ': xs) sn
instance zero ~ HZero => HLengthEq2 '[] zero

-- | @HLengthGe xs n@ says that @HLength xs >= n@.
--
-- unlike the expression with a type family HLength,
-- ghc assumes @xs ~ (aFresh ': bFresh)@ when given a
-- constraint @HLengthGe xs (HSucc HZero)@
class HLengthGe (xs :: [*]) (n :: HNat)
instance (HLengthGe xs n, xxs ~ (x ': xs)) => HLengthGe xxs (HSucc n)
instance HLengthGe xxs HZero

-- | @HAppendList1 xs ys xsys@ is the type-level way of saying @xs ++ ys == xsys@
--
-- used by 'HSplitAt'
class HStripPrefix xs xsys ys
      => HAppendList1 (xs :: [k]) (ys :: [k]) (xsys :: [k])
        | xs ys -> xsys,
          xs xsys -> ys
          -- , ys xsys -> xs
          -- hard to prove

instance HAppendList1 '[] ys ys
instance (HAppendList1 xs ys zs) => HAppendList1 (x ': xs) ys (x ': zs)


-- | analog of 'Data.List.stripPrefix'
class HStripPrefix xs xsys ys | xs xsys -> ys
instance (x' ~ x, HStripPrefix xs xsys ys) => HStripPrefix (x' ': xs) (x ': xsys) ys
instance HStripPrefix '[] ys ys


-- ** take

class HTake (n :: HNat) xs ys | n xs -> ys where
    hTake :: (HLengthEq ys n, HLengthGe xs n) => Proxy n -> HList xs -> HList ys

instance HTake HZero xs '[] where
    hTake :: (HLengthEq '[] 'HZero, HLengthGe xs 'HZero) =>
Proxy 'HZero -> HList xs -> HList '[]
hTake Proxy 'HZero
_ HList xs
_ = HList '[]
HNil

instance (HLengthEq ys n, HLengthGe xs n, HTake n xs ys)
        => HTake (HSucc n) (x ': xs) (x ': ys) where
    hTake :: (HLengthEq (x : ys) ('HSucc n), HLengthGe (x : xs) ('HSucc n)) =>
Proxy ('HSucc n) -> HList (x : xs) -> HList (x : ys)
hTake Proxy ('HSucc n)
sn (HCons x
x HList xs
xs) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons x
x (forall (n :: HNat) (xs :: [*]) (ys :: [*]).
(HTake n xs ys, HLengthEq ys n, HLengthGe xs n) =>
Proxy n -> HList xs -> HList ys
hTake (forall (n :: HNat). Proxy ('HSucc n) -> Proxy n
hPred Proxy ('HSucc n)
sn) HList xs
xs)

-- ** drop

class HDrop (n :: HNat) xs ys | n xs -> ys where
    hDrop :: HLengthGe xs n => Proxy n -> HList xs -> HList ys

instance HDrop HZero xs xs where
    hDrop :: HLengthGe xs 'HZero => Proxy 'HZero -> HList xs -> HList xs
hDrop Proxy 'HZero
_ HList xs
xs = HList xs
xs

instance (HLengthGe xs n, HDrop n xs ys) => HDrop (HSucc n) (x ': xs) ys where
    hDrop :: HLengthGe (x : xs) ('HSucc n) =>
Proxy ('HSucc n) -> HList (x : xs) -> HList ys
hDrop Proxy ('HSucc n)
sn (HCons x
_ HList xs
xs) = forall (n :: HNat) (xs :: [*]) (ys :: [*]).
(HDrop n xs ys, HLengthGe xs n) =>
Proxy n -> HList xs -> HList ys
hDrop (forall (n :: HNat). Proxy ('HSucc n) -> Proxy n
hPred Proxy ('HSucc n)
sn) HList xs
xs


-- * Conversion to and from tuples

class HTuple v t | v -> t, t -> v where
    -- | alternatively: @hUncurry (,,,)@
    hToTuple :: HList v -> t
    hFromTuple :: t -> HList v

-- | @Iso (HList v) (HList v') a b@
hTuple :: p a (f b) -> p (HList v) (f (HList v))
hTuple p a (f b)
x = forall (p :: * -> * -> *) (f :: * -> *) s a b t.
(Profunctor p, Functor f) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
iso forall (v :: [*]) t. HTuple v t => HList v -> t
hToTuple forall (v :: [*]) t. HTuple v t => t -> HList v
hFromTuple p a (f b)
x

-- | @Iso' (HList v) a@
hTuple' :: p a (f a) -> p (HList v) (f (HList v))
hTuple' p a (f a)
x = forall {k1} {k2} optic (p :: k1 -> k2 -> *) (a :: k1)
       (f :: k1 -> k2) (s :: k1).
(optic ~ (p a (f a) -> p s (f s))) =>
optic -> optic
isSimple forall {p :: * -> * -> *} {f :: * -> *} {v :: [*]} {a} {v :: [*]}
       {b}.
(Profunctor p, Functor f, HTuple v a, HTuple v b) =>
p a (f b) -> p (HList v) (f (HList v))
hTuple p a (f a)
x

instance HTuple '[] () where
    hToTuple :: HList '[] -> ()
hToTuple HList '[]
R:HList[]
HNil = ()
    hFromTuple :: () -> HList '[]
hFromTuple () = HList '[]
HNil

instance HTuple '[a,b] (a,b) where
    hToTuple :: HList '[a, b] -> (a, b)
hToTuple (a
a `HCons` b
b `HCons` HList '[]
R:HList[]
HNil) = (a
a,b
b)
    hFromTuple :: (a, b) -> HList '[a, b]
hFromTuple (a
a,b
b) = (a
a forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` b
b forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList '[]
HNil)

instance HTuple '[a,b,c] (a,b,c) where
    hToTuple :: HList '[a, b, c] -> (a, b, c)
hToTuple (a
a `HCons` b
b `HCons` c
c `HCons` HList '[]
R:HList[]
HNil) = (a
a,b
b,c
c)
    hFromTuple :: (a, b, c) -> HList '[a, b, c]
hFromTuple (a
a,b
b,c
c) = (a
a forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` b
b forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` c
c forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList '[]
HNil)

instance HTuple '[a,b,c,d] (a,b,c,d) where
    hToTuple :: HList '[a, b, c, d] -> (a, b, c, d)
hToTuple (a
a `HCons` b
b `HCons` c
c `HCons` d
d `HCons` HList '[]
R:HList[]
HNil) = (a
a,b
b,c
c,d
d)
    hFromTuple :: (a, b, c, d) -> HList '[a, b, c, d]
hFromTuple (a
a,b
b,c
c,d
d) = (a
a forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` b
b forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` c
c forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` d
d forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList '[]
HNil)

instance HTuple '[a,b,c,d,e] (a,b,c,d,e) where
    hToTuple :: HList '[a, b, c, d, e] -> (a, b, c, d, e)
hToTuple (a
a `HCons` b
b `HCons` c
c `HCons` d
d `HCons` e
e `HCons` HList '[]
R:HList[]
HNil) = (a
a,b
b,c
c,d
d,e
e)
    hFromTuple :: (a, b, c, d, e) -> HList '[a, b, c, d, e]
hFromTuple (a
a,b
b,c
c,d
d,e
e) = (a
a forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` b
b forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` c
c forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` d
d forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` e
e forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList '[]
HNil)

instance HTuple '[a,b,c,d,e,f] (a,b,c,d,e,f) where
    hToTuple :: HList '[a, b, c, d, e, f] -> (a, b, c, d, e, f)
hToTuple (a
a `HCons` b
b `HCons` c
c `HCons` d
d `HCons` e
e `HCons` f
f `HCons` HList '[]
R:HList[]
HNil) = (a
a,b
b,c
c,d
d,e
e,f
f)
    hFromTuple :: (a, b, c, d, e, f) -> HList '[a, b, c, d, e, f]
hFromTuple (a
a,b
b,c
c,d
d,e
e,f
f) = (a
a forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` b
b forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` c
c forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` d
d forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` e
e forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` f
f forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList '[]
HNil)


-- | 'tails'
class HTails a b | a -> b, b -> a where
    hTails :: HList a -> HList b

instance HTails '[] '[HList '[]] where
    hTails :: HList '[] -> HList '[HList '[]]
hTails HList '[]
_ = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons HList '[]
HNil HList '[]
HNil

instance (HTails xs ys) => HTails (x ': xs) (HList (x ': xs) ': ys) where
    hTails :: HList (x : xs) -> HList (HList (x : xs) : ys)
hTails xxs :: HList (x : xs)
xxs@(HCons x
_x HList xs
xs) = HList (x : xs)
xxs forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall (a :: [*]) (b :: [*]). HTails a b => HList a -> HList b
hTails HList xs
xs


-- | 'inits'
class HInits a b | a -> b, b -> a where
    hInits :: HList a -> HList b

instance HInits1 a b => HInits a (HList '[] ': b) where
    hInits :: HList a -> HList (HList '[] : b)
hInits HList a
xs = HList '[]
HNil forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall (a :: [*]) (b :: [*]). HInits1 a b => HList a -> HList b
hInits1 HList a
xs


-- | behaves like @tail . inits@
class HInits1 a b | a -> b, b -> a where
    hInits1 :: HList a -> HList b

instance HInits1 '[] '[HList '[]] where
    hInits1 :: HList '[] -> HList '[HList '[]]
hInits1 HList '[]
_ = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons HList '[]
HNil HList '[]
HNil

instance (HInits1 xs ys,
          HMapCxt HList (FHCons2 x) ys ys',
          HMapCons x ys ~ ys',
          HMapTail ys' ~ ys)
  => HInits1 (x ': xs) (HList '[x] ':  ys') where
    hInits1 :: HList (x : xs) -> HList (HList '[x] : ys')
hInits1 (HCons x
x HList xs
xs) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons x
x HList '[]
HNil forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {f}.
(SameLength' a b, SameLength' b a, HMapAux r f a b) =>
f -> r a -> r b
hMap (forall x. x -> FHCons2 x
FHCons2 x
x) (forall (a :: [*]) (b :: [*]). HInits1 a b => HList a -> HList b
hInits1 HList xs
xs)


-- | similar to 'FHCons'
data FHCons2 x = FHCons2 x

instance (hxs ~ HList xs,
          hxxs ~ HList (x ': xs))
  => ApplyAB (FHCons2 x) hxs hxxs where
  applyAB :: FHCons2 x -> hxs -> hxxs
applyAB (FHCons2 x
x) hxs
xs = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons x
x hxs
xs


-- | evidence to satisfy the fundeps in HInits
type family HMapCons (x :: *) (xxs :: [*]) :: [*]
type instance HMapCons x (HList a ': b) = HList (x ': a) ': HMapCons x b
type instance HMapCons x '[] = '[]

-- | evidence to satisfy the fundeps in HInits
type family HMapTail (xxs :: [*]) :: [*]
type instance HMapTail ( HList (a ': as) ': bs) = HList as ': HMapTail bs
type instance HMapTail '[] = '[]


-- * partition

{- | @HPartitionEq f x1 xs xi xo@ is analogous to

> (xi,xo) = partition (f x1) xs

where @f@ is a \"function\" passed in using it's instance of 'HEqBy'
-}
class HPartitionEq f x1 xs xi xo | f x1 xs -> xi xo where
    hPartitionEq :: Proxy f -> Proxy x1 -> HList xs -> (HList xi, HList xo)

instance HPartitionEq f x1 '[] '[] '[] where
    hPartitionEq :: Proxy f -> Proxy x1 -> HList '[] -> (HList '[], HList '[])
hPartitionEq Proxy f
_ Proxy x1
_ HList '[]
_ = (HList '[]
HNil, HList '[]
HNil)

instance
   (HEqBy f x1 x b,
    HPartitionEq1 b f x1 x xs xi xo) => HPartitionEq f x1 (x ': xs) xi xo where
      hPartitionEq :: Proxy f -> Proxy x1 -> HList (x : xs) -> (HList xi, HList xo)
hPartitionEq Proxy f
f Proxy x1
x1 (HCons x
x HList xs
xs) = forall {k} {k} (b :: Bool) (f :: k) (x1 :: k) x (xs :: [*])
       (xi :: [*]) (xo :: [*]).
HPartitionEq1 b f x1 x xs xi xo =>
Proxy b
-> Proxy f -> Proxy x1 -> x -> HList xs -> (HList xi, HList xo)
hPartitionEq1 (forall {k} (t :: k). Proxy t
Proxy :: Proxy b) Proxy f
f Proxy x1
x1 x
x HList xs
xs

class HPartitionEq1 (b :: Bool) f x1 x xs xi xo | b f x1 x xs -> xi xo where
    hPartitionEq1 :: Proxy b -> Proxy f -> Proxy x1 -> x -> HList xs -> (HList xi, HList xo)

instance HPartitionEq f x1 xs xi xo =>
    HPartitionEq1 True f x1 x xs (x ': xi) xo where
      hPartitionEq1 :: Proxy 'True
-> Proxy f
-> Proxy x1
-> x
-> HList xs
-> (HList (x : xi), HList xo)
hPartitionEq1 Proxy 'True
_ Proxy f
f Proxy x1
x1 x
x HList xs
xs = case forall {k} {k} (f :: k) (x1 :: k) (xs :: [*]) (xi :: [*])
       (xo :: [*]).
HPartitionEq f x1 xs xi xo =>
Proxy f -> Proxy x1 -> HList xs -> (HList xi, HList xo)
hPartitionEq Proxy f
f Proxy x1
x1 HList xs
xs of
         (HList xi
xi, HList xo
xo) -> (x
x forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList xi
xi, HList xo
xo)

instance HPartitionEq f x1 xs xi xo =>
    HPartitionEq1 False f x1 x xs xi (x ': xo) where
      hPartitionEq1 :: Proxy 'False
-> Proxy f
-> Proxy x1
-> x
-> HList xs
-> (HList xi, HList (x : xo))
hPartitionEq1 Proxy 'False
_ Proxy f
f Proxy x1
x1 x
x HList xs
xs = case forall {k} {k} (f :: k) (x1 :: k) (xs :: [*]) (xi :: [*])
       (xo :: [*]).
HPartitionEq f x1 xs xi xo =>
Proxy f -> Proxy x1 -> HList xs -> (HList xi, HList xo)
hPartitionEq Proxy f
f Proxy x1
x1 HList xs
xs of
         (HList xi
xi, HList xo
xo) -> (HList xi
xi, x
x forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList xo
xo)


-- * groupBy

{- | @HGroupBy f x y@ is analogous to @y = 'groupBy' f x@

given that @f@ is used by 'HEqBy'
-}
class HGroupBy (f :: t) (as :: [*]) (gs :: [*]) | f as -> gs, gs -> as where
    hGroupBy :: Proxy f -> HList as -> HList gs

instance (HSpanEqBy f a as fst snd,
          HGroupBy f snd gs) => HGroupBy f (a ': as) (HList (a ': fst) ': gs) where
    hGroupBy :: Proxy f -> HList (a : as) -> HList (HList (a : fst) : gs)
hGroupBy Proxy f
f (HCons a
x HList as
xs) = case forall t (f :: t) x (y :: [*]) (fst :: [*]) (snd :: [*]).
HSpanEqBy f x y fst snd =>
Proxy f -> x -> HList y -> (HList fst, HList snd)
hSpanEqBy Proxy f
f a
x HList as
xs of
                      (HList fst
first, HList snd
second) -> (a
x forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList fst
first) forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall t (f :: t) (as :: [*]) (gs :: [*]).
HGroupBy f as gs =>
Proxy f -> HList as -> HList gs
hGroupBy Proxy f
f HList snd
second

instance HGroupBy f '[] '[] where
    hGroupBy :: Proxy f -> HList '[] -> HList '[]
hGroupBy Proxy f
_f HList '[]
R:HList[]
HNil = HList '[]
HNil

-- * span

-- | @HSpanEq x y fst snd@ is analogous to @(fst,snd) = 'span' (== x) y@
class HSpanEqBy (f :: t) (x :: *) (y :: [*]) (fst :: [*]) (snd :: [*])
      | f x y -> fst snd, fst snd -> y where
  hSpanEqBy :: Proxy f -> x -> HList y -> (HList fst, HList snd)

instance (HSpanEqBy1 f x y fst snd,
          HAppendListR fst snd ~ y)
    => HSpanEqBy f x y fst snd where
  hSpanEqBy :: Proxy f -> x -> HList y -> (HList fst, HList snd)
hSpanEqBy Proxy f
f x
x HList y
y =  forall t (f :: t) x (y :: [*]) (i :: [*]) (o :: [*]).
HSpanEqBy1 f x y i o =>
Proxy f -> x -> HList y -> (HList i, HList o)
hSpanEqBy1 Proxy f
f x
x HList y
y

class HSpanEqBy1 (f :: t) (x :: *) (y :: [*]) (i :: [*]) (o :: [*])
      | f x y -> i o where
  hSpanEqBy1 :: Proxy f -> x -> HList y -> (HList i, HList o)

class HSpanEqBy2 (b :: Bool) (f :: t) (x :: *) (y :: *) (ys :: [*]) (i :: [*]) (o :: [*])
      | b f x y ys -> i o where
  hSpanEqBy2 :: Proxy b -> Proxy f -> x -> y -> HList ys -> (HList i, HList o)


instance (HEqBy f x y b,
          HSpanEqBy2 b f x y ys i o) => HSpanEqBy1 f x (y ': ys) i o where
  hSpanEqBy1 :: Proxy f -> x -> HList (y : ys) -> (HList i, HList o)
hSpanEqBy1 Proxy f
f x
x (HCons y
y HList ys
ys) = forall t (b :: Bool) (f :: t) x y (ys :: [*]) (i :: [*])
       (o :: [*]).
HSpanEqBy2 b f x y ys i o =>
Proxy b -> Proxy f -> x -> y -> HList ys -> (HList i, HList o)
hSpanEqBy2 (forall {k} (t :: k). Proxy t
Proxy :: Proxy b) Proxy f
f x
x (y
y :: y) (HList ys
ys :: HList ys)

instance HSpanEqBy1 f x '[] '[] '[] where
    hSpanEqBy1 :: Proxy f -> x -> HList '[] -> (HList '[], HList '[])
hSpanEqBy1 Proxy f
_f x
_x HList '[]
_xs = (HList '[]
HNil, HList '[]
HNil)

instance HSpanEqBy1 f x zs i o
    => HSpanEqBy2 True f x y zs (y ': i) o where
  hSpanEqBy2 :: Proxy 'True
-> Proxy f -> x -> y -> HList zs -> (HList (y : i), HList o)
hSpanEqBy2 Proxy 'True
_ Proxy f
f x
x y
y HList zs
zs = case forall t (f :: t) x (y :: [*]) (i :: [*]) (o :: [*]).
HSpanEqBy1 f x y i o =>
Proxy f -> x -> HList y -> (HList i, HList o)
hSpanEqBy1 Proxy f
f x
x HList zs
zs of
                                      (HList i
i, HList o
o) -> (forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons y
y HList i
i, HList o
o)

instance HSpanEqBy2 False f x y ys '[] (y ': ys) where
  hSpanEqBy2 :: Proxy 'False
-> Proxy f -> x -> y -> HList ys -> (HList '[], HList (y : ys))
hSpanEqBy2 Proxy 'False
_b Proxy f
_f x
_x y
y HList ys
ys = (HList '[]
HNil, forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons y
y HList ys
ys)



-- * zip

-- $note see alternative implementations in "Data.HList.HZip"



instance (SameLengths [x,y,xy], HZipList x y xy) => HUnzip HList x y xy where
  hUnzip :: HList xy -> (HList x, HList y)
hUnzip = forall (x :: [*]) (y :: [*]) (l :: [*]).
HZipList x y l =>
HList l -> (HList x, HList y)
hUnzipList

instance (SameLengths [x,y,xy], HZipList x y xy) => HZip HList x y xy where
  hZip :: HList x -> HList y -> HList xy
hZip = forall (x :: [*]) (y :: [*]) (l :: [*]).
HZipList x y l =>
HList x -> HList y -> HList l
hZipList


class HZipList x y l | x y -> l, l -> x y where
  hZipList   :: HList x -> HList y -> HList l
  hUnzipList :: HList l -> (HList x, HList y)

instance HZipList '[] '[] '[] where
  hZipList :: HList '[] -> HList '[] -> HList '[]
hZipList HList '[]
_ HList '[]
_ = HList '[]
HNil
  hUnzipList :: HList '[] -> (HList '[], HList '[])
hUnzipList HList '[]
_ = (HList '[]
HNil, HList '[]
HNil)

instance ((x,y)~z, HZipList xs ys zs) => HZipList (x ': xs) (y ': ys) (z ': zs) where
  hZipList :: HList (x : xs) -> HList (y : ys) -> HList (z : zs)
hZipList (HCons x
x HList xs
xs) (HCons y
y HList ys
ys) = (x
x,y
y) forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` forall (x :: [*]) (y :: [*]) (l :: [*]).
HZipList x y l =>
HList x -> HList y -> HList l
hZipList HList xs
xs HList ys
ys
  hUnzipList :: HList (z : zs) -> (HList (x : xs), HList (y : ys))
hUnzipList (HCons ~(x
x,y
y) HList zs
zs) = let ~(HList xs
xs,HList ys
ys) = forall (x :: [*]) (y :: [*]) (l :: [*]).
HZipList x y l =>
HList l -> (HList x, HList y)
hUnzipList HList zs
zs in (x
x forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList xs
xs, y
y forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList ys
ys)

-- * Monoid instance

{- | Analogous to the Monoid instance for tuples

>>> import Data.Monoid
>>> mempty :: HList '[(), All, [Int]]
H[(),All {getAll = True},[]]

>>> mappend (hBuild "a") (hBuild "b") :: HList '[String]
H["ab"]

-}
instance
   (HProxies a,
    HMapCxt HList ConstMempty (AddProxy a) a,
    HZip HList a a aa,
    HMapCxt HList UncurryMappend aa a) => Monoid (HList a) where
  mempty :: HList a
mempty = forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {f}.
(SameLength' a b, SameLength' b a, HMapAux r f a b) =>
f -> r a -> r b
hMap ConstMempty
ConstMempty
            forall a b. (a -> b) -> a -> b
$ (forall (xs :: [*]) (pxs :: [*]). HProxiesFD xs pxs => HList pxs
hProxies :: HList (AddProxy a))
  mappend :: HList a -> HList a -> HList a
mappend HList a
a HList a
b = forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {f}.
(SameLength' a b, SameLength' b a, HMapAux r f a b) =>
f -> r a -> r b
hMap UncurryMappend
UncurryMappend forall a b. (a -> b) -> a -> b
$ forall (r :: [*] -> *) (x :: [*]) (y :: [*]) (xy :: [*]).
HZip r x y xy =>
r x -> r y -> r xy
hZip HList a
a HList a
b

instance
    (HZip HList a a aa,
     HMapCxt HList UncurryMappend aa a) => Semigroup (HList a) where
  HList a
a <> :: HList a -> HList a -> HList a
<> HList a
b = forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {f}.
(SameLength' a b, SameLength' b a, HMapAux r f a b) =>
f -> r a -> r b
hMap UncurryMappend
UncurryMappend forall a b. (a -> b) -> a -> b
$ forall (r :: [*] -> *) (x :: [*]) (y :: [*]) (xy :: [*]).
HZip r x y xy =>
r x -> r y -> r xy
hZip HList a
a HList a
b

-- ** helper functions

data ConstMempty = ConstMempty
instance (x ~ Proxy y, Monoid y) => ApplyAB ConstMempty x y where
    applyAB :: ConstMempty -> x -> y
applyAB ConstMempty
_ x
_ = forall a. Monoid a => a
mempty

data UncurryMappend = UncurryMappend
instance (aa ~ (a,a), Monoid a) => ApplyAB UncurryMappend aa a where
    applyAB :: UncurryMappend -> aa -> a
applyAB UncurryMappend
_ = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Monoid a => a -> a -> a
mappend

data UncurrySappend = UncurrySappend
instance (aa ~ (a,a), Semigroup a) => ApplyAB UncurrySappend aa a where
    applyAB :: UncurrySappend -> aa -> a
applyAB UncurrySappend
_ = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Semigroup a => a -> a -> a
(<>)