{-# LANGUAGE TypeOperators #-}

module ZkFold.Symbolic.Data.List where

import           Control.Applicative              (Applicative)
import           Data.Functor.Rep                 (Representable)
import           Data.Kind                        (Type)
import           Data.Proxy                       (Proxy (..))
import           Data.Traversable                 (Traversable)
import           Data.Zip                         (Zip)
import           GHC.Generics                     (Par1 (..))
import           Prelude                          (fmap, fst, pure, type (~), undefined, ($), (.), (<$>))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Data.Utils           (zipWithM)
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool        (Bool (..))
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Combinators
import           ZkFold.Symbolic.Data.Conditional
import           ZkFold.Symbolic.MonadCircuit

data List (context :: (Type -> Type) -> Type) x
    = List
        { forall (context :: (Type -> Type) -> Type) x.
List context x -> context (Layout x)
lHash    :: (context (Layout x))
        , forall (context :: (Type -> Type) -> Type) x.
List context x -> context Par1
lSize    :: (context Par1)
        , forall (context :: (Type -> Type) -> Type) x. List context x -> [x]
lWitness :: [x]
        -- ^ TODO: As the name suggests, this is only needed in witness cinstruction in uncons.
        -- This list is never used in circuit itlest.
        -- Think of a better solution for carrying witnesses.
        -- Besides, List is not an instance of SymbolicData while this list is present
        }

-- | TODO: A proof-of-concept where hash == id.
-- Replace id with a proper hash if we need lists to be cryptographically secure.
--
emptyList
    :: forall context x
    .  Symbolic context
    => Applicative (Layout x)
    => List context x
emptyList :: forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, Applicative (Layout x)) =>
List context x
emptyList = context (Layout x) -> context Par1 -> [x] -> List context x
forall (context :: (Type -> Type) -> Type) x.
context (Layout x) -> context Par1 -> [x] -> List context x
List (Layout x (BaseField context) -> context (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Layout x (BaseField context) -> context (Layout x))
-> Layout x (BaseField context) -> context (Layout x)
forall a b. (a -> b) -> a -> b
$ BaseField context -> Layout x (BaseField context)
forall a. a -> Layout x a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BaseField context
forall a. AdditiveMonoid a => a
zero) (Par1 (BaseField context) -> context Par1
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Par1 (BaseField context) -> context Par1)
-> Par1 (BaseField context) -> context Par1
forall a b. (a -> b) -> a -> b
$ BaseField context -> Par1 (BaseField context)
forall p. p -> Par1 p
Par1 BaseField context
forall a. AdditiveMonoid a => a
zero) []

-- | A list is empty if it's size is 0, in which case the first element of @runInvert@ is @one@.
--
null
    :: forall context x
    .  Symbolic context
    => List context x
    -> Bool context
null :: forall (context :: (Type -> Type) -> Type) x.
Symbolic context =>
List context x -> Bool context
null List{context Par1
context (Layout x)
[x]
lHash :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context (Layout x)
lSize :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context Par1
lWitness :: forall (context :: (Type -> Type) -> Type) x. List context x -> [x]
lHash :: context (Layout x)
lSize :: context Par1
lWitness :: [x]
..} = context Par1 -> Bool context
forall (c :: (Type -> Type) -> Type). c Par1 -> Bool c
Bool (context Par1
-> CircuitFun Par1 Par1 (BaseField context) -> context Par1
forall (f :: Type -> Type) (g :: Type -> Type).
context f -> CircuitFun f g (BaseField context) -> context g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun f g (BaseField c) -> c g
fromCircuitF context Par1
lSize (((Par1 i, Par1 i) -> Par1 i) -> m (Par1 i, Par1 i) -> m (Par1 i)
forall a b. (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Par1 i, Par1 i) -> Par1 i
forall a b. (a, b) -> a
fst (m (Par1 i, Par1 i) -> m (Par1 i))
-> (Par1 i -> m (Par1 i, Par1 i)) -> Par1 i -> m (Par1 i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Par1 i -> m (Par1 i, Par1 i)
forall i a (m :: Type -> Type) (f :: Type -> Type).
(MonadCircuit i a m, Representable f, Traversable f) =>
f i -> m (f i, f i)
runInvert))

infixr 5 .:
(.:)
    :: forall context x
    .  Symbolic context
    => Traversable (Layout x)
    => Zip (Layout x)
    => SymbolicData x
    => Context x ~ context
    => Support x ~ Proxy context
    => x
    -> List context x
    -> List context x
x
x .: :: forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, Traversable (Layout x), Zip (Layout x),
 SymbolicData x, Context x ~ context, Support x ~ Proxy context) =>
x -> List context x -> List context x
.: List{context Par1
context (Layout x)
[x]
lHash :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context (Layout x)
lSize :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context Par1
lWitness :: forall (context :: (Type -> Type) -> Type) x. List context x -> [x]
lHash :: context (Layout x)
lSize :: context Par1
lWitness :: [x]
..} = context (Layout x) -> context Par1 -> [x] -> List context x
forall (context :: (Type -> Type) -> Type) x.
context (Layout x) -> context Par1 -> [x] -> List context x
List context (Layout x)
incSum context Par1
incSize (x
xx -> [x] -> [x]
forall a. a -> [a] -> [a]
:[x]
lWitness)
    where
        xRepr :: context (Layout x)
        xRepr :: context (Layout x)
xRepr = x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces x
x (forall {k} (t :: k). Proxy t
forall (t :: (Type -> Type) -> Type). Proxy t
Proxy @context)

        incSum :: context (Layout x)
        incSum :: context (Layout x)
incSum = context (Layout x)
-> context (Layout x)
-> context Par1
-> (forall {i} {m :: Type -> Type}.
    MonadCircuit i (BaseField context) m =>
    Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type) (k :: Type -> Type).
Symbolic c =>
c f
-> c g
-> c h
-> (forall i (m :: Type -> Type).
    MonadCircuit i (BaseField c) m =>
    f i -> g i -> h i -> m (k i))
-> c k
fromCircuit3F context (Layout x)
lHash context (Layout x)
xRepr context Par1
lSize ((forall {i} {m :: Type -> Type}.
  MonadCircuit i (BaseField context) m =>
  Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
 -> context (Layout x))
-> (forall {i} {m :: Type -> Type}.
    MonadCircuit i (BaseField context) m =>
    Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x)
forall a b. (a -> b) -> a -> b
$
            \Layout x i
vHash Layout x i
vRepr (Par1 i
s) -> (i -> i -> m i) -> Layout x i -> Layout x i -> m (Layout x i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM (\i
h i
r -> ClosedPoly i (BaseField context) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
h x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p i
r x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (i -> x
p i
s x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
forall a. MultiplicativeMonoid a => a
one))) Layout x i
vHash Layout x i
vRepr

        incSize :: context Par1
        incSize :: context Par1
incSize = context Par1
-> CircuitFun Par1 Par1 (BaseField context) -> context Par1
forall (f :: Type -> Type) (g :: Type -> Type).
context f -> CircuitFun f g (BaseField context) -> context g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun f g (BaseField c) -> c g
fromCircuitF context Par1
lSize (\(Par1 i
s) -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i (BaseField context) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
s x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
forall a. MultiplicativeMonoid a => a
one))

uncons
    :: forall context x
    .  Symbolic context
    => SymbolicData x
    => Applicative (Layout x)
    => Traversable (Layout x)
    => Representable (Layout x)
    => Zip (Layout x)
    => SymbolicData (List context x) -- TODO: Implement this
    => Representable (Layout (List context x))
    => Traversable (Layout (List context x))
    => Context x ~ context
    => Context (List context x) ~ context
    => Support x ~ Proxy context
    => List context x
    -> (x, List context x)
uncons :: forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, SymbolicData x, Applicative (Layout x),
 Traversable (Layout x), Representable (Layout x), Zip (Layout x),
 SymbolicData (List context x),
 Representable (Layout (List context x)),
 Traversable (Layout (List context x)), Context x ~ context,
 Context (List context x) ~ context, Support x ~ Proxy context) =>
List context x -> (x, List context x)
uncons List context x
l = (List context x -> x
forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, Applicative (Layout x), Traversable (Layout x),
 Representable (Layout x), Zip (Layout x), SymbolicData x,
 Context x ~ context, Support x ~ Proxy context) =>
List context x -> x
head List context x
l, List context x -> List context x
forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, Applicative (Layout x), Traversable (Layout x),
 Zip (Layout x), SymbolicData x, SymbolicData (List context x),
 Representable (Layout (List context x)),
 Traversable (Layout (List context x)), Context x ~ context,
 Context (List context x) ~ context, Support x ~ Proxy context) =>
List context x -> List context x
tail List context x
l)

-- | TODO: Is there really a nicer way to handle empty lists?
--
head
    :: forall context x
    .  Symbolic context
    => Applicative (Layout x)
    => Traversable (Layout x)
    => Representable (Layout x)
    => Zip (Layout x)
    => SymbolicData x
    => Context x ~ context
    => Support x ~ Proxy context
    => List context x -> x
head :: forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, Applicative (Layout x), Traversable (Layout x),
 Representable (Layout x), Zip (Layout x), SymbolicData x,
 Context x ~ context, Support x ~ Proxy context) =>
List context x -> x
head xs :: List context x
xs@List{context Par1
context (Layout x)
[x]
lHash :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context (Layout x)
lSize :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context Par1
lWitness :: forall (context :: (Type -> Type) -> Type) x. List context x -> [x]
lHash :: context (Layout x)
lSize :: context Par1
lWitness :: [x]
..} = x -> x -> Bool context -> x
forall b a. Conditional b a => a -> a -> b -> a
bool ((Support x -> Context x (Layout x)) -> x
forall x.
SymbolicData x =>
(Support x -> Context x (Layout x)) -> x
restore ((Support x -> Context x (Layout x)) -> x)
-> (Support x -> Context x (Layout x)) -> x
forall a b. (a -> b) -> a -> b
$ \Support x
_ -> context (Layout x)
Context x (Layout x)
unsafeHead) ((Support x -> Context x (Layout x)) -> x
forall x.
SymbolicData x =>
(Support x -> Context x (Layout x)) -> x
restore ((Support x -> Context x (Layout x)) -> x)
-> (Support x -> Context x (Layout x)) -> x
forall a b. (a -> b) -> a -> b
$ \Support x
_ -> Layout x (BaseField (Context x)) -> Context x (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Layout x (BaseField (Context x)) -> Context x (Layout x))
-> Layout x (BaseField (Context x)) -> Context x (Layout x)
forall a b. (a -> b) -> a -> b
$ BaseField context -> Layout x (BaseField context)
forall a. a -> Layout x a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BaseField context
forall a. AdditiveMonoid a => a
zero) (List context x -> Bool context
forall (context :: (Type -> Type) -> Type) x.
Symbolic context =>
List context x -> Bool context
null List context x
xs)
    where
        xRepr :: context (Layout x)
        xRepr :: context (Layout x)
xRepr = case [x]
lWitness of
                  (x
x:[x]
_) -> x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces x
x Proxy context
Support x
forall {k} (t :: k). Proxy t
Proxy
                  [x]
_     -> Layout x (BaseField context) -> context (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Layout x (BaseField context) -> context (Layout x))
-> Layout x (BaseField context) -> context (Layout x)
forall a b. (a -> b) -> a -> b
$ BaseField context -> Layout x (BaseField context)
forall a. a -> Layout x a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BaseField context
forall a. AdditiveMonoid a => a
zero

        -- | Head is a circuit comprised of variables satisfying the equation for prepending (i.e. (.:))
        -- We have to pass witnesses to it as well.
        --
        unsafeHead :: context (Layout x)
        unsafeHead :: context (Layout x)
unsafeHead = context (Layout x)
-> context (Layout x)
-> context Par1
-> (forall {i} {m :: Type -> Type}.
    MonadCircuit i (BaseField context) m =>
    Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type) (k :: Type -> Type).
Symbolic c =>
c f
-> c g
-> c h
-> (forall i (m :: Type -> Type).
    MonadCircuit i (BaseField c) m =>
    f i -> g i -> h i -> m (k i))
-> c k
fromCircuit3F context (Layout x)
lHash context (Layout x)
xRepr context Par1
lSize ((forall {i} {m :: Type -> Type}.
  MonadCircuit i (BaseField context) m =>
  Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
 -> context (Layout x))
-> (forall {i} {m :: Type -> Type}.
    MonadCircuit i (BaseField context) m =>
    Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x)
forall a b. (a -> b) -> a -> b
$
            \Layout x i
vHash Layout x i
vRepr (Par1 i
s) -> (i -> i -> m i) -> Layout x i -> Layout x i -> m (Layout x i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM (\i
h i
r -> NewConstraint i (BaseField context)
-> Witness i (BaseField context) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
NewConstraint var a -> Witness var a -> m var
newConstrained (\i -> x
p i
v -> i -> x
p i
h x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
p i
v x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* (i -> x
p i
s x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ x
forall a. MultiplicativeMonoid a => a
one)) ((i -> x) -> i -> x
forall a b. (a -> b) -> a -> b
$ i
r)) Layout x i
vHash Layout x i
vRepr

tail
    :: forall context x
    .  Symbolic context
    => Applicative (Layout x)
    => Traversable (Layout x)
    => Zip (Layout x)
    => SymbolicData x
    => SymbolicData (List context x) -- TODO: Implement this
    => Representable (Layout (List context x))
    => Traversable (Layout (List context x))
    => Context x ~ context
    => Context (List context x) ~ context
    => Support x ~ Proxy context
    => List context x
    -> List context x
tail :: forall (context :: (Type -> Type) -> Type) x.
(Symbolic context, Applicative (Layout x), Traversable (Layout x),
 Zip (Layout x), SymbolicData x, SymbolicData (List context x),
 Representable (Layout (List context x)),
 Traversable (Layout (List context x)), Context x ~ context,
 Context (List context x) ~ context, Support x ~ Proxy context) =>
List context x -> List context x
tail xs :: List context x
xs@List{context Par1
context (Layout x)
[x]
lHash :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context (Layout x)
lSize :: forall (context :: (Type -> Type) -> Type) x.
List context x -> context Par1
lWitness :: forall (context :: (Type -> Type) -> Type) x. List context x -> [x]
lHash :: context (Layout x)
lSize :: context Par1
lWitness :: [x]
..} = List context x -> List context x -> Bool context -> List context x
forall b a. Conditional b a => a -> a -> b -> a
bool List context x
unsafeTail List context x
xs (List context x -> Bool context
forall (context :: (Type -> Type) -> Type) x.
Symbolic context =>
List context x -> Bool context
null List context x
xs)
    where
        tailId :: [a] -> [a]
        tailId :: forall a. [a] -> [a]
tailId []      = []
        tailId (a
_:[a]
xs') = [a]
xs'

        unsafeTail :: List context x
        unsafeTail :: List context x
unsafeTail = context (Layout x) -> context Par1 -> [x] -> List context x
forall (context :: (Type -> Type) -> Type) x.
context (Layout x) -> context Par1 -> [x] -> List context x
List context (Layout x)
decSum context Par1
decSize ([x] -> [x]
forall a. [a] -> [a]
tailId [x]
lWitness)

        xRepr :: context (Layout x)
        xRepr :: context (Layout x)
xRepr = case [x]
lWitness of
                  (x
x:[x]
_) -> x -> Support x -> Context x (Layout x)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
pieces x
x Proxy context
Support x
forall {k} (t :: k). Proxy t
Proxy
                  [x]
_     -> Layout x (BaseField context) -> context (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Symbolic c, Functor f) =>
f (BaseField c) -> c f
embed (Layout x (BaseField context) -> context (Layout x))
-> Layout x (BaseField context) -> context (Layout x)
forall a b. (a -> b) -> a -> b
$ BaseField context -> Layout x (BaseField context)
forall a. a -> Layout x a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure BaseField context
forall a. AdditiveMonoid a => a
zero

        decSum :: context (Layout x)
        decSum :: context (Layout x)
decSum = context (Layout x)
-> context (Layout x)
-> context Par1
-> (forall {i} {m :: Type -> Type}.
    MonadCircuit i (BaseField context) m =>
    Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type) (h :: Type -> Type) (k :: Type -> Type).
Symbolic c =>
c f
-> c g
-> c h
-> (forall i (m :: Type -> Type).
    MonadCircuit i (BaseField c) m =>
    f i -> g i -> h i -> m (k i))
-> c k
fromCircuit3F context (Layout x)
lHash context (Layout x)
xRepr context Par1
lSize ((forall {i} {m :: Type -> Type}.
  MonadCircuit i (BaseField context) m =>
  Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
 -> context (Layout x))
-> (forall {i} {m :: Type -> Type}.
    MonadCircuit i (BaseField context) m =>
    Layout x i -> Layout x i -> Par1 i -> m (Layout x i))
-> context (Layout x)
forall a b. (a -> b) -> a -> b
$
            \Layout x i
vHash Layout x i
vRepr (Par1 i
s) -> (i -> i -> m i) -> Layout x i -> Layout x i -> m (Layout x i)
forall (f :: Type -> Type) (m :: Type -> Type) a b c.
(Traversable f, Zip f, Applicative m) =>
(a -> b -> m c) -> f a -> f b -> m (f c)
zipWithM (\i
h i
r -> ClosedPoly i (BaseField context) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
h x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
p i
r x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
p i
s)) Layout x i
vHash Layout x i
vRepr

        decSize :: context Par1
        decSize :: context Par1
decSize = context Par1
-> CircuitFun Par1 Par1 (BaseField context) -> context Par1
forall (f :: Type -> Type) (g :: Type -> Type).
context f -> CircuitFun f g (BaseField context) -> context g
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type)
       (g :: Type -> Type).
Symbolic c =>
c f -> CircuitFun f g (BaseField c) -> c g
fromCircuitF context Par1
lSize (\(Par1 i
s) -> i -> Par1 i
forall p. p -> Par1 p
Par1 (i -> Par1 i) -> m i -> m (Par1 i)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ClosedPoly i (BaseField context) -> m i
forall var a (m :: Type -> Type).
MonadCircuit var a m =>
ClosedPoly var a -> m var
newAssigned (\i -> x
p -> i -> x
p i
s x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- x
forall a. MultiplicativeMonoid a => a
one))

{-- TODO: Foldable relies on Haskell types such as Bool (i.e. null = foldr (\_ _ -> False) True)
   I am not sure this is suitable for Symbolic interface

reverse :: forall context x . Foldable (List context) => List context x -> List context x
reverse = foldl (flip (.:)) emptyList

init :: forall context x . Foldable (List context) => List context x -> List context x
init = reverse . tail . reverse

last :: forall context x . Foldable (List context) => List context x -> x
last = head . reverse
--}
last :: List context x -> x
last :: forall (context :: (Type -> Type) -> Type) x. List context x -> x
last = List context x -> x
forall a. HasCallStack => a
undefined

(++) :: List context x -> List context x -> List context x
List context x
_ ++ :: forall (context :: (Type -> Type) -> Type) x.
List context x -> List context x -> List context x
++ List context x
_ = List context x
forall a. HasCallStack => a
undefined

filter ::
       (x -> Bool context)
    -> List context x
    -> List context x
filter :: forall x (context :: (Type -> Type) -> Type).
(x -> Bool context) -> List context x -> List context x
filter = (x -> Bool context) -> List context x -> List context x
forall a. HasCallStack => a
undefined

delete :: x -> List context x -> List context x
delete :: forall x (context :: (Type -> Type) -> Type).
x -> List context x -> List context x
delete = x -> List context x -> List context x
forall a. HasCallStack => a
undefined

(\\) :: List context x -> List context x -> List context x
List context x
_ \\ :: forall (context :: (Type -> Type) -> Type) x.
List context x -> List context x -> List context x
\\ List context x
_ = List context x
forall a. HasCallStack => a
undefined