Frex.Algebra

Algebras for a `Frex.Signature` and associated definitions

Reexports

import public Notation
import public Notation.Semantic
import public Data.Vect
import public Data.Vect.Elem
import public Data.Vect.Properties
import public Data.Rel

Definitions

(^) : Type -> Nat -> Type

  N-ary tuples

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 10

curry : (a ^ n -> a) -> ary n a

  Curry a function from n-tuples to an n-ary function

Totality: total
Visibility: public export

uncurry : ary n a -> a ^ n -> a

  Uncurry an n-ary function into a function from n-tuples

Totality: total
Visibility: public export

uncurryCurryId : (f : (a ^ n -> a)) -> (xs : a ^ n) -> uncurry (curry f) xs = f xs

Totality: total
Visibility: export

algebraOver : Signature -> Type -> Type

  States: each operation has an interpretation

Totality: total
Visibility: public export

algebraOver' : Signature -> Type -> Type

Totality: total
Visibility: public export

record Algebra : Signature -> Type

  An algebra for a signature Sig consists of:
  @U : A type called the carrier
  @Sem : a semantic interpretation for each Sig-operation
  The smart constructor `MkAlgebra` is more usable in concrete cases

Totality: total
Visibility: public export
Constructor:

MakeAlgebra : {0 Sig : Signature} -> (0 U : Type) -> algebraOver Sig U -> Algebra Sig

Projections:

.Semantics : {0 Sig : Signature} -> ({rec:0} : Algebra Sig) -> algebraOver Sig (U {rec:0})
0 .U : {0 Sig : Signature} -> Algebra Sig -> Type

Hints:

Cast (Algebra sig) (SetoidAlgebra sig)
Semantic (Algebra sig) (Op sig)
Semantic (Algebra sig) (Term sig x)

0 .U : {0 Sig : Signature} -> Algebra Sig -> Type

Totality: total
Visibility: public export

0 U : {0 Sig : Signature} -> Algebra Sig -> Type

Totality: total
Visibility: public export

.Semantics : {0 Sig : Signature} -> ({rec:0} : Algebra Sig) -> algebraOver Sig (U {rec:0})

Totality: total
Visibility: public export

Semantics : {0 Sig : Signature} -> ({rec:0} : Algebra Sig) -> algebraOver Sig (U {rec:0})

Totality: total
Visibility: public export

MkAlgebra : (0 U : Type) -> algebraOver' sig U -> Algebra sig

  Smart constructor for an algebra for a signature Sig:
  @U : A type called the carrier
  @Sem : a semantic interpretation for each Sig-operation

Totality: total
Visibility: public export

data Term : (0 _ : Signature) -> Type -> Type

  Algebraic terms of this signature with variables in the given type

Totality: total
Visibility: public export
Constructors:

Done : a -> Term sig a

  A variable with the given index

Call : (f : Op sig) -> Vect (arity f) (Term sig a) -> Term sig a

  An operator, applied to a vector of sub-terms

Hints:

Applicative (Term sig)
(DecEq (Op sig), DecEq a) => DecEq (Term sig a)
(Eq (Op sig), Eq a) => Eq (Term sig a)
Functor (Term sig)
Monad (Term sig)
(Ord (Op sig), Ord a) => Ord (Term sig a)
pres .signature = sig => Semantic (a <~.~> b) (Term sig y)
pres .signature = sig => Semantic (Coproduct a b) (Term sig y)
pres .signature = sig => Semantic (Extension a x) (Term sig y)
pres .signature = sig => Semantic (Frex a x) (Term sig y)
pres .signature = sig => Semantic (Model pres) (Term sig x)
pres .signature = sig => Semantic (ModelOver pres x) (Term sig y)
pres .signature = sig => Semantic (Free pres x) (Term sig y)
Semantic (Algebra sig) (Term sig x)
Semantic (SetoidAlgebra sig) (Term sig x)
Show (FreePresetoid sig x u v)
Uninhabited (Done x = Call f xs)
Uninhabited (Call f xs = Done x)

withParens : Printer sig a -> Printer sig a

  Print parens (but not at the toplevel)

Totality: total
Visibility: export

withNames : Printer sig () -> Printer sig (Fin n)

Totality: total
Visibility: export

withFocus : String -> Printer sig a -> Printer sig (Maybe a)

Totality: total
Visibility: export

withVal : Printer sig a -> Printer sig a

Totality: total
Visibility: export

displayPrec : Printer sig a -> Prec -> Term sig a -> Doc ()

Totality: total
Visibility: export

display : Printer sig a -> Term sig a -> Doc ()

Totality: total
Visibility: export

withNesting : Printer sig a -> Printer sig (Term sig a)

  This printer assumes there's at least one layer of term above
  the nested one i.e. you can't have just `Done t`.

Totality: total
Visibility: export

bindTerm : {auto a : Algebra sig} -> Term sig x -> (x -> U a) -> U a

Totality: total
Visibility: public export

bindTerms : {auto a : Algebra sig} -> Vect n (Term sig x) -> (x -> U a) -> Vect n (U a)

Totality: total
Visibility: public export

bindTermsIsMap : {auto a : Algebra sig} -> (xs : Vect n (Term sig x)) -> (env : (x -> U a)) -> bindTerms xs env = map (flip (a .Sem) env) xs

  Specifies `bindTerms` specialises `map bindTerm`.

Totality: total
Visibility: export

Free : (0 sig : Signature) -> (0 _ : Type) -> Algebra sig

  The free `sig`-algebra over over a given type

Totality: total
Visibility: public export

call : sig .OpWithArity n -> ary n (Term sig x)

  The corresponding  n-ary operation over the term algebra

Totality: total
Visibility: public export

X : Fin k -> Term sig (Fin k)

  Smart constructor for variables

Totality: total
Visibility: public export

cast : Term sig (Maybe a) -> Term sig (Either a (Fin 1))

  Converting a focus to a term with one free variable

Totality: total
Visibility: public export

TermAlgebra : (0 sig : Signature) -> Nat -> Algebra sig

  Free `sig`-algebra over `n`-variables.

Totality: total
Visibility: public export

bindTermsPureRightUnit : (ts : Vect n (Term sig x)) -> bindTerms ts pure = ts

Totality: total
Visibility: export

bindPureRightUnit : (t : Term sig x) -> t >>= pure = t

  Monad law corresponding to right unit law of monoids

Totality: total
Visibility: export

0 CongruenceWRT : (a : Setoid) -> (U a ^ n -> U a) -> Type

  The equivalence relation on `a` is a congruence w.r.t. the operation `f`.

Totality: total
Visibility: public export

EqualCongruence : (f : (a ^ n -> a)) -> CongruenceWRT (cast a) f

  Equality is always a congruence

Totality: total
Visibility: export

record SetoidAlgebra : Signature -> Type

  A setoid algebra: an algebra over a setoid whose equivalence
  relation respects all the algebraic operations

Totality: total
Visibility: public export
Constructor:

MkSetoidAlgebra : {0 Sig : Signature} -> (algebra : Algebra Sig) -> (equivalence : Equivalence (U algebra)) -> ((f : Op Sig) -> CongruenceWRT (MkSetoid (U algebra) equivalence) (algebra .Sem f)) -> SetoidAlgebra Sig

Projections:

.algebra : {0 Sig : Signature} -> SetoidAlgebra Sig -> Algebra Sig

  Underlying algebra

.congruence : {0 Sig : Signature} -> ({rec:0} : SetoidAlgebra Sig) -> (f : Op Sig) -> CongruenceWRT (MkSetoid (U (algebra {rec:0})) (equivalence {rec:0})) ((algebra {rec:0}) .Sem f)

  All algebraic operations respect the equivalence relation

.equivalence : {0 Sig : Signature} -> ({rec:0} : SetoidAlgebra Sig) -> Equivalence (U (algebra {rec:0}))

  Equivalence relation making the carrier a setoid

Hints:

Cast (SetoidAlgebra sig) Setoid
Cast (Algebra sig) (SetoidAlgebra sig)
Cast (a <~> b) (a ~> b)
Cast (SetoidAlgebra sig) (PresetoidAlgebra sig)
Semantic (SetoidAlgebra sig) (Op sig)
Semantic (SetoidAlgebra sig) (Term sig x)

.algebra : {0 Sig : Signature} -> SetoidAlgebra Sig -> Algebra Sig

  Underlying algebra

Totality: total
Visibility: public export

algebra : {0 Sig : Signature} -> SetoidAlgebra Sig -> Algebra Sig

  Underlying algebra

Totality: total
Visibility: public export

.equivalence : {0 Sig : Signature} -> ({rec:0} : SetoidAlgebra Sig) -> Equivalence (U (algebra {rec:0}))

  Equivalence relation making the carrier a setoid

Totality: total
Visibility: public export

equivalence : {0 Sig : Signature} -> ({rec:0} : SetoidAlgebra Sig) -> Equivalence (U (algebra {rec:0}))

  Equivalence relation making the carrier a setoid

Totality: total
Visibility: public export

.congruence : {0 Sig : Signature} -> ({rec:0} : SetoidAlgebra Sig) -> (f : Op Sig) -> CongruenceWRT (MkSetoid (U (algebra {rec:0})) (equivalence {rec:0})) ((algebra {rec:0}) .Sem f)

  All algebraic operations respect the equivalence relation

Totality: total
Visibility: public export

congruence : {0 Sig : Signature} -> ({rec:0} : SetoidAlgebra Sig) -> (f : Op Sig) -> CongruenceWRT (MkSetoid (U (algebra {rec:0})) (equivalence {rec:0})) ((algebra {rec:0}) .Sem f)

  All algebraic operations respect the equivalence relation

Totality: total
Visibility: public export

0 U : SetoidAlgebra sig -> Type

Totality: total
Visibility: public export

cast : (a : SetoidAlgebra sig) -> Preorder (U a) ((a .equivalence) .relation)

Totality: total
Visibility: public export

cast : (f : Op sig) -> VectSetoid (arity f) (cast a) ~> cast a

Totality: total
Visibility: public export

0 Preserves : (a : SetoidAlgebra sig) -> (b : SetoidAlgebra sig) -> (U a -> U b) -> Op sig -> Type

  States: the function `h : U a -> U b` preserves the `sig`-operation `f`

Totality: total
Visibility: public export

0 Homomorphism : (a : SetoidAlgebra sig) -> (b : SetoidAlgebra sig) -> (U a -> U b) -> Type

  States: the function `h : U a -> U b` preserves all `sig`-operations

Totality: total
Visibility: public export

record (~>) : {Sig : Signature} -> SetoidAlgebra Sig -> SetoidAlgebra Sig -> Type

  Homomorphisms between Setoid `Sig`-algebras
  @H : setoid morphism between the carriers
  @preserves : satisfying the homomorphism property

Totality: total
Visibility: public export
Constructor:

MkSetoidHomomorphism : {0 Sig : Signature} -> (H : cast a ~> cast b) -> Homomorphism a b (H .H) -> a ~> b

Projections:

.H : {0 Sig : Signature} -> a ~> b -> cast a ~> cast b

  Underlying Setoid homomorphism

.preserves : {0 Sig : Signature} -> ({rec:0} : a ~> b) -> Homomorphism a b ((H {rec:0}) .H)

  Preservation of `Sig`-operations up to the setoid's equivalence

Hint:

Cast (a <~> b) (a ~> b)

Fixity Declarations:
infix operator, level 5
infix operator, level 5
infix operator, level 5

.H : {0 Sig : Signature} -> a ~> b -> cast a ~> cast b

  Underlying Setoid homomorphism

Totality: total
Visibility: public export

H : {0 Sig : Signature} -> a ~> b -> cast a ~> cast b

  Underlying Setoid homomorphism

Totality: total
Visibility: public export

.preserves : {0 Sig : Signature} -> ({rec:0} : a ~> b) -> Homomorphism a b ((H {rec:0}) .H)

  Preservation of `Sig`-operations up to the setoid's equivalence

Totality: total
Visibility: public export

preserves : {0 Sig : Signature} -> ({rec:0} : a ~> b) -> Homomorphism a b ((H {rec:0}) .H)

  Preservation of `Sig`-operations up to the setoid's equivalence

Totality: total
Visibility: public export

id : (a : SetoidAlgebra sig) -> a ~> a

Totality: total
Visibility: public export

(.) : b ~> c -> a ~> b -> a ~> c

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9

0 (~>) : Algebra sig -> Algebra sig -> Type

Totality: total
Visibility: public export
Fixity Declarations:
infix operator, level 5
infix operator, level 5
infix operator, level 5

bindHom : (env : (x -> U a)) -> Homomorphism (cast (Free sig x)) (cast a) (flip bindTerm env)

  States: `(>>= f) : Free sig x -> a` is an algebra homomorphism

Totality: total
Visibility: export

eval : {auto a : Algebra sig} -> (x -> U a) -> Free sig x ~> a

  Like Algebra.(>>=), but pack the `sig`-homomorphism structure

Totality: total
Visibility: public export

bindAssociative : {auto a : Algebra sig} -> (t : Term sig x) -> (f : (x -> Term sig y)) -> (g : (y -> U a)) -> bindTerm (bindTerm t f) g = bindTerm t (\i => bindTerm (f i) g)

Totality: total
Visibility: public export

bindTermsAssociative : {auto a : Algebra sig} -> (ts : Vect n (Term sig x)) -> (f : (x -> Term sig y)) -> (g : (y -> U a)) -> bindTerms (bindTerms ts f) g = bindTerms ts (\x => bindTerm (f x) g)

Totality: total
Visibility: public export

bindCongruence : (t : Term sig (U x)) -> SetoidHomomorphism (x ~~> cast a) (cast a) (\u => bindTerm t (u .H))

  The setoid equivalence is a congruence wrt. all algebraic terms

Totality: total
Visibility: export

bindTermsCongruence : (ts : Vect n (Term sig (U x))) -> SetoidHomomorphism (x ~~> cast a) (VectSetoid n (cast a)) (\u => bindTerms ts (u .H))

  Auxiliary function used in the inductive argument for `bindCongruence`

Totality: total
Visibility: export

eval : Term sig (U x) -> (x ~~> cast a) ~> cast a

  Evaluation of algebraic terms in a SetoidAlgebra is a setoid homomorphism

Totality: total
Visibility: public export

0 Preserves : (a : SetoidAlgebra sig) -> (b : SetoidAlgebra sig) -> (U a -> U b) -> Term sig x -> Type

  Every term over x induces an `x`-ary operation.
  States: `h` preserves the this operation.

Totality: total
Visibility: public export

homoPreservesSem : (h : a ~> b) -> (t : Term sig x) -> Preserves a b ((h .H) .H) t

  Homomorphism preserve all algebraic operations

Totality: total
Visibility: public export

homoPreservesSemMap : (h : a ~> b) -> (ts : Vect n (Term sig x)) -> (env : (x -> U a)) -> ((VectSetoid n (cast b)) .equivalence) .relation (map ((h .H) .H) (bindTerms ts env)) (bindTerms ts ((h .H) .H . env))

  Auxiliary generalisation to prove `homoPreservesSem`.

Totality: total
Visibility: public export

record (<~>) : SetoidAlgebra sig -> SetoidAlgebra sig -> Type

Totality: total
Visibility: public export
Constructor:

MkIsomorphism : (Iso : cast a <~> cast b) -> Homomorphism a b ((Iso .Fwd) .H) -> a <~> b

Projections:

.FwdHomo : ({rec:0} : a <~> b) -> Homomorphism a b (((Iso {rec:0}) .Fwd) .H)
.Iso : a <~> b -> cast a <~> cast b

Hint:

Cast (a <~> b) (a ~> b)

Fixity Declarations:
infix operator, level 5
infix operator, level 5

.Iso : a <~> b -> cast a <~> cast b

Totality: total
Visibility: public export

Iso : a <~> b -> cast a <~> cast b

Totality: total
Visibility: public export

.FwdHomo : ({rec:0} : a <~> b) -> Homomorphism a b (((Iso {rec:0}) .Fwd) .H)

Totality: total
Visibility: public export

FwdHomo : ({rec:0} : a <~> b) -> Homomorphism a b (((Iso {rec:0}) .Fwd) .H)

Totality: total
Visibility: public export

BwdHomo : (a : SetoidAlgebra sig) -> (b : SetoidAlgebra sig) -> (iso : a <~> b) -> Homomorphism b a (((iso .Iso) .Bwd) .H)

Totality: total
Visibility: public export

sym : a <~> b -> b <~> a

  Reverse an isomorphism

Totality: total
Visibility: public export

(~~>) : SetoidAlgebra sig -> SetoidAlgebra sig -> Setoid

  The setoid of homomorphisms between algebras with pointwise equivalence.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 5

.sem : (a : SetoidAlgebra sig) -> sig .OpWithArity n -> ary n (U a)

  nary interpretation of an operator in an algebra

Totality: total
Visibility: public export

callEqSem : (a : Algebra sig) -> (op : Op sig) -> (xs : Vect (arity op) (U a)) -> bindTerm (Call op (tabulate Done)) (\i => index i xs) = a .Sem op xs

  Each operation in the signature is an algebraic operation

Totality: total
Visibility: public export

record (~>) : Signature -> Signature -> Type

Totality: total
Visibility: public export
Constructor:

MkSignatureMorphism : (sig1 .OpWithArity n -> Term sig2 (Fin n)) -> sig1 ~> sig2

Projection:

.H : sig1 ~> sig2 -> sig1 .OpWithArity n -> Term sig2 (Fin n)

Hint:

sig1 ~> sig2 => Cast (Equation sig1) (Equation sig2)

Fixity Declarations:
infix operator, level 5
infix operator, level 5
infix operator, level 5

.H : sig1 ~> sig2 -> sig1 .OpWithArity n -> Term sig2 (Fin n)

Totality: total
Visibility: public export

H : sig1 ~> sig2 -> sig1 .OpWithArity n -> Term sig2 (Fin n)

Totality: total
Visibility: public export

OpTranslation : (sig1 .OpWithArity n -> sig2 .OpWithArity n) -> sig1 ~> sig2

Totality: total
Visibility: public export

cast : sig1 ~> sig2 => Term sig1 a -> Term sig2 a

Totality: total
Visibility: public export

castTerms : sig1 ~> sig2 -> Vect k (Term sig1 a) -> Vect k (Term sig2 a)

Totality: total
Visibility: public export