| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
ZkFold.Symbolic.Data.Morph
Synopsis
- type Replica c t u = (SymbolicOutput u, Context u ~ c, Layout u ~ Layout t, Payload u ~ Payload t)
- data MorphTo c input output = 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
- type MorphFrom ctx input output = forall c. (SymbolicFold c, BaseField c ~ BaseField ctx) => MorphTo c input output
Documentation
type Replica c t u = (SymbolicOutput u, Context u ~ c, Layout u ~ Layout t, Payload u ~ Payload t) Source #
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 Source #
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.
(@) :: (Replica c input i, Replica c output o) => MorphTo c input output -> i -> o Source #
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 Source #
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.