symbolic-base-0.1.0.0: ZkFold Symbolic compiler and zero-knowledge proof protocols
Safe HaskellSafe-Inferred
LanguageHaskell2010

ZkFold.Base.Control.HApplicative

Synopsis

Documentation

class HFunctor c => HApplicative c where Source #

A higher-order functor with application, providing operations to apply a function of type (forall a. f a -> g a -> ...) of arbitrary arity to arguments of corresponding types f a, g a, ...

Minimal complete definition

(hpure | hunit), (hap | hliftA2 | hpair)

Methods

hpure :: (forall a. f a) -> c f Source #

Lift a proxy functor into the structure. If hunit is specified instead, a default definition is available. The following is expected to hold:

Definition
hpure x == hmap (const x) hunit

hunit :: c U1 Source #

Lift a concrete proxy functor U1 into the structure. Note that it is almost always better to define hpure instead and rely on the default implementation of hunit. The following is expected to hold:

Definition
hunit == hpure U1

hap :: c (Transform f g) -> c f -> c g Source #

Sequential application. It is hard to find the legitimate usecase for this function; this is only provided for comparison with classic Applicative class.

The default definition is via hpair. The following is expected to hold:

Definition
hap t f == hmap (\(Transform g :*: x) -> g x) (hpair t x)

hliftA2 :: (forall a. f a -> g a -> h a) -> c f -> c g -> c h Source #

Applies a binary function of type (forall a. f a -> g a -> h a) to a pair of arguments of types c f and c g, yielding the result of type c h.

If hap is specified instead, a default definition is available. The following is expected to hold:

Definition
hliftA2 f x y == hap (hmap (Transform . f) x) y
Compatibility
hmap f x == hliftA2 (const f) hunit x

hpair :: c f -> c g -> c (f :*: g) Source #

Joins two structures, preserving the outputs. Note that it is almost always better to define hliftA2 instead and rely on the default implementation of hpair. The following is expected to hold:

Definition
hpair x y == hliftA2 (:*:) x y
Associativity
hliftA2 (\(a :*: b) c -> a :*: (b :*: c)) (hpair x y) z == hpair x (hpair y z)
Left identity
hliftA2 const x hunit == x
Right identity
hliftA2 (const id) hunit y == y

Instances

Instances details
Ord (Rep i) => HApplicative (ArithmeticCircuit a i :: (Type -> Type) -> Type) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

hpure :: (forall (a0 :: k). f a0) -> ArithmeticCircuit a i f Source #

hunit :: ArithmeticCircuit a i U1 Source #

hap :: forall (f :: k -> Type) (g :: k -> Type). ArithmeticCircuit a i (Transform f g) -> ArithmeticCircuit a i f -> ArithmeticCircuit a i g Source #

hliftA2 :: (forall (a0 :: k). f a0 -> g a0 -> h a0) -> ArithmeticCircuit a i f -> ArithmeticCircuit a i g -> ArithmeticCircuit a i h Source #

hpair :: forall (f :: k -> Type) (g :: k -> Type). ArithmeticCircuit a i f -> ArithmeticCircuit a i g -> ArithmeticCircuit a i (f :*: g) Source #

HApplicative (Interpreter a :: (k -> Type) -> Type) Source # 
Instance details

Defined in ZkFold.Symbolic.Interpreter

Methods

hpure :: (forall (a0 :: k0). f a0) -> Interpreter a f Source #

hunit :: Interpreter a U1 Source #

hap :: forall (f :: k0 -> Type) (g :: k0 -> Type). Interpreter a (Transform f g) -> Interpreter a f -> Interpreter a g Source #

hliftA2 :: (forall (a0 :: k0). f a0 -> g a0 -> h a0) -> Interpreter a f -> Interpreter a g -> Interpreter a h Source #

hpair :: forall (f :: k0 -> Type) (g :: k0 -> Type). Interpreter a f -> Interpreter a g -> Interpreter a (f :*: g) Source #

newtype Transform f g a Source #

A newtype wrapper for natural transformations used in hap definition.

Constructors

Transform 

Fields

hmapA :: HApplicative c => (forall a. f a -> g a) -> c f -> c g Source #

If hap and hpure do not rely on hmap (i.e. at least are not implemented by default), this function can be used to implement hmap.

hliftA1 :: HApplicative c => (forall a. f a -> g a) -> c f -> c g Source #

If hliftA2 and hunit do not rely on hmap (at least, hliftA2 is not implemented by default), this function can be used to implement hmap.

hliftA3 :: HApplicative c => (forall a. f a -> g a -> h a -> i a) -> c f -> c g -> c h -> c i Source #

Applies a ternary natural transformation to a triple of arguments behind an HApplicative.