ZkFold.Symbolic.Data.Morph

Documentation

type Replica c t u = (SymbolicOutput u, Context u ~ c, Layout u ~ Layout t, Payload u ~ Payload t)

A type u is a Replica of type t in context c iff: * it is SymbolicOutput; * its context is c; * its representation (layout and payload) match those of t.

data MorphTo c input output

A function is a "morph" of a function of type input -> output to context c iff it is a function of type i -> o for some Replicas i, o of input and output, correspondingly, in context c.

Constructors

forall i o.(Replica c input i, Replica c output o) => Morph (i -> o)

(@) :: (Replica c input i, Replica c output o) => MorphTo c input output -> i -> o

One can apply a morph of a function input -> output in context c if they provide Replicas of input and output in context c.

type MorphFrom ctx input output = forall c. (SymbolicFold c, BaseField c ~ BaseField ctx) => MorphTo c input output

A function is a "morph" of a function of type input -> output from context ctx iff, for each context c over same base field, it is a morph to c.

Thus, if a function is MorphFrom, it can be * safely passed through parametricity boundary set by sfoldl; * applied there in an anonymous context to an argument.