{-# LANGUAGE Trustworthy #-}
-- |
--
-- This module is designed to imported qualified:
--
-- @
-- import qualified Data.SOP.NP.DeFun as NP
-- @
--
module Data.SOP.NP.DeFun (
    -- * Append
    Append, AppendSym, AppendSym1,
    append, appendSym, appendSym1,
    -- * Map
    Map, MapSym, MapSym1,
    map, mapSym, mapSym1,
    -- * Concat
    Concat, ConcatSym,
    concat, concatSym,
    -- * ConcatMap
    ConcatMap, ConcatMapSym, ConcatMapSym1,
    concatMap, concatMapSym, concatMapSym1,
    -- * Map2
    Map2, Map2Sym, Map2Sym1, Map2Sym2,
    map2, map2Sym, map2Sym1, map2Sym2,
    -- * Sequence
    Sequence, SequenceSym,
    sequence, sequenceSym,
    -- * Foldr
    Foldr, FoldrSym, FoldrSym1, FoldrSym2,
    foldr, foldrSym, foldrSym1, foldrSym2,
    -- * Foldl
    Foldl, FoldlSym, FoldlSym1, FoldlSym2,
    foldl, foldlSym, foldlSym1, foldlSym2,
    -- * ZipWith
    ZipWith, ZipWithSym, ZipWithSym1, ZipWithSym2,
    zipWith, zipWithSym, zipWithSym1, zipWithSym2,
    -- * Reverse
    Reverse, ReverseSym,
    reverse, reverseSym,
) where

import DeFun.List

import Data.SOP.NP (NP (..))

import DeFun.Core
import DeFun.Function

-- $setup
-- >>> import Prelude (Char, Maybe (..), Show)
-- >>> import Numeric.Natural (Natural)
-- >>> import Data.SOP.NP (NP (..))
-- >>> import DeFun.Core
-- >>> :set -dppr-cols9999
--
-- >>> data Nat = Z | S Nat
-- >>> data SNat (n :: Nat) where { SZ :: SNat Z; SS :: SNat n -> SNat (S n) }
-- >>> deriving instance Show (SNat n)

-------------------------------------------------------------------------------
-- Append
-------------------------------------------------------------------------------

append :: NP a xs -> NP a ys -> NP a (Append xs ys)
append :: forall {a} (a :: a -> *) (xs :: [a]) (ys :: [a]).
NP a xs -> NP a ys -> NP a (Append xs ys)
append NP a xs
Nil       NP a ys
ys = NP a ys
ys
append (a x
x :* NP a xs
xs) NP a ys
ys = a x
x forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {a} (a :: a -> *) (xs :: [a]) (ys :: [a]).
NP a xs -> NP a ys -> NP a (Append xs ys)
append NP a xs
xs NP a ys
ys

appendSym :: Lam2 (NP a) (NP a) (NP a) AppendSym
appendSym :: forall {k} (a :: k -> *). Lam2 (NP a) (NP a) (NP a) AppendSym
appendSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} (a :: a -> *) (xs :: [a]).
NP a xs -> Lam (NP a) (NP a) (AppendSym1 xs)
appendSym1

appendSym1 :: NP a xs -> Lam (NP a) (NP a) (AppendSym1 xs)
appendSym1 :: forall {a} (a :: a -> *) (xs :: [a]).
NP a xs -> Lam (NP a) (NP a) (AppendSym1 xs)
appendSym1 NP a xs
xs = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} (a :: a -> *) (xs :: [a]) (ys :: [a]).
NP a xs -> NP a ys -> NP a (Append xs ys)
append NP a xs
xs)

-------------------------------------------------------------------------------
-- Map
-------------------------------------------------------------------------------

map :: Lam a b f -> NP a xs -> NP b (Map f xs)
map :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b)
       (xs :: [a]).
Lam a b f -> NP a xs -> NP b (Map f xs)
map Lam a b f
_ NP a xs
Nil       = forall {k} (a :: k -> *). NP a '[]
Nil
map Lam a b f
f (a x
x :* NP a xs
xs) = Lam a b f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b)
       (xs :: [a]).
Lam a b f -> NP a xs -> NP b (Map f xs)
map Lam a b f
f NP a xs
xs

mapSym :: Lam (a :~> b) (Lam (NP a) (NP b)) MapSym
mapSym :: forall {k} {k} (a :: k -> *) (b :: k -> *).
Lam (a :~> b) (Lam (NP a) (NP b)) MapSym
mapSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b).
Lam a b f -> Lam (NP a) (NP b) (MapSym1 f)
mapSym1

mapSym1 :: Lam a b f -> Lam (NP a) (NP b) (MapSym1 f)
mapSym1 :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b).
Lam a b f -> Lam (NP a) (NP b) (MapSym1 f)
mapSym1 Lam a b f
f = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b)
       (xs :: [a]).
Lam a b f -> NP a xs -> NP b (Map f xs)
map Lam a b f
f)

-------------------------------------------------------------------------------
-- Concat
-------------------------------------------------------------------------------

concat :: NP (NP a) xss -> NP a (Concat xss)
concat :: forall {a} (a :: a -> *) (xss :: [[a]]).
NP (NP a) xss -> NP a (Concat xss)
concat NP (NP a) xss
Nil         = forall {k} (a :: k -> *). NP a '[]
Nil
concat (NP a x
xs :* NP (NP a) xs
xss) = forall {a} (a :: a -> *) (xs :: [a]) (ys :: [a]).
NP a xs -> NP a ys -> NP a (Append xs ys)
append NP a x
xs (forall {a} (a :: a -> *) (xss :: [[a]]).
NP (NP a) xss -> NP a (Concat xss)
concat NP (NP a) xs
xss)

concatSym :: Lam (NP (NP a)) (NP a) ConcatSym
concatSym :: forall {k} (a :: k -> *). Lam (NP (NP a)) (NP a) ConcatSym
concatSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} (a :: a -> *) (xss :: [[a]]).
NP (NP a) xss -> NP a (Concat xss)
concat

-------------------------------------------------------------------------------
-- ConcatMap
-------------------------------------------------------------------------------

concatMap :: Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs)
concatMap :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> [b])
       (xs :: [a]).
Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs)
concatMap Lam a (NP b) f
_ NP a xs
Nil       = forall {k} (a :: k -> *). NP a '[]
Nil
concatMap Lam a (NP b) f
f (a x
x :* NP a xs
xs) = forall {a} (a :: a -> *) (xs :: [a]) (ys :: [a]).
NP a xs -> NP a ys -> NP a (Append xs ys)
append (Lam a (NP b) f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x) (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> [b])
       (xs :: [a]).
Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs)
concatMap Lam a (NP b) f
f NP a xs
xs)

concatMapSym :: Lam2 (a :~> NP b) (NP a) (NP b) ConcatMapSym
concatMapSym :: forall {k} {k} (a :: k -> *) (b :: k -> *).
Lam2 (a :~> NP b) (NP a) (NP b) ConcatMapSym
concatMapSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> [b]).
Lam a (NP b) f -> Lam (NP a) (NP b) (ConcatMapSym1 f)
concatMapSym1

concatMapSym1 :: Lam a (NP b) f -> Lam (NP a) (NP b) (ConcatMapSym1 f)
concatMapSym1 :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> [b]).
Lam a (NP b) f -> Lam (NP a) (NP b) (ConcatMapSym1 f)
concatMapSym1 Lam a (NP b) f
f = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> [b])
       (xs :: [a]).
Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs)
concatMap Lam a (NP b) f
f)

-------------------------------------------------------------------------------
-- Map2
-------------------------------------------------------------------------------

map2 :: Lam2 a b c f -> NP a xs -> NP b ys -> NP c (Map2 f xs ys)
map2 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]).
Lam2 a b c f -> NP a xs -> NP b ys -> NP c (Map2 f xs ys)
map2 Lam2 a b c f
f NP a xs
xs NP b ys
ys = forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> [b])
       (xs :: [a]).
Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs)
concatMap (forall {b1} {c1} {a1} (b2 :: b1 -> *) (c2 :: c1 -> *)
       (f :: b1 ~> c1) (a2 :: a1 -> *) (g :: a1 ~> b1).
Lam b2 c2 f -> Lam a2 b2 g -> Lam a2 c2 (CompSym2 f g)
compSym2 (forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
       (c2 :: c1 -> *) (f :: a1 ~> (b1 ~> c1)) (x :: b1).
Lam2 a2 b2 c2 f -> b2 x -> Lam a2 c2 (FlipSym2 f x)
flipSym2 forall {k} {k} (a :: k -> *) (b :: k -> *).
Lam (a :~> b) (Lam (NP a) (NP b)) MapSym
mapSym NP b ys
ys) Lam2 a b c f
f) NP a xs
xs

map2Sym :: Lam3 (a :~> b :~> c) (NP a) (NP b) (NP c) Map2Sym
map2Sym :: forall {k} {k} {k} (a :: k -> *) (b :: k -> *) (c :: k -> *).
Lam3 (a :~> (b :~> c)) (NP a) (NP b) (NP c) Map2Sym
map2Sym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)).
Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (Map2Sym1 f)
map2Sym1

map2Sym1 :: Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (Map2Sym1 f)
map2Sym1 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)).
Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (Map2Sym1 f)
map2Sym1 Lam2 a b c f
f = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (xs :: [a]).
Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (Map2Sym2 f xs)
map2Sym2 Lam2 a b c f
f)

map2Sym2 :: Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (Map2Sym2 f xs)
map2Sym2 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (xs :: [a]).
Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (Map2Sym2 f xs)
map2Sym2 Lam2 a b c f
f NP a xs
xs = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]).
Lam2 a b c f -> NP a xs -> NP b ys -> NP c (Map2 f xs ys)
map2 Lam2 a b c f
f NP a xs
xs)

-------------------------------------------------------------------------------
-- Sequence
-------------------------------------------------------------------------------

sequence :: NP (NP a) xss -> NP (NP a) (Sequence xss)
sequence :: forall {a} (a :: a -> *) (xss :: [[a]]).
NP (NP a) xss -> NP (NP a) (Sequence xss)
sequence NP (NP a) xss
Nil         = forall {k} (a :: k -> *). NP a '[]
Nil forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {k} (a :: k -> *). NP a '[]
Nil
sequence (NP a x
xs :* NP (NP a) xs
xss) = forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]).
Lam2 a b c f -> NP a xs -> NP b ys -> NP c (Map2 f xs ys)
map2 (forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
       (c2 :: c1 -> *) (con :: a1 -> b1 -> c1).
LamRep2 a2 b2 c2 (Con2 con) -> Lam2 a2 b2 c2 (Con2 con)
con2 forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
(:*)) NP a x
xs (forall {a} (a :: a -> *) (xss :: [[a]]).
NP (NP a) xss -> NP (NP a) (Sequence xss)
sequence NP (NP a) xs
xss)

sequenceSym :: Lam (NP (NP a)) (NP (NP a)) SequenceSym
sequenceSym :: forall {k} (a :: k -> *). Lam (NP (NP a)) (NP (NP a)) SequenceSym
sequenceSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} (a :: a -> *) (xss :: [[a]]).
NP (NP a) xss -> NP (NP a) (Sequence xss)
sequence

-------------------------------------------------------------------------------
-- Foldr
-------------------------------------------------------------------------------

foldr :: Lam2 a b b f -> b x -> NP a ys -> b (Foldr f x ys)
foldr :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b))
       (x :: b) (ys :: [a]).
Lam2 a b b f -> b x -> NP a ys -> b (Foldr f x ys)
foldr Lam2 a b b f
_ b x
z NP a ys
Nil       = b x
z
foldr Lam2 a b b f
f b x
z (a x
x :* NP a xs
xs) = Lam2 a b b f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b))
       (x :: b) (ys :: [a]).
Lam2 a b b f -> b x -> NP a ys -> b (Foldr f x ys)
foldr Lam2 a b b f
f b x
z NP a xs
xs)

foldrSym :: Lam3 (a :~> b :~> b) b (NP a) b FoldrSym
foldrSym :: forall {k} {b} (a :: k -> *) (b :: b -> *).
Lam3 (a :~> (b :~> b)) b (NP a) b FoldrSym
foldrSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b)).
Lam2 a b b f -> Lam2 b (NP a) b (FoldrSym1 f)
foldrSym1

foldrSym1 :: Lam2 a b b f -> Lam2 b (NP a) b (FoldrSym1 f)
foldrSym1 :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b)).
Lam2 a b b f -> Lam2 b (NP a) b (FoldrSym1 f)
foldrSym1 Lam2 a b b f
f = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b))
       (x :: b).
Lam2 a b b f -> b x -> Lam (NP a) b (FoldrSym2 f x)
foldrSym2 Lam2 a b b f
f)

foldrSym2 :: Lam2 a b b f -> b x -> Lam (NP a) b (FoldrSym2 f x)
foldrSym2 :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b))
       (x :: b).
Lam2 a b b f -> b x -> Lam (NP a) b (FoldrSym2 f x)
foldrSym2 Lam2 a b b f
f b x
z = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b))
       (x :: b) (ys :: [a]).
Lam2 a b b f -> b x -> NP a ys -> b (Foldr f x ys)
foldr Lam2 a b b f
f b x
z)

-------------------------------------------------------------------------------
-- Foldl
-------------------------------------------------------------------------------

foldl :: Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys)
foldl :: forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b))
       (x :: b) (ys :: [a]).
Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys)
foldl Lam2 b a b f
_ b x
z NP a ys
Nil       = b x
z
foldl Lam2 b a b f
f b x
z (a x
x :* NP a xs
xs) = forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b))
       (x :: b) (ys :: [a]).
Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys)
foldl Lam2 b a b f
f (Lam2 b a b f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ b x
z forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x) NP a xs
xs

foldlSym :: Lam3 (b :~> a :~> b) b (NP a) b FoldlSym
foldlSym :: forall {b} {k} (b :: b -> *) (a :: k -> *).
Lam3 (b :~> (a :~> b)) b (NP a) b FoldlSym
foldlSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b)).
Lam2 b a b f -> Lam2 b (NP a) b (FoldlSym1 f)
foldlSym1

foldlSym1 :: Lam2 b a b f -> Lam2 b (NP a) b (FoldlSym1 f)
foldlSym1 :: forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b)).
Lam2 b a b f -> Lam2 b (NP a) b (FoldlSym1 f)
foldlSym1 Lam2 b a b f
f = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b))
       (x :: b).
Lam2 b a b f -> b x -> Lam (NP a) b (FoldlSym2 f x)
foldlSym2 Lam2 b a b f
f)

foldlSym2 :: Lam2 b a b f -> b x -> Lam (NP a) b (FoldlSym2 f x)
foldlSym2 :: forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b))
       (x :: b).
Lam2 b a b f -> b x -> Lam (NP a) b (FoldlSym2 f x)
foldlSym2 Lam2 b a b f
f b x
z = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b))
       (x :: b) (ys :: [a]).
Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys)
foldl Lam2 b a b f
f b x
z)

-------------------------------------------------------------------------------
-- ZipWith
-------------------------------------------------------------------------------

zipWith :: Lam2 a b c f -> NP a xs -> NP b ys -> NP c (ZipWith f xs ys)
zipWith :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]).
Lam2 a b c f -> NP a xs -> NP b ys -> NP c (ZipWith f xs ys)
zipWith Lam2 a b c f
_ NP a xs
Nil       NP b ys
_         = forall {k} (a :: k -> *). NP a '[]
Nil
zipWith Lam2 a b c f
_ (a x
_ :* NP a xs
_)  NP b ys
Nil       = forall {k} (a :: k -> *). NP a '[]
Nil
zipWith Lam2 a b c f
f (a x
x :* NP a xs
xs) (b x
y :* NP b xs
ys) = Lam2 a b c f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
       (x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ b x
y forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]).
Lam2 a b c f -> NP a xs -> NP b ys -> NP c (ZipWith f xs ys)
zipWith Lam2 a b c f
f NP a xs
xs NP b xs
ys

zipWithSym :: Lam3 (a :~> b :~> c) (NP a) (NP b) (NP c) ZipWithSym
zipWithSym :: forall {k} {k} {k} (a :: k -> *) (b :: k -> *) (c :: k -> *).
Lam3 (a :~> (b :~> c)) (NP a) (NP b) (NP c) ZipWithSym
zipWithSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)).
Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (ZipWithSym1 f)
zipWithSym1

zipWithSym1 :: Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (ZipWithSym1 f)
zipWithSym1 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)).
Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (ZipWithSym1 f)
zipWithSym1 Lam2 a b c f
f = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (xs :: [a]).
Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (ZipWithSym2 f xs)
zipWithSym2 Lam2 a b c f
f)

zipWithSym2 :: Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (ZipWithSym2 f xs)
zipWithSym2 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (xs :: [a]).
Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (ZipWithSym2 f xs)
zipWithSym2 Lam2 a b c f
f NP a xs
xs = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
       (f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]).
Lam2 a b c f -> NP a xs -> NP b ys -> NP c (ZipWith f xs ys)
zipWith Lam2 a b c f
f NP a xs
xs)

-------------------------------------------------------------------------------
-- Reverse
-------------------------------------------------------------------------------

-- |
--
-- >>> reverse (SZ :* SS SZ :* SS (SS SZ) :* Nil)
-- SS (SS SZ) :* SS SZ :* SZ :* Nil
--
reverse :: NP a xs -> NP a (Reverse xs)
reverse :: forall {a} (a :: a -> *) (xs :: [a]). NP a xs -> NP a (Reverse xs)
reverse = forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b))
       (x :: b) (ys :: [a]).
Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys)
foldl (forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
       (c2 :: c1 -> *) (f :: a1 ~> (b1 ~> c1)).
Lam2 a2 b2 c2 f -> Lam2 b2 a2 c2 (FlipSym1 f)
flipSym1 (forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
       (c2 :: c1 -> *) (con :: a1 -> b1 -> c1).
LamRep2 a2 b2 c2 (Con2 con) -> Lam2 a2 b2 c2 (Con2 con)
con2 forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
(:*))) forall {k} (a :: k -> *). NP a '[]
Nil

reverseSym :: Lam (NP a) (NP a) ReverseSym
reverseSym :: forall {k} (a :: k -> *). Lam (NP a) (NP a) ReverseSym
reverseSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} (a :: a -> *) (xs :: [a]). NP a xs -> NP a (Reverse xs)
reverse