anoma / geb Goto Github PK

Open the REPL (sbcl (terminal), M-x sly, M-x swank)
- For the terminal, this is just calling the common lisp implementation from the terminal.
  
  user@system:geb-directory % sbcl.
- For Emacs, this is simply calling either M-x sly or M-x slime if you are using either sly or slime
From Emacs: open geb.asd and press C-ck (sly-compile-and-load-file, or swank-compile-and-load-file if you are using swank).

Now that we have the file open, we can now load the system by writing:

;; only necessary for the first time!
(ql:quickload :geb/documentation)

;; if you want to load it in the future
(asdf:load-system :geb/documentation)

;; if you want to load the codbase and run tests at the same time
(asdf:test-system :geb/documentation)

;; if you want to run the tests once the system is loaded!
(geb-test:run-tests)

2.3 Geb as a binary

[in package GEB.ENTRY]

The standard way to use geb currently is by loading the code into one's lisp environment

(ql:quickload :geb)

However, one may be interested in running geb in some sort of compilation process, that is why we also give out a binary for people to use

An example use of this binary is as follows

mariari@Gensokyo % ./geb.image -i "foo.lisp" -e "geb.lambda.main::*entry*" -l -p -o "foo.pir"

mariari@Gensokyo % cat foo.pir
def entry x1 = {
  (x1)
};%
mariari@Gensokyo % ./geb.image -i "foo.lisp" -e "geb.lambda.main::*entry*" -l -p
def *entry* x {
  0
}

mariari@Gensokyo % ./geb.image -h
  -i --input                      string   Input geb file location
  -e --entry-point                string   The function to run, should be fully qualified I.E. geb::my-main
  -l --stlc                       boolean  Use the simply typed lambda calculus frontend
  -o --output                     string   Save the output to a file rather than printing
  -v --version                    boolean  Prints the current version of the compiler
  -p --vampir                     string   Return a vamp-ir expression
  -s --library                    boolean  Print standard library
  -h -? --help                    boolean  The current help message

mariari@Gensokyo % ./geb.image -v
0.3.2

starting from a file foo.lisp that has

any valid lambda form. Good examples can be found at the following section:

The Simply Typed Lambda Calculus model

with the term bound to some global variable

(in-package :geb.lambda.main)

(defparameter *entry*
  (lamb (list (coprod so1 so1))
        (index 0)))

inside of it.

The command needs an entry-point (-e or --entry-point), as we are simply call LOAD on the given file, and need to know what to translate.

from STLC, we expect the form to be wrapped in the GEB.LAMBDA.SPEC.TYPED which takes both the type and the value to properly have enough context to evaluate.

It is advised to bind this to a parameter like in our example as -e expects a symbol.

the -l flag means that we are not expecting a geb term, but rather a lambda frontend term, this is to simply notify us to compile it as a lambda term rather than a geb term. In time this will go away

The flag -s prints the standard library the compiler uses. If -p is used alongside it, the standard library gets printed before the compiled circuit.

The flag -t after -p signals that the user wants to make an automatically generated test equality. Given a compiled VampIR function with name foo and arguments x1...xn prints an equality as foo x1 ... xn = y

[function] COMPILE-DOWN &KEY VAMPIR STLC ENTRY LIBRARY TEST (STREAM *STANDARD-OUTPUT*)

3 Glossary

[glossary-term] closed type

A closed type is a type that can not be extended dynamically. A good example of this kind of term is an ML ADT.
```
data Tree = Empty
          | Leaf Int
          | Node Tree Tree
```
In our lisp code we have a very similar convention:
```
(in-package :geb.spec)

(deftype substmorph ()
  `(or substobj
       alias
       comp init terminal case pair distribute
       inject-left inject-right
       project-left project-right))
```
This type is closed, as only one of GEB:SUBSTOBJ, GEB:INJECT-LEFT, GEB:INJECT-RIGHT etc can form the GEB:SUBSTMORPH type.

The main benefit of this form is that we can be exhaustive over what can be found in GEB:SUBSTMORPH.
```
(defun so-hom-obj (x z)
  (match-of substobj x
    (so0          so1)
    (so1          z)
    (alias        (so-hom-obj (obj x) z))
    ((coprod x y) (prod (so-hom-obj x z)
                        (so-hom-obj y z)))
    ((prod x y)   (so-hom-obj x (so-hom-obj y z)))))
```
If we forget a case, like GEB:COPROD it wanrs us with an non exhaustion warning.

Meaning that if we update definitions this works well.

The main downside is that we can not extend the type after the fact, meaning that all interfaces on SO-HOM-OBJ must take the unaltered type. This is in stark contrast to open types. To find out more about the trade offs and usage in the code-base read the section Open Types versus Closed Types.

[glossary-term] open type

An open type is a type that can be extended by user code down the line. A good example of this in ML is the type class system found in Haskell.

In our code base, it is simple as creating a Common Lisp Object System (CLOS) term
```
(defclass <substobj> (direct-pointwise-mixin) ())
```
and to create a child of it all we need to do is.
```
(defclass so0 (<substobj>) ())
```
Now any methods on GEB:<SUBSTOBJ> will cover GEB:SO0(0 1).

The main disadvantage of these is that exhaustion can not be checked, and thus the user has to know what methods to fill out. In a system with a bit more checks this is not a problem in practice. To find out more about the trade offs and usage in the code-base read the section Open Types versus Closed Types.

[glossary-term] Common Lisp Object System (CLOS)

The object system found in CL. Has great features like a Meta Object Protocol that helps it facilitate extensions.

4 Original Efforts

Originally GEB started off as an Idris codebase written by the designer and creator of GEB, Terence Rokop, However further efforts spawned for even further formal verification by Artem Gureev. Due to this, we have plenty of code not in Common Lisp that ought to be a good read.

4.1 Geb's Idris Code

The Idris folder can be found in the geb-idris folder provided in the codebase

At the time of this document, there is over 16k lines of Idris code written. This serves as the bulk of the POC that is GEB and is a treasure trove of interesting information surrounding category theory.

4.2 Geb's Agda Code

The Agda folder can be found in the geb-agda folder provided in the codebase

The Agda codebase serves as a great place to view formally verified properties about the GEB project. Although Geb's Idris Code is written in a dependently typed language, it serves as reference example of GEB, while Geb's Agda Code serves as the mathematical formalism proving various conjectures about GEB

5 Categorical Model

Geb is organizing programming language concepts (and entities!) using category theory, originally developed by mathematicians, but very much alive in programming language theory. Let us look at a simple well-known example: the category of sets and functions. It is the bread and butter example: sets $A,B,C,…$ play the role of objects, functions are arrows between objects $A—f→B$, and the latter compose as functions do, such that every path of matching functions $$A—f→B—g→C—h→D$$ composes to a corresponding composite function $$A—f;g;h→D$$ (or $h∘g∘f$ if you prefer) and we enjoy the luxury of not having to worry about the order in which we compose; for the sake of completeness, there are identify functions $A —\mathrm{id}_A→ A$ on each set $A$, serving as identities (which correspond to the composite of the empty path on an object). Sets and functions together form a category—based on function composition; thus, let's call this category sets-'n'-functions. This example, even “restricted” to finite sets-'n'-functions, will permeate through Geb.

One of the first lessons (in any introduction to category theory) about sets-'n'-functions is the characterization of products and disjoint sums of sets in terms of functions alone, i.e., without ever talking about elements of sets. Products and co-products are the simplest examples of universal constructions. One of the first surprises follows suit when we generalize functions to partial functions, relations, or even multi-relations: we obtain very different categories! For example, in the category sets-'n'-relations, the disjoint union of sets features as both a product and a co-product, as a categorical construction.

Do not fear! The usual definition of products in terms of elements of sets are absolutely compatible with the universal construction in sets-'n'-functions. However we gain the possibility to compare the “result” of the universal constructions in sets-'n'-functions with the one in sets-'n'-relations (as both actually do have products).

for the purposes of Geb, many things can be expressed in analogy to the category of sets-'n'-functions; thus a solid understanding of the latter will be quite useful. In particular, we shall rely on the following universal constructions:

The construction of binary products $A × B$ of sets $A,B$, and the empty product $mathsf{1}$.
The construction of “function spaces” $B^A$ of sets $A,B$, called exponentials, i.e., collections of functions between pairs of sets.
The so-called currying of functions, $C^{(B^A)} cong C^{(A × B)}$, such that providing several arguments to a function can done either simultaneously, or in sequence.
The construction of sums (a.k.a. co-products) $A + B$ of sets $A,B$, corresponding to forming disjoint unions of sets; the empty sum is $varnothing$.

Product, sums and exponentials are the (almost) complete tool chest for writing polynomial expressions, e.g., $$Ax^{sf 2} +x^{sf 1} - Dx^{sf 0}.$$ (We need these later to define “algebraic data types”.) In the above expression, we have sets instead of numbers/constants where $ mathsf{2} = lbrace 1, 2 rbrace$, $ mathsf{1} = lbrace 1 rbrace$, $ mathsf{0} = lbrace rbrace = varnothing$, and $A$ and $B$ are arbitrary (finite) sets. We are only missing a counterpart for the variable! Raising an arbitrary set to “the power” of a constant set happens to have a very natural counterpart: the central actor of the most-well known fundamental result about categories, which generalizes Cayley's Theorem, i.e., the Yoneda embedding.

If you are familiar with the latter, buckle up and jump to Poly in Sets. Have a look at our streamlined account of The Yoneda Lemma if you are familiar with Cartesian closed categories, or take it slow and read up on the background in one of the classic or popular textbooks. Tastes tend to vary. However, Benjamin Pierce's Basic Category Theory for Computer Scientists deserves being pointed out as it is very amenable and covers the background we need in 60 short pages.

5.1 Morphisms

5.2 Objects

5.3 The Yoneda Lemma

5.4 Poly in Sets

6 Project Idioms and Conventions

The Geb Project is written in Common Lisp, which means the authors have a great choice in freedom in how the project is laid out and operates. In particular the style of Common Lisp here is a functional style with some OO idioms in the style of Smalltalk.

The subsections will outline many idioms that can be found throughout the codebase.

6.1 Spec Files, Main Files and Project Layout

[in package GEB.SPECS]

The codebase is split between many files. Each folder can be seen as a different idea within geb itself! Thus the poly has packages revolving around polynomials, the geb folder has packages regarding the main types of geb Subst Obj and Subst Morph, etc etc.

The general layout quirk of the codebase is that packages like geb.package.spec defines the specification for the base types for any category we wish to model, and these reside in the specs folder not in the folder that talks about the packages of those types. This is due to loading order issues, we thus load the specs packages before each of their surrounding packages, so that each package can built off the last. Further, packages like geb.package.main define out most of the functionality of the package to be used by other packages in geb.package, then all of these are reexported out in the geb.package package

Further to make working with each package of an idea is easy, we have the main package of the folder (typically named the same as the folder name) reexport most important components so if one wants to work with the fully fledged versions of the package they can simply without having to import too many packages at once.

For example, the geb.poly.spec defines out the types and data structures of the Polynomial Types, this is then rexported in geb.poly, giving the module geb.poly a convenient interface for all functions that operate on geb.poly.

6.2 Open Types versus Closed Types

closed type's and open type's both have their perspective tradeoff of openness versus exhaustiveness (see the linked articles for more on that). Due to this, they both have their own favorable applications. I would argue that a closed ADT type is great tool for looking at a function mathematically and treating the object as a whole rather than piecemeal. Whereas a more open extension is great for thinking about how a particular object/case behaves. They are different mindsets for different styles of code.

In the geb project, we have chosen to accept both styles, and allow both to coexist in the same setting. We have done this with a two part idiom.

(deftype substobj ()
  `(or alias prod coprod so0 so1))

(defclass <substobj> (direct-pointwise-mixin) ())

(defclass so0 (<substobj>) ...)

(defclass prod (<substobj>) ...)

The closed type is GEB:SUBSTOBJ, filling and defining every structure it knows about. This is a fixed idea that a programmer may statically update and get exhaustive warnings about. Whereas GEB:<SUBSTOBJ> is the open interface for the type. Thus we can view [GEB:<SUBSTOBJ>] as the general idea of a [GEB:SUBSTOBJ]. Before delving into how we combine these methods, let us look at two other benefits given by [GEB:<SUBSTOBJ>]

We can put all the Mixins into the superclass to enforce that any type that extends it has the extended behaviors we wish. This is a great way to generically enhance the capabilities of the type without operating on it directly.
We can dispatch on GEB:<SUBSTOBJ> since DEFMETHOD only works on Common Lisp Object System (CLOS) types and not generic types in CL.

Methods for closed and open types

With these pieces in play let us explore how we write a method in a way that is conducive to open and closed code.

(in-package :geb)

(defgeneric to-poly (morphism))

(defmethod to-poly ((obj <substmorph>))
  (typecase-of substmorph obj
    (alias        ...)
    (substobj     (error "Impossible")
    (init          0)
    (terminal      0)
    (inject-left   poly:ident)
    (inject-right  ...)
    (comp          ...)
    (case          ...)
    (pair          ...)
    (project-right ...)
    (project-left  ...)
    (distribute    ...)
    (otherwise (subclass-responsibility obj))))

(defmethod to-poly ((obj <substobj>))
  (declare (ignore obj))
  poly:ident)

In this piece of code we can notice a few things:

We case on [GEB:SUBSTMORPH] exhaustively
We cannot hit the [GEB:<SUBSTOBJ>] case due to method dispatch
We have this [GEB.UTILS:SUBCLASS-RESPONSIBILITY] function getting called.
We can write further methods extending the function to other subtypes.

Thus the [GEB.COMMON:TO-POLY] function is written in such a way that it supports a closed definition and open extensions, with [GEB.UTILS:SUBCLASS-RESPONSIBILITY] serving to be called if an extension a user wrote has no handling of this method.

Code can also be naturally written in a more open way as well, by simply running methods on each class instead.

Potential Drawback and Fixes

One nasty drawback is that we can't guarantee the method exists. In java this can easily be done with interfaces and then enforcing they are fulfilled. Sadly CL has no such equivalent. However, this is all easily implementable. If this ever becomes a major problem, it is trivial to implement this by registering the subclasses, and the perspective methods, and scouring the image for instance methods, and computing if any parent class that isn't the one calling responsibility fulfills it. Thus, in practice, you should be able to ask the system if any particular extension fulfills what extension sets that the base object has and give CI errors if they are not fulfilled, thus enforcing closed behavior when warranted.

6.3 ≺Types≻

These refer to the open type variant to a closed type. Thus when one sees a type like GEB: it is the open version of GEB:SUBSTOBJ. Read Open Types versus Closed Types for information on how to use them.

7 The Geb Model

[in package GEB]

Everything here relates directly to the underlying machinery of GEB, or to abstractions that help extend it.

7.1 The Categorical Interface

[in package GEB.MIXINS]

This covers the main Categorical interface required to be used and contained in various data structures

[class] CAT-OBJ

I offer the service of being a base category objects with no extensions

[class] CAT-MORPH

I offer the service of being a base categorical morphism with no extensions

[generic-function] DOM X

Grabs the domain of the morphism. Returns a CAT-OBJ

[generic-function] CODOM X

Grabs the codomain of the morphism. Returns a CAT-OBJ

[generic-function] CURRY-PROD CAT-MORPH CAT-LEFT CAT-RIGHT

Curries the given product type given the product. This returns a CAT-MORPH.

This interface version takes the left and right product type to properly dispatch on. Instances should specialize on the CAT-RIGHT argument

Use GEB.MAIN:CURRY instead.

7.2 Geneircs

[in package GEB.GENERICS]

These functions represent the generic functions that can be run on many parts of the compiler, they are typically rexported on any package that implements the given generic function.

You can view their documentation in their respective API sections.

The main documentation for the functionality is given here, with examples often given in the specific methods

[generic-function] GAPPLY MORPHISM OBJECT

Applies a given Moprhism to a given object.

This is practically a naive interpreter for any category found throughout the codebase.

Some example usages of GAPPLY are.

GEB> (gapply (comp
              (mcase geb-bool:true
                     geb-bool:not)
              (->right so1 geb-bool:bool))
             (left so1))
(right s-1)
GEB> (gapply (comp
              (mcase geb-bool:true
                     geb-bool:not)
              (->right so1 geb-bool:bool))
             (right so1))
(left s-1)

[generic-function] WELL-DEFP-CAT MORPHISM

Given a moprhism of a category, checks that it is well-defined. E.g. that composition of morphism is well-defined by checking that the domain of MCAR corresponds to the codomain of MCADR

[generic-function] MAYBE OBJECT

Wraps the given OBJECT into a Maybe monad The Maybe monad in this case is simply wrapping the term in a coprod of so1(0 1)

[generic-function] SO-HOM-OBJ OBJECT1 OBJECT2

Takes in X and Y Geb objects and provides an internal hom-object (so-hom-obj X Y) representing a set of functions from X to Y

[generic-function] SO-EVAL OBJECT1 OBJECT2

Takes in X and Y Geb objects and provides an evaluation morphism (prod (so-hom-obj X Y) X) -> Y

[generic-function] WIDTH OBJECT

Given an OBJECT of Geb presents it as a SeqN object. That is, width corresponds the object part of the to-seqn functor.

[generic-function] TO-CIRCUIT MORPHISM NAME

Turns a MORPHISM into a Vampir circuit. the NAME is the given name of the output circuit.

[generic-function] TO-BITC MORPHISM

Turns a given MORPHISM into a [GEB.BITC.SPEC:BITC]

[generic-function] TO-SEQN MORPHISM

Turns a given MORPHISM into a [GEB.SEQN.SPEC:SEQN]

[generic-function] TO-POLY MORPHISM

Turns a given MORPHISM into a [GEB.POLY.SPEC:POLY]

[generic-function] TO-CAT CONTEXT TERM

Turns a MORPHISM with a context into Geb's Core category

[generic-function] TO-VAMPIR MORPHISM VALUES CONSTRAINTS

Turns a MORPHISM into a Vampir circuit, with concrete values.

The more natural interface is [TO-CIRCUIT], however this is a more low level interface into what the polynomial categories actually implement, and thus can be extended or changed.

The VALUES are likely vampir values in a list.

The CONSTRAINTS represent constraints that get creating

7.3 Core Category

[in package GEB.SPEC]

The underlying category of GEB. With Subst Obj covering the shapes and forms (GEB-DOCS/DOCS:@OBJECTS) of data while Subst Morph deals with concrete GEB-DOCS/DOCS:@MORPHISMS within the category.

From this category, most abstractions will be made, with SUBSTOBJ serving as a concrete type layout, with SUBSTMORPH serving as the morphisms between different SUBSTOBJ types. This category is equivalent to finset.

A good example of this category at work can be found within the Booleans section.

7.3.1 Subst Obj

This section covers the objects of the SUBSTMORPH category. Note that SUBSTOBJ refers to the [closed type], whereas <SUBSTOBJ> refers to the [open type] that allows for user extension.

[type] SUBSTOBJ

[class] <SUBSTOBJ> <SUBSTMORPH> DIRECT-POINTWISE-MIXIN META-MIXIN CAT-OBJ

the class corresponding to SUBSTOBJ. See GEB-DOCS/DOCS:@OPEN-CLOSED

SUBSTOBJ type is not a constructor itself, instead it's best viewed as the sum type, with the types below forming the constructors for the term. In ML we would write it similarly to:

type substobj = so0
              | so1
              | prod
              | coprod

[class] PROD <SUBSTOBJ>

The PRODUCT object. Takes two CAT-OBJ values that get put into a pair.

The formal grammar of PRODUCT is
```
(prod mcar mcadr)
```
where PROD is the constructor, [MCAR] is the left value of the product, and [MCADR] is the right value of the product.

Example:
```
(geb-gui::visualize (prod geb-bool:bool geb-bool:bool))
```
Here we create a product of two [GEB-BOOL:BOOL] types.

[class] COPROD <SUBSTOBJ>

the CO-PRODUCT object. Takes CAT-OBJ values that get put into a choice of either value.

The formal grammar of PRODUCT is
```
(coprod mcar mcadr)
```
Where CORPOD is the constructor, [MCAR] is the left choice of the sum, and [MCADR] is the right choice of the sum.

Example:
```
(geb-gui::visualize (coprod so1 so1))
```
Here we create the boolean type, having a choice between two unit values.

[class] SO0 <SUBSTOBJ>

The Initial Object. This is sometimes known as the VOID type.

the formal grammar of SO0 is
```
so0
```
where SO0 is THE initial object.

Example

lisp

[class] SO1 <SUBSTOBJ>

The Terminal Object. This is sometimes referred to as the Unit type.

the formal grammar or SO1 is
```
so1
```
where SO1 is THE terminal object

Example
```
(coprod so1 so1)
```
Here we construct [GEB-BOOL:BOOL] by simply stating that we have the terminal object on either side, giving us two possible ways to fill the type.
```
(->left so1 so1)

(->right so1 so1)
```
where applying [->LEFT] gives us the left unit, while [->RIGHT] gives us the right unit.

The Accessors specific to Subst Obj

[accessor] MCAR PROD (:MCAR)

[accessor] MCADR PROD (:MCADR)

[accessor] MCAR COPROD (:MCAR)

[accessor] MCADR COPROD (:MCADR)

7.3.2 Subst Morph

The overarching types that categorizes the SUBSTMORPH category. Note that SUBSTMORPH refers to the [closed type], whereas <SUBSTMORPH> refers to the [open type] that allows for user extension.

[type] SUBSTMORPH

The morphisms of the SUBSTMORPH category

[class] <SUBSTMORPH> DIRECT-POINTWISE-MIXIN META-MIXIN CAT-MORPH

the class type corresponding to SUBSTMORPH. See GEB-DOCS/DOCS:@OPEN-CLOSED

SUBSTMORPH type is not a constructor itself, instead it's best viewed as the sum type, with the types below forming the constructors for the term. In ML we would write it similarly to:

type substmorph = comp
                | substobj
                | case
                | init
                | terminal
                | pair
                | distribute
                | inject-left
                | inject-right
                | project-left
                | project-right

Note that an instance of SUBSTOBJ, acts like the identity morphism to the layout specified by the given SUBSTOBJ. Thus we can view this as automatically lifting a SUBSTOBJ into a SUBSTMORPH

[class] COMP <SUBSTMORPH>

The composition morphism. Takes two CAT-MORPH values that get applied in standard composition order.

The formal grammar of COMP is
```
(comp mcar mcadr)
```
which may be more familiar as
```
g 。f
```
Where COMP( 。) is the constructor, [MCAR](g) is the second morphism that gets applied, and [MCADR](f) is the first morphism that gets applied.

Example:
```
(geb-gui::visualize
 (comp
  (<-right so1 geb-bool:bool)
  (pair (<-left so1 geb-bool:bool)
        (<-right so1 geb-bool:bool))))
```
In this example we are composing two morphisms. the first morphism that gets applied ([PAIR] ...) is the identity function on the type (PROD SO1 [GEB-BOOL:BOOL]), where we pair the left projection and the right projection, followed by taking the right projection of the type.

Since we know (COMP f id) is just f per the laws of category theory, this expression just reduces to
```
(<-right so1 geb-bool:bool)
```

[class] CASE <SUBSTMORPH>

Eliminates coproducts. Namely Takes two CAT-MORPH values, one gets applied on the left coproduct while the other gets applied on the right coproduct. The result of each CAT-MORPH values must be the same.

The formal grammar of CASE is:
```
(mcase mcar mcadr)
```
Where [MCASE] is the constructor, [MCAR] is the morphism that gets applied to the left coproduct, and [MCADR] is the morphism that gets applied to the right coproduct.

Example:
```
(comp
 (mcase geb-bool:true
        geb-bool:not)
 (->right so1 geb-bool:bool))
```
In the second example, we inject a term with the shape [GEB-BOOL:BOOL] into a pair with the shape (SO1 × [GEB-BOOL:BOOL]), then we use [MCASE] to denote a morphism saying. IF the input is of the shape [SO1], then give us True, otherwise flip the value of the boolean coming in.

[class] INIT <SUBSTMORPH>

The INITIAL Morphism, takes any [CAT-OBJ] and creates a moprhism from SO0 (also known as void) to the object given.

The formal grammar of INITIAL is
```
(init obj)
```
where INIT is the constructor. [OBJ] is the type of object that will be conjured up from SO0, when the morphism is applied onto an object.

Example:
```
(init so1)
```
In this example we are creating a unit value out of void.

[class] TERMINAL <SUBSTMORPH>

The TERMINAL morphism, Takes any [CAT-OBJ] and creates a morphism from that object to SO1 (also known as unit).

The formal grammar of TERMINAL is
```
(terminal obj)
```
where TERMINAL is the constructor. [OBJ] is the type of object that will be mapped to SO1, when the morphism is applied onto an object.

Example:
```
(terminal (coprod so1 so1))

(geb-gui::visualize (terminal (coprod so1 so1)))

(comp value (terminal (codomain value)))

(comp true (terminal bool))
```
In the first example, we make a morphism from the corpoduct of SO1 and SO1 (essentially [GEB-BOOL:BOOL]) to SO1.

In the third example we can proclaim a constant function by ignoring the input value and returning a morphism from unit to the desired type.

The fourth example is taking a [GEB-BOOL:BOOL] and returning [GEB-BOOL:TRUE].

[class] PAIR <SUBSTMORPH>

Introduces products. Namely Takes two CAT-MORPH values. When the PAIR morphism is applied on data, these two [CAT-MORPH]'s are applied to the object, returning a pair of the results

The formal grammar of constructing an instance of pair is:
```
(pair mcar mcdr)
```
where PAIR is the constructor, MCAR is the left morphism, and MCDR is the right morphism

Example:
```
(pair (<-left so1 geb-bool:bool)
      (<-right so1 geb-bool:bool))

(geb-gui::visualize (pair (<-left so1 geb-bool:bool)
                          (<-right so1 geb-bool:bool)))
```
Here this pair morphism takes the pair SO1(0 1) × GEB-BOOL:BOOL, and projects back the left field SO1 as the first value of the pair and projects back the GEB-BOOL:BOOL field as the second values.

[class] DISTRIBUTE <SUBSTMORPH>

The distributive law

[class] INJECT-LEFT <SUBSTMORPH>

The left injection morphism. Takes two CAT-OBJ values. It is the dual of INJECT-RIGHT

The formal grammar is
```
(->left mcar mcadr)
```
Where [->LEFT] is the constructor, [MCAR] is the value being injected into the coproduct of [MCAR] + [MCADR], and the [MCADR] is just the type for the unused right constructor.

Example:
```
(geb-gui::visualize (->left so1 geb-bool:bool))

(comp
 (mcase geb-bool:true
        geb-bool:not)
 (->left so1 geb-bool:bool))
```
In the second example, we inject a term with the shape SO1(0 1) into a pair with the shape (SO1 × [GEB-BOOL:BOOL]), then we use MCASE to denote a morphism saying. IF the input is of the shape [SO1], then give us True, otherwise flip the value of the boolean coming in.

[class] INJECT-RIGHT <SUBSTMORPH>

The right injection morphism. Takes two CAT-OBJ values. It is the dual of INJECT-LEFT

The formal grammar is
```
(->right mcar mcadr)
```
Where ->RIGHT is the constructor, [MCADR] is the value being injected into the coproduct of [MCAR] + [MCADR], and the [MCAR] is just the type for the unused left constructor.

Example:
```
(geb-gui::visualize (->right so1 geb-bool:bool))

(comp
 (mcase geb-bool:true
        geb-bool:not)
 (->right so1 geb-bool:bool))
```
In the second example, we inject a term with the shape [GEB-BOOL:BOOL] into a pair with the shape (SO1 × [GEB-BOOL:BOOL]), then we use [MCASE] to denote a morphism saying. IF the input is of the shape [SO1], then give us True, otherwise flip the value of the boolean coming in.

[class] PROJECT-LEFT <SUBSTMORPH>

The LEFT PROJECTION. Takes two [CAT-MORPH] values. When the LEFT PROJECTION morphism is then applied, it grabs the left value of a product, with the type of the product being determined by the two [CAT-MORPH] values given.

the formal grammar of a PROJECT-LEFT is:
```
(<-left mcar mcadr)
```
Where [<-LEFT] is the constructor, [MCAR] is the left type of the PRODUCT and [MCADR] is the right type of the PRODUCT.

Example:
```
(geb-gui::visualize
  (<-left geb-bool:bool (prod so1 geb-bool:bool)))
```
In this example, we are getting the left [GEB-BOOL:BOOL] from a product with the shape

(GEB-BOOL:BOOL × SO1 × [GEB-BOOL:BOOL])

[class] PROJECT-RIGHT <SUBSTMORPH>

The RIGHT PROJECTION. Takes two [CAT-MORPH] values. When the RIGHT PROJECTION morphism is then applied, it grabs the right value of a product, with the type of the product being determined by the two [CAT-MORPH] values given.

the formal grammar of a PROJECT-RIGHT is:
```
(<-right mcar mcadr)
```
Where [<-RIGHT] is the constructor, [MCAR] is the right type of the PRODUCT and [MCADR] is the right type of the PRODUCT.

Example:
```
(geb-gui::visualize
 (comp (<-right so1 geb-bool:bool)
       (<-right geb-bool:bool (prod so1 geb-bool:bool))))
```
In this example, we are getting the right [GEB-BOOL:BOOL] from a product with the shape

(GEB-BOOL:BOOL × SO1 × [GEB-BOOL:BOOL])

[class] FUNCTOR <SUBSTMORPH>

The Accessors specific to Subst Morph

[accessor] MCAR COMP (:MCAR)

The first composed morphism

[accessor] MCADR COMP (:MCADR)

the second morphism

[accessor] OBJ INIT (:OBJ)

[accessor] OBJ INIT (:OBJ)

[accessor] MCAR CASE (:MCAR)

The morphism that gets applied on the left coproduct

[accessor] MCADR CASE (:MCADR)

The morphism that gets applied on the right coproduct

[accessor] MCAR PAIR (:MCAR)

The left morphism

[accessor] MCDR PAIR (:MCDR)

The right morphism

[accessor] MCAR DISTRIBUTE (:MCAR)

[accessor] MCADR DISTRIBUTE (:MCADR)

[accessor] MCADDR DISTRIBUTE (:MCADDR)

[accessor] MCAR INJECT-LEFT (:MCAR)

[accessor] MCADR INJECT-LEFT (:MCADR)

[accessor] MCAR INJECT-RIGHT (:MCAR)

[accessor] MCADR INJECT-RIGHT (:MCADR)

[accessor] MCAR PROJECT-LEFT (:MCAR)

[accessor] MCADR PROJECT-LEFT (:MCADR)

[accessor] MCAR PROJECT-RIGHT (:MCAR)

[accessor] MCADR PROJECT-RIGHT (:MCADR)

Right projection (product elimination)

7.3.3 Realized Subst Objs

This section covers the REALIZED-OBJECT type. This represents a realized SUBSTOBJ term.

The REALIZED-OBJECT is not a real constructor but rather a sum type for the following type

(deftype realized-object () `(or left right list so1 so0))

In ML we would have written something like

type realized-object = so0
                     | so1
                     | list
                     | left
                     | right

[type] REALIZED-OBJECT

A realized object that can be sent into.

Lists represent PROD in the <SUBSTOBJ> category

LEFT and RIGHT represents realized values for COPROD

Lastly SO1 and SO0 represent the proper class

[class] LEFT DIRECT-POINTWISE-MIXIN

[class] RIGHT DIRECT-POINTWISE-MIXIN

[function] LEFT OBJ

[function] RIGHT OBJ

7.4 Accessors

[in package GEB.UTILS]

These functions are generic lenses of the GEB codebase. If a class is defined, where the names are not known, then these accessors are likely to be used. They may even augment existing classes.

[generic-function] MCAR X

Can be seen as calling CAR on a generic CLOS object

[generic-function] MCADR X

like MCAR but for the CADR

[generic-function] MCADDR X

like MCAR but for the CADDR

[generic-function] MCADDDR OBJ

like MCAR but for the CADDDR

[generic-function] MCDR X

Similar to MCAR, however acts like a CDR for [classes] that we wish to view as a SEQUENCE

[generic-function] OBJ X

Grabs the underlying object

[generic-function] NAME X

the name of the given object

[generic-function] FUNC X

the function of the object

[generic-function] PREDICATE X

the PREDICATE of the object

[generic-function] THEN X

the then branch of the object

[generic-function] ELSE X

the then branch of the object

[generic-function] CODE X

the code of the object

7.5 Constructors

[in package GEB.SPEC]

The API for creating GEB terms. All the functions and variables here relate to instantiating a term

[variable] *SO0* s-0

The Initial Object

[variable] *SO1* s-1

The Terminal Object

More Ergonomic API variants for *SO0* and *SO1*

[symbol-macro] SO0

[symbol-macro] SO1

[macro] ALIAS NAME OBJ

[function] MAKE-ALIAS &KEY NAME OBJ

[function] HAS-ALIASP OBJ

[function] <-LEFT MCAR MCADR

projects left constructor

[function] <-RIGHT MCAR MCADR

projects right constructor

[function] ->LEFT MCAR MCADR

injects left constructor

[function] ->RIGHT MCAR MCADR

injects right constructor

[function] MCASE MCAR MCADR

[function] MAKE-FUNCTOR &KEY OBJ FUNC

7.6 API

Various forms and structures built on-top of Core Category

[method] GAPPLY (MORPH <SUBSTMORPH>) OBJECT

My main documentation can be found on GAPPLY

I am the GAPPLY for <SBUSTMORPH>, the OBJECT that I expect is of type REALIZED-OBJECT. See the documentation for REALIZED-OBJECT for the forms it can take.

Some examples of me are

GEB> (gapply (comp
              (mcase geb-bool:true
                     geb-bool:not)
              (->right so1 geb-bool:bool))
             (left so1))
(right s-1)
GEB> (gapply (comp
              (mcase geb-bool:true
                     geb-bool:not)
              (->right so1 geb-bool:bool))
             (right so1))
(left s-1)
GEB> (gapply geb-bool:and
             (list (right so1)
                   (right so1)))
(right s-1)
GEB> (gapply geb-bool:and
             (list (left so1)
                   (right so1)))
(left s-1)
GEB> (gapply geb-bool:and
             (list (right so1)
                   (left so1)))
(left s-1)
GEB> (gapply geb-bool:and
             (list (left so1)
                   (left so1)))
(left s-1)

[method] GAPPLY (MORPH OPAQUE-MORPH) OBJECT

My main documentation can be found on GAPPLY

I am the GAPPLY for a generic OPAQUE-MOPRH I simply dispatch GAPPLY on my interior code lisp GEB> (gapply (comp geb-list:*car* geb-list:*cons*) (list (right geb-bool:true-obj) (left geb-list:*nil*))) (right GEB-BOOL:TRUE)

[method] GAPPLY (MORPH OPAQUE) OBJECT

My main documentation can be found on GAPPLY

I am the GAPPLY for a generic OPAQUE I simply dispatch GAPPLY on my interior code, which is likely just an object

[method] WELL-DEFP-CAT (MORPH <SUBSTMORPH>)

[method] WELL-DEFP-CAT (MORPH <NATMORPH>)

[method] WELL-DEFP-CAT (MORPH <NATOBJ>)

7.6.1 Booleans

[in package GEB-BOOL]

Here we define out the idea of a boolean. It comes naturally from the concept of coproducts. In ML they often define a boolean like

data Bool = False | True

We likewise define it with coproducts

(def bool (coprod so1 so1))

(def true  (->right so1 so1))
(def false (->left  so1 so1))

The functions given work on this.

[symbol-macro] TRUE

[symbol-macro] FALSE

[symbol-macro] FALSE-OBJ

[symbol-macro] TRUE-OBJ

[symbol-macro] BOOL

[symbol-macro] NOT

[symbol-macro] AND

[symbol-macro] OR

7.6.2 Lists

[in package GEB-LIST]

Here we define out the idea of a List. It comes naturally from the concept of coproducts. Since we lack polymorphism this list is concrete over GEB-BOOL:@GEB-BOOL In ML syntax it looks like

data List = Nil | Cons Bool List

We likewise define it with coproducts, with the recursive type being opaque

(defparameter *nil* (so1))

(defparameter *cons-type* (reference 'cons))

(defparameter *canonical-cons-type*
  (opaque 'cons
          (prod geb-bool:bool *cons-type*)))

(defparameter *list*
  (coprod *nil* *cons-type*))

The functions given work on this.

[variable] *NIL* NIL

[variable] *CONS-TYPE* CONS

[variable] *LIST* LIST

[variable] *CAR* CAR

[variable] *CONS* CONS-Μ

[variable] *CDR* CDR

[symbol-macro] CONS->LIST

[symbol-macro] NIL->LIST

[variable] *CANONICAL-CONS-TYPE* CONS

7.6.3 Translation Functions

[in package GEB.TRANS]

These cover various conversions from Subst Morph and Subst Obj into other categorical data structures.

[method] TO-POLY (OBJ <SUBSTOBJ>)

[method] TO-POLY (OBJ <SUBSTMORPH>)

[method] TO-CIRCUIT (OBJ <SUBSTMORPH>) NAME

Turns a Subst Morph to a Vamp-IR Term

[method] TO-BITC (OBJ <SUBSTMORPH>)

[method] TO-SEQN (OBJ <SUBSTOBJ>)

Preserves identity morphims

[method] TO-SEQN (OBJ GEB.EXTENSION.SPEC:<NATOBJ>)

[method] TO-SEQN (OBJ COMP)

Preserves composition

[method] TO-SEQN (OBJ INIT)

Produces a list of zeroes Currently not aligning with semantics of drop-width as domain and codomain can be of differing lengths

[method] TO-SEQN (OBJ TERMINAL)

Drops everything to the terminal object, i.e. to nothing

[method] TO-SEQN (OBJ INJECT-LEFT)

Injects an x by marking its entries with 0 and then inserting as padded bits if necessary

[method] TO-SEQN (OBJ INJECT-RIGHT)

Injects an x by marking its entries with 1 and then inserting as padded bits if necessary

[method] TO-SEQN (OBJ CASE)

Cases by forgetting the padding and if necessary dropping the extra entries if one of the inputs had more of them to start with

[method] TO-SEQN (OBJ PROJECT-LEFT)

Takes a list of an even length and cuts the right half

[method] TO-SEQN (OBJ PROJECT-RIGHT)

Takes a list of an even length and cuts the left half

[method] TO-SEQN (OBJ PAIR)

Forks entries and then applies both morphism on corresponding entries

[method] TO-SEQN (OBJ DISTRIBUTE)

Given A x (B + C) simply moves the 1-bit entry to the front and keep the same padding relations to get ((A x B) + (A x C)) as times appends sequences

[method] TO-SEQN (OBJ GEB.EXTENSION.SPEC:NAT-DIV)

Division is interpreted as divition

[method] TO-SEQN (OBJ GEB.EXTENSION.SPEC:NAT-CONST)

A choice of a natural number is the same exact choice in SeqN

[method] TO-SEQN (OBJ GEB.EXTENSION.SPEC:NAT-INJ)

Injection of bit-sizes is interpreted in the same maner in SeqN

[method] TO-SEQN (OBJ GEB.EXTENSION.SPEC:ONE-BIT-TO-BOOL)

Iso interpreted in an evident manner

[method] TO-SEQN (OBJ GEB.EXTENSION.SPEC:NAT-DECOMPOSE)

Decomposition is interpreted on the nose

[method] TO-SEQN (OBJ GEB.EXTENSION.SPEC:NAT-EQ)

Equality predicate is interpreted on the nose

[method] TO-SEQN (OBJ GEB.EXTENSION.SPEC:NAT-LT)

Equality predicate is interpreted on the nose

7.6.4 Utility

[in package GEB.MAIN]

Various utility functions on top of Core Category

[function] PAIR-TO-LIST PAIR &OPTIONAL ACC

converts excess pairs to a list format

[function] SAME-TYPE-TO-LIST PAIR TYPE &OPTIONAL ACC

converts the given type to a list format

[function] CLEAVE V1 &REST VALUES

Applies each morphism to the object in turn.

[function] CONST F X

The constant morphism.

Takes a morphism from SO1 to a desired value of type $B$, along with a [<SUBSTOBJ>] that represents the input type say of type $A$, giving us a morphism from $A$ to $B$.

Thus if: F : SO1 → a, X : b

then: (const f x) : a → b
```
Γ, f : so1 → b, x : a
----------------------
(const f x) : a → b
```
Further, If the input F has an ALIAS, then we wrap the output in a new alias to denote it's a constant version of that value.

Example:
```
(const true bool) ; bool -> bool
```

[function] COMMUTES X Y

[function] COMMUTES-LEFT MORPH

swap the input domain of the given [cat-morph]

In order to swap the domain we expect the [cat-morph] to be a PROD

Thus if: (dom morph) ≡ (prod x y), for any x, y [CAT-OBJ]

then: (commutes-left (dom morph)) ≡ (prod y x) u ` Γ, f : x × y → a

(commutes-left f) : y × x → a `

[function] !-> A B

[method] SO-EVAL (X <NATOBJ>) Y

[method] SO-EVAL (X <SUBSTOBJ>) Y

[method] SO-HOM-OBJ (X <NATOBJ>) Z

[method] SO-HOM-OBJ (X <SUBSTOBJ>) Z

[generic-function] SO-CARD-ALG OBJ

Gets the cardinality of the given object, returns a FIXNUM

[method] SO-CARD-ALG (OBJ <SUBSTOBJ>)

[function] CURRY F

Curries the given object, returns a [cat-morph]

The [cat-morph] given must have its DOM be of a PROD type, as CURRY invokes the idea of

if f : (PROD a b) → c

for all a, b, and c being an element of [cat-morph]

then: (curry f): a → c^b

where c^b means c to the exponent of b (EXPT c b)
```
Γ, f : a × b → c,
--------------------
(curry f) : a → c^b
```
In category terms, a → c^b is isomorphic to a → b → c

[function] COPROD-MOR F G

Given f : A → B and g : C → D gives appropriate morphism between COPROD objects f x g : A + B → C + D via the universal property. That is, the morphism part of the coproduct functor Geb x Geb → Geb

[function] PROD-MOR F G

Given f : A → B and g : C → D gives appropriate morphism between PROD objects f x g : A x B → C x D via the universal property. This is the morphism part of the product functor Geb x Geb → Geb

[function] UNCURRY Y Z F

Given a morphism f : x → z^y and explicitly given y and z variables produces an uncurried version f' : x × y → z of said morphism

[generic-function] TEXT-NAME MORPH

Gets the name of the moprhism

These utilities are on top of [CAT-OBJ]

[method] MAYBE (OBJ <SUBSTOBJ>)

I recursively add maybe terms to all <SBUSTOBJ> terms, for what maybe means checkout my generic function documentation.

turning products of A x B into Maybe (Maybe A x Maybe B),

turning coproducts of A | B into Maybe (Maybe A | Maybe B),

turning [SO1(0 1)] into Maybe [SO1]

and [SO0(0 1)] into Maybe [SO0]

[method] MAYBE (OBJ <NATOBJ>)

7.7 Examples

PLACEHOLDER: TO SHOW OTHERS HOW EXAMPLEs WORK

Let's see the transcript of a real session of someone working with GEB:

(values (princ :hello) (list 1 2))
.. HELLO
=> :HELLO
=> (1 2)

(+ 1 2 3 4)
=> 10

8 Extension Sets for Categories

[in package GEB.EXTENSION.SPEC]

This package contains many extensions one may see over the codebase.

Each extension adds an unique feature to the categories they are extending. To learn more, read about the individual extension you are interested in.

Common Sub expressions represent repeat logic that can be found throughout any piece of code

[class] COMMON-SUB-EXPRESSION DIRECT-POINTWISE-MIXIN META-MIXIN CAT-MORPH

I represent common sub-expressions found throughout the code.

I implement a few categorical extensions. I am a valid CAT-MORPH along with fulling the interface for the [GEB.POLY.SPEC:] category.

The name should come from an algorithm that automatically fines common sub-expressions and places the appropriate names.

[function] MAKE-COMMON-SUB-EXPRESSION &KEY OBJ NAME

The Opaque extension lets users write categorical objects and morphisms where their implementation hide the specifics of what types they are operating over

[class] OPAQUE CAT-OBJ META-MIXIN

I represent an object where we want to hide the implementation details of what kind of GEB:SUBSTOBJ I am.

[class] REFERENCE CAT-OBJ CAT-MORPH DIRECT-POINTWISE-MIXIN META-MIXIN

I represent a reference to an OPAQUE identifier.

[class] OPAQUE-MORPH CAT-MORPH META-MIXIN

This represents a morphsim where we want to deal with an OPAQUE that we know intimate details of

[accessor] CODE OPAQUE-MORPH (:CODE)

the code that represents the underlying morphsism

[accessor] DOM OPAQUE-MORPH (:DOM)

The dom of the opaque morph

[accessor] CODOM OPAQUE-MORPH (:CODOM)

The codom of the opaque morph

[accessor] CODE OPAQUE (:CODE)

[accessor] NAME OPAQUE (:NAME)

[accessor] NAME REFERENCE (:NAME)

[function] REFERENCE NAME

[function] OPAQUE-MORPH CODE &KEY (DOM (DOM CODE)) (CODOM (CODOM CODE))

[function] OPAQUE NAME CODE

The Natural Object/Morphism extension allows to expand the core Geb category with additional constructors standing in for bt-sequence representation of natural numbers along with basic operation relating to those.

[type] NATOBJ

[class] <NATOBJ> DIRECT-POINTWISE-MIXIN META-MIXIN CAT-OBJ CAT-MORPH

the class corresponding to [NATOBJ], the extension of SUBSTOBJ adding to Geb bit representation of natural numbers.

[class] NAT-WIDTH <NATOBJ>

the NAT-WIDTH object. Takes a non-zero natural number [NUM] and produces an object standing for cardinality 2^([NUM]) corresponding to [NUM]-wide bit number.

The formal grammar of NAT-WIDTH is
```
(nat-width num)
```
where NAT-WIDTH is the constructor, [NUM] the choice of a natural number we want to be the width of the bits we are to consder.

[accessor] NUM NAT-WIDTH (:NUM)

[function] NAT-WIDTH NUM

[type] NATMORPH

[class] <NATMORPH> DIRECT-POINTWISE-MIXIN META-MIXIN CAT-MORPH

the class corresponding to [NATMORPH], the extension of SUBSTMORPH adding to Geb basic operations on bit representations of natural numbers

[class] NAT-ADD <NATMORPH>

Given a natural number [NUM] greater than 0, gives a morphsm (nat-add num) : (nat-mod num) x (nat-mod num) -> (nat-mod num) representing floored addition of two bits of length n.

The formal grammar of NAT-ADD is

lisp (nat-add num)

[class] NAT-MULT <NATMORPH>

Given a natural number [NUM] greater than 0, gives a morphsm (nat-mult num) : (nat-mod num) x (nat-mod num) -> (nat-mod n) representing floored multiplication in natural numbers modulo n.

The formal grammar of NAT-MULT is

lisp (nat-mult num)

[class] NAT-SUB <NATMORPH>

Given a natural number [NUM] greater than 0, gives a morphsm (nat-sub sum) : (nat-mod num) x (nat-mod num) -> (nat-mod num) representing floored subtraction of two bits of length n.

The formal grammar of NAT-SUB is

lisp (nat-sub num)

[class] NAT-DIV <NATMORPH>

Given a natural number [NUM] greater than 0, gives a morphsm (nat-div num) : (nat-mod num) x (nat-mod num) -> (nat-mod num) representing floored division in natural numbers modulo n.

The formal grammar of NAT-DIV is

lisp (nat-div num)

[class] NAT-CONST <NATMORPH>

Given a NUM natural number, gives a morphsm (nat-const num pos) : so1 -> (nat-width num).

That is, chooses the POS natural number as a NUM-wide bit number

The formal grammar of NAT-ADD is

lisp (nat-const num pos)

[class] NAT-INJ <NATMORPH>

Given a nutural number [NUM] presents a [NUM]-wide bit number as a ([NUM] + 1)-wide bit number via injecting.

The formal grammar of NAT-INJ is
```
(nat-inj num)
```
In Geb, the injection presents itself as a morphism (nat-width num) -> (nat-width (1 + num))

[class] NAT-CONCAT <NATMORPH>

Given two natural numbers of bit length n and m, concatenates them in that order giving a bit of length n + m.

The formal grammar of NAT-CONCAT is
```
(nat-concat num-left num-right)
```
In Geb this corresponds to a morphism (nat-width num-left) x (nat-width num-right) -> (nat-width (n + m))

For a translation to SeqN simply take x of n width and y of m with and take x^m + y

[class] ONE-BIT-TO-BOOL <NATMORPH>

A map nat-width 1 -> bool sending #*0 to false and #*1 to true

[class] NAT-DECOMPOSE <NATMORPH>

Morphism nat-width n -> (nat-width 1) x (nat-width (1- n)) splitting a natural number into the last and all but last collection of bits

[class] NAT-EQ <NATMORPH>

Morphism nat-width n x nat-width n -> bool which evaluated to true iff both inputs are the same

[class] NAT-LT <NATMORPH>

Morphism nat-width n x nat-width n -> bool which evaluated to true iff the first input is less than the second

[class] NAT-MOD <NATMORPH>

Morphism nat-width n x nat-width n -> nat-width n which takes a modulo of the left projection of a pair by the second projection of a pari

[accessor] NUM NAT-ADD (:NUM)

[accessor] NUM NAT-MULT (:NUM)

[accessor] NUM NAT-SUB (:NUM)

[accessor] NUM NAT-DIV (:NUM)

[accessor] NUM NAT-CONST (:NUM)

[accessor] POS NAT-CONST (:POS)

[accessor] NUM NAT-INJ (:NUM)

[accessor] NUM-LEFT NAT-CONCAT (:NUM-LEFT)

[accessor] NUM-RIGHT NAT-CONCAT (:NUM-RIGHT)

[accessor] NUM NAT-DECOMPOSE (:NUM)

[accessor] NUM NAT-EQ (:NUM)

[accessor] NUM NAT-LT (:NUM)

[accessor] NUM NAT-MOD (:NUM)

[function] NAT-ADD NUM

[function] NAT-MULT NUM

[function] NAT-SUB NUM

[function] NAT-DIV NUM

[function] NAT-CONST NUM POS

[function] NAT-INJ NUM

[function] NAT-CONCAT NUM-LEFT NUM-RIGHT

[function] ONE-BIT-TO-BOOL

[function] NAT-DECOMPOSE NUM

[function] NAT-EQ NUM

[function] NAT-LT NUM

[function] NAT-MOD NUM

[generic-function] NUM OBJ

[generic-function] POS OBJ

[generic-function] NUM-LEFT OBJ

[generic-function] NUM-RIGHT OBJ

[variable] *ONE-BIT-TO-BOOL* #<ONE-BIT-TO-BOOL #x302007E62DDD>

[symbol-macro] ONE-BIT-TO-BOOL

9 The GEB GUI

[in package GEB-GUI]

This section covers the suite of tools that help visualize geb objects and make the system nice to work with

9.1 Visualizer

The GEB visualizer deals with visualizing any objects found in the Core Category

if the visualizer gets a Subst Morph, then it will show how the GEB:SUBSTMORPH changes any incoming term.

if the visualizer gets a Subst Obj, then it shows the data layout of the term, showing what kind of data

[function] VISUALIZE OBJECT &OPTIONAL (ASYNC T)

Visualizes both Subst Obj and Subst Morph objects

[function] KILL-RUNNING

Kills all threads and open gui objects created by VISUALIZE

9.1.1 Aiding the Visualizer

One can aid the visualization process a bit, this can be done by simply placing ALIAS around the object, this will place it in a box with a name to better identify it in the graphing procedure.

9.2 Export Visualizer

This works like the normal visualizer except it exports it to a file to be used by other projects or perhaps in papers

[function] SVG OBJECT PATH &KEY (DEFAULT-VIEW (MAKE-INSTANCE 'SHOW-VIEW))

Runs the visualizer, outputting a static SVG image at the directory of choice.

You can customize the view. By default it uses the show-view, which is the default of the visualizer.

A good example usage is
```
GEB-TEST> (geb-gui:svg (shallow-copy-object geb-bool:and) "/tmp/foo.svg")
```

9.3 The GEB Graphizer

[in package GEB-GUI.GRAPHING]

This section covers the GEB Graph representation

9.3.1 The GEB Graphizer Core

[in package GEB-GUI.CORE]

This section covers the graphing procedure in order to turn a GEB object into a format for a graphing backend.

The core types that facilittate the functionality

[type] NOTE

A note is a note about a new node in the graph or a note about a NODE which should be merged into an upcoming NODE.

An example of a NODE-NOTE would be in the case of pair
```
(pair g f)
```
```
               Π₁
     --f--> Y------
X----|            |-----> [Y × Z]
     --g--> Z-----
               Π₂
```
An example of a MERGE-NOTE
```
(Case f g)
(COMP g f)
```
```
           χ₁
         -------> X --f---
[X + Y]--|                ---> A
         -------> Y --g---/
           χ₂

X -f-> Y --> Y -g-> Z
```
Notice that in the pair case, we have a note and a shared node to place down, where as in both of the MERGE-NOTE examples, the Note at the end is not prepended by any special information

[class] NODE META-MIXIN

I represent a graphical node structure. I contain my children and a value to display, along with the representation for which the node really stands for.

Further, we derive the meta-mixin, as it's important for arrow drawing to know if we are the left or the right or the nth child of a particular node. This information is tracked, by storing the object that goes to it in the meta table and recovering the note.

[class] NODE-NOTE

[class] SQUASH-NOTE

This note should be squashed into another note and or node.

[function] MAKE-NOTE &REST INITARGS &KEY FROM NOTE VALUE &ALLOW-OTHER-KEYS

[function] MAKE-SQUASH &REST INITARGS &KEY VALUE &ALLOW-OTHER-KEYS

[generic-function] GRAPHIZE MORPH NOTES

Turns a morphism into a node graph.

The NOTES serve as a way of sharing and continuing computation.

If the NOTE is a :SHARED NOTE then it represents a NODE without children, along with saying where it came from. This is to be stored in parent of the NOTE

If the NOTE is a :CONTINUE NOTE, then the computation is continued at the spot.

The parent field is to set the note on the parent if the NOTE is going to be merged

[generic-function] VALUE X

[function] CONS-NOTE NOTE NOTES

Adds a note to the notes list.

[function] APPLY-NOTE NOTE-TO-BE-ON NOTE

Here we apply the NOTE to the NODE.

In the case of a new node, we record down the information in the note, and set the note as the child of the current NODE. The NODE is returned.

In the case of a squash-note, we instead just return the squash-note as that is the proper NODE to continue from

[generic-function] REPRESENTATION X

[generic-function] CHILDREN X

[function] DETERMINE-TEXT-AND-OBJECT-FROM-NODE FROM TO

Helps lookup the text from the node

[function] NOTERIZE-CHILDREN NODE FUNC

Applies a specified note to the CHILDREN of the NODE.

It does this by applying FUNC on all the CHILDREN and the index of the child in the list

[function] NOTORIZE-CHILDREN-WITH-INDEX-SCHEMA PREFIX NODE

Notorizes the node with a prefix appended with the subscripted number

9.3.2 The GEB Graphizer Passes

[in package GEB-GUI.GRAPHING.PASSES]

This changes how the graph is visualized, simplifying the graph in ways that are intuitive to the user

[function] PASSES NODE

Runs all the passes that simplify viewing the graph. These simplifications should not change the semantics of the graph, only display it in a more bearable way

10 Seqn Specification

[in package GEB.SEQN]

This covers a GEB view of multibit sequences. In particular this type will be used in translating GEB's view of multibit sequences into Vampir

10.1 Seqn Types

[in package GEB.SEQN.SPEC]

[type] SEQN

[class] <SEQN> DIRECT-POINTWISE-MIXIN CAT-MORPH

Seqn is a category whose objects are finite sequences of natural numbers. The n-th natural number in the sequence represents the bitwidth of the n-th entry of the corresponding polynomial circuit

Entries are to be read as (x_1,..., x_n) and x_i is the ith entry So car of a such a list will be the first entry, this is the dissimilarity with the bit notation where newer entries come first in the list

We interpret pairs as actual pairs if entry is of width above 0 and drop it otherwise in the Vamp-Ir setup so that ident bool x bool goes to name x1 = x1 as (seqwidth bool) = (1, max(0, 0))

[class] COMPOSITION <SEQN>

composes the MCAR and MCADR morphisms f : (a1,...,an) -> (b1,..., bm), g : (b1,...,bm) -> (c1, ..., ck) compose g f : (a1,...,an) -> (c1,...,cn)

[class] ID <SEQN>

For (x1,...,xn), id (x1,...,xn) : (x1,....,xn) -> (x1,...,xn)

[class] PARALLEL-SEQ <SEQN>

For f : (a1,..., an) -> (x1,...,xk), g : (b1,..., bm) -> (y1,...,yl) parallel f g : (a1,...,an, b1,...bm) -> (x1,...,xk,y1,...,yl)

[class] FORK-SEQ <SEQN>

Copies the MCAR of length n onto length 2*n by copying its inputs (MCAR). fork (a1, ...., an) -> (a1,...,an, a1,..., an)

[class] DROP-NIL <SEQN>

Drops everything onto a 0 vector, the terminal object drop-nil (x1, ..., xn) : (x1,...,xn) -> (0)

[class] REMOVE-RIGHT <SEQN>

Removes an extra 0 entry from MCAR on the right remove (x1,...,xn) : (x1,...,xn, 0) -> (x1,...,xn)

[class] REMOVE-LEFT <SEQN>

Removes an extra 0 entry from MCAR on the left remove (x1,...,xn) : (0, x1,...,xn) -> (x1,...,xn)

[class] DROP-WIDTH <SEQN>

Given two vectors of same length but with the first ones of padded width, simply project the core bits without worrying about extra zeroes at the end if they are not doing any work drop-width (x1,...,xn) (y1,...,yn) : (x1,...,xn) -> (y1,...,yn) where xi > yi for each i and entries need to be in the image of the evident injection map

In other words the constraints here are that on the enput ei corresponding to xi bit entry the constraint is that range yi ei is true alongside the usual (isrange xi ei) constraint

Another implementation goes through manual removal of extra bits (specifically xi-yi bits) to the left after the decomposition by range xi

[class] INJ-LENGTH-LEFT <SEQN>

Taken an MCAR vector appends to it MCADR list of vectors with arbitrary bit length by doing nothing on the extra entries, i.e. just putting 0es there. inj-lengh-left (x1,...,xn) (y1,...,ym): (x1,...,xn) -> (x1,...,xn, y1,...,yn) Where 0es go in the place of ys or nothing if the injection is into 0-bits

So what gets injected is the left part

[class] INJ-LENGTH-RIGHT <SEQN>

Taken an MCADR vector appends to it MCAR list of vectors with arbitrary bit length by doing nothing on the extra entries, i.e. just putting 0es there. inj-lengh-right (x1,...,xn) (y1,...,ym): (y1,...,ym) -> (x1,...,xn, y1,...,yn) Where 0es go in the place of xs. If any of yi's are 0-bit vectors, the injection goes to nil entry on those parts

What gets injected is the right part

[class] INJ-SIZE <SEQN>

Taken an MCAR 1-long and injects it to MCADR-wide slot wider than the original one by padding it with 0es on the left. inj-size x1 m: (x1) -> (m)

Just a special case of drop-width

[class] BRANCH-SEQ <SEQN>

Takes an f: (x1,...,xn) -> c, g : (x1,...,xn) ->c and produces branch-seq f g (1, x1,...,xn) -> c acting as f on 0 entry and g on 1

[class] SHIFT-FRONT <SEQN>

Takes an MCAR sequence of length at least MCADR and shifts the MCADR-entry to the front shift-front (x1,...,xn) k : (x1,...,xk,...,xn) -> (xk, x1,..., x_k-1, x_k+1,...,xn)

[class] ZERO-BIT <SEQN>

Zero choice of a bit zero: (0) -> (1)

[class] ONE-BIT <SEQN>

1 choice of a bit one: (0) -> (1)

[class] SEQN-ADD <SEQN>

Compiles to range-checked addition of natural numbers of MCAR width. seqn-add n : (n, n) -> (n)

[class] SEQN-SUBTRACT <SEQN>

Compiles to negative-checked subtraction of natural numbers of MCAR width. seqn-subtract n : (n, n) -> (n)

[class] SEQN-MULTIPLY <SEQN>

Compiles to range-checked multiplication of natural numbers of MCAR width. seqn-multiply n : (n, n) -> (n)

[class] SEQN-DIVIDE <SEQN>

Compiles to usual Vamp-IR floored multiplication of natural numbers of MCAR width. seqn-divide n : (n, n) -> (n)

[class] SEQN-NAT <SEQN>

Produces a MCAR-wide representation of MCADR natural number seqn-nat n m = (0) -> (n)

[class] SEQN-CONCAT <SEQN>

Takes a number of MCAR and MCADR width and produces a number of MCAR + MCADR width by concatenating the bit representations. Using field elements, this translates to multiplying the first input by 2 to the power of MCADR and summing with the second entry seqn-concat n m = (n, m) -> (n+m)

[class] SEQN-DECOMPOSE <SEQN>

The type signature of the morphism is seqn-docompose n : (n) -> (1, (n - 1)) with the intended semantics being that the morphism takes an n-bit integer and splits it, taking the leftmost bit to the left part of the codomain and the rest of the bits to the right

[class] SEQN-EQ <SEQN>

The type signature of the morphism is seqn-eq n : (n, n) -> (1, 0) with the intended semantics being that the morphism takes two n-bit integers and produces 1 iff they are equal

[class] SEQN-LT <SEQN>

The type signature of the morphism is seqn-eq n : (n, n) -> (1, 0) with the intended semantics being that the morphism takes two n-bit integers and produces 1 iff the first one is less than the second

[class] SEQN-MOD <SEQN>

The type signature of the morphism is seqn-mod n : (n, n) -> (n) with the intended semantics being that the morphism takes two n-bit integers and produces the modulo of the first integer by the second

10.2 Seqn Constructors

[in package GEB.SEQN.SPEC]

Every accessor for each of the classes making up seqn

[function] COMPOSITION MCAR MCADR

[function] ID MCAR

[function] FORK-SEQ MCAR

[function] PARALLEL-SEQ MCAR MCADR

[function] DROP-NIL MCAR

[function] REMOVE-RIGHT MCAR

[function] REMOVE-LEFT MCAR

[function] DROP-WIDTH MCAR MCADR

[function] INJ-LENGTH-LEFT MCAR MCADR

[function] INJ-LENGTH-RIGHT MCAR MCADR

[function] INJ-SIZE MCAR MCADR

[function] BRANCH-SEQ MCAR MCADR

[function] SHIFT-FRONT MCAR MCADR

[symbol-macro] ZERO-BIT

[symbol-macro] ONE-BIT

[function] SEQN-ADD MCAR

[function] SEQN-SUBTRACT MCAR

[function] SEQN-MULTIPLY MCAR

[function] SEQN-DIVIDE MCAR

[function] SEQN-NAT MCAR MCADR

[function] SEQN-CONCAT MCAR MCADR

[function] SEQN-DECOMPOSE MCAR

[function] SEQN-EQ MCAR

[function] SEQN-LT MCAR

[function] SEQN-MOD MCAR

10.3 seqn api

[in package GEB.SEQN.MAIN]

this covers the seqn api

[function] FILL-IN NUM SEQ

Fills in extra inputs on the right with 0-oes

[function] PROD-LIST L1 L2

Takes two lists of same length and gives pointwise product where first element come from first list and second from second
```
SEQN> (prod-list (list 1 2) (list 3 4))
((1 3) (2 4))
```

[function] SEQ-MAX-FILL SEQ1 SEQ2

Takes two lists, makes them same length by adding 0es on the right where necessary and takes their pointwise product

[method] WIDTH (OBJ <SUBSTOBJ>)

[method] WIDTH (OBJ <NATOBJ>)

[function] INJ-COPROD-PARALLEL OBJ COPR

takes an width(A) or width(B) already transformed with a width(A+B) and gives an appropriate injection of (a1,...,an) into (max (a1, b1), ...., max(an, bn),...) i.e. where the maxes are being taken during the width operation without filling in of the smaller object

[function] ZERO-LIST LENGTH

[method] DOM (X <SEQN>)

Gives the domain of a morphism in SeqN. For a less formal description consult the specs file

[method] COD (X <SEQN>)

Gives the codomain of a morphism in SeqN. For a less formal description consult the specs file

[method] WELL-DEFP-CAT (MORPH <SEQN>)

[method] GAPPLY (MORPHISM <SEQN>) VECTOR

Takes a list of vectors of natural numbers and gives out their evaluations. Currently does not correspond directly to the intended semantics but is capable of successfully evaluating all compiled terms

10.4 Seqn Transformations

[in package GEB.SEQN.TRANS]

This covers transformation functions from

[method] TO-CIRCUIT (MORPHISM <SEQN>) NAME

Turns a SeqN term into a Vamp-IR Gate with the given name Note that what is happening is that we look at the domain of the morphism and skip 0es, making non-zero entries into wires

[function] TEST-CALL CIRCUIT

Given a compiled VampIR function with name foo and arguments x1...xn prints an equality as foo in1 ... in2 = out

[method] TO-VAMPIR (OBJ ID) INPUTS CONSTRAINTS

Given a tuple (x1,...,xn) does nothing with it

[method] TO-VAMPIR (OBJ COMPOSITION) INPUTS CONSTRAINTS

Compile the MCADR after feeding in appropriate inputs and then feed them as entries to compiled MCAR

[method] TO-VAMPIR (OBJ PARALLEL-SEQ) INPUTS CONSTRAINTS

Compile MCAR and MCADR and then append the tuples

[method] TO-VAMPIR (OBJ FORK-SEQ) INPUTS CONSTRAINTS

Given a tuple (x1,...,xn) copies it twice

[method] TO-VAMPIR (OBJ DROP-NIL) INPUTS CONSTRAINTS

Drops everything by producing nothing

[method] TO-VAMPIR (OBJ REMOVE-RIGHT) INPUTS CONSTRAINTS

We do not have nul inputs so does nothing

[method] TO-VAMPIR (OBJ REMOVE-LEFT) INPUTS CONSTRAINTS

We do not have nul inputs so does nothing

[method] TO-VAMPIR (OBJ DROP-WIDTH) INPUTS CONSTRAINTS

The compilation does not produce dropping with domain inputs wider than codomain ones appropriately. Hence we do not require range checks here and simply project

[method] TO-VAMPIR (OBJ INJ-LENGTH-LEFT) INPUTS CONSTRAINTS

Look at the MCAR. Look at non-null wide entries and place 0-es in the outputs otherwise ignore

[method] TO-VAMPIR (OBJ INJ-LENGTH-RIGHT) INPUTS CONSTRAINTS

Look at the MCADR. Look at non-null wide entries and place 0-es in the outputs

[method] TO-VAMPIR (OBJ INJ-SIZE) INPUTS CONSTRAINTS

During th ecompilation procedure the domain will not have larger width than the codomain so we simply project

[method] TO-VAMPIR (OBJ BRANCH-SEQ) INPUTS CONSTRAINTS

With the leftmost input being 1 or 0, pointwise do usual bit branching. If 0 run the MCAR, if 1 run the MCADR

[method] TO-VAMPIR (OBJ SHIFT-FRONT) INPUTS CONSTRAINTS

Takes the MCADR entry and moves it upward leaving everything else fixed. Note that we have to be careful as inputs will have 0es removed already and hence we cannot count as usual

[method] TO-VAMPIR (OBJ ZERO-BIT) INPUTS CONSTRAINTS

[method] TO-VAMPIR (OBJ ONE-BIT) INPUTS CONSTRAINTS

[method] TO-VAMPIR (OBJ SEQN-ADD) INPUTS CONSTRAINTS

[method] TO-VAMPIR (OBJ SEQN-SUBTRACT) INPUTS CONSTRAINTS

[method] TO-VAMPIR (OBJ SEQN-MULTIPLY) INPUTS CONSTRAINTS

[method] TO-VAMPIR (OBJ SEQN-DIVIDE) INPUTS CONSTRAINTS

[method] TO-VAMPIR (OBJ SEQN-NAT) INPUTS CONSTRAINTS

[method] TO-VAMPIR (OBJ SEQN-CONCAT) INPUTS CONSTRAINTS

11 Bits (Boolean Circuit) Specification

[in package GEB.BITC]

This covers a GEB view of Boolean Circuits. In particular this type will be used in translating GEB's view of Boolean Circuits into Vampir

11.1 Bits Types

[in package GEB.BITC.SPEC]

This section covers the types of things one can find in the [BIT(0 1)s] constructors

[type] BITC

[class] <BITC> DIRECT-POINTWISE-MIXIN CAT-MORPH

[class] COMPOSE <BITC>

composes the MCAR and the MCADR

[class] FORK <BITC>

Copies the MCAR of length n onto length 2*n by copying its inputs (MCAR).

[class] PARALLEL <BITC>
```
(parallel x y)
```
constructs a PARALLEL term where the [MCAR] is x and the [MCADR] is y,

where if
```
x : a → b,          y : c → d
-------------------------------
(parallel x y) : a + c → b + d
```
then the PARALLEL will return a function from a and c to b and d where the [MCAR] and [MCADR] run on subvectors of the input.

[class] SWAP <BITC>
```
(swap n m)
```
binds the [MCAR] to n and [MCADR] to m, where if the input vector is of length n + m, then it swaps the bits, algebraically we view it as
```
(swap n m) : #*b₁...bₙbₙ₊₁...bₙ₊ₘ → #*bₙ₊₁...bₘ₊ₙb₁...bₙ
```

[class] ONE <BITC>

ONE represents the map from 0 onto 1 producing a vector with only 1 in it.

[class] ZERO <BITC>

[ZERO] map from 0 onto 1 producing a vector with only 0 in it.

[class] IDENT <BITC>

[IDENT] represents the identity

[class] DROP <BITC>

[DROP] represents the unique morphism from n to 0.

[class] BRANCH <BITC>
```
(branch x y)
```
constructs a BRANCH term where the [MCAR] is x and the [MCADR] is y,

where if
```
x : a → b,          y : a → b
-------------------------------
(branch x y) : 1+a → b
```
then the [BRANCH] will return a function on the type 1 + a, where the 1 represents a bit to branch on. If the first bit is 0, then the [MCAR] is ran, however if the bit is 1, then the [MCADR] is ran.

11.2 Bits (Boolean Circuit) Constructors

[in package GEB.BITC.SPEC]

Every accessor for each of the CLASS's found here are from Accessors

[function] COMPOSE MCAR MCADR &REST ARGS

Creates a multiway constructor for [COMPOSE]

[function] FORK MCAR

FORK ARG1

[function] PARALLEL MCAR MCADR &REST ARGS

Creates a multiway constructor for [PARALLEL]

[function] SWAP MCAR MCADR

swap ARG1 and ARG2

[symbol-macro] ONE

[symbol-macro] ZERO

[function] IDENT MCAR

ident ARG1

[function] DROP MCAR

drop ARG1

[function] BRANCH MCAR MCADR

branch with ARG1 or ARG2

11.3 Bits (Boolean Circuit) API

[in package GEB.BITC.MAIN]

This covers the Bits (Boolean Circuit) API

[method] GAPPLY (MORPHISM <BITC>) (OBJECT BIT-VECTOR)

My My main documentation can be found on GAPPLY

I am the GAPPLY for <BITC>, the OBJECT that I expect is of type NUMBER. GAPPLY reduces down to ordinary common lisp expressions rather straight forwardly

;; figure out the number of bits the function takes
GEB-TEST> (dom (to-bitc geb-bool:and))
2 (2 bits, #x2, #o2, #b10)
GEB-TEST> (gapply (to-bitc geb-bool:and) #*11)
#*1
GEB-TEST> (gapply (to-bitc geb-bool:and) #*10)
#*0
GEB-TEST> (gapply (to-bitc geb-bool:and) #*01)
#*0
GEB-TEST> (gapply (to-bitc geb-bool:and) #*00)
#*0

[method] GAPPLY (MORPHISM <BITC>) (OBJECT LIST)

I am a helper gapply function, where the second argument for [<BITC>] is a list. See the docs for the BIT-VECTOR version for the proper one. We do allow sending in a list like so

;; figure out the number of bits the function takes
GEB-TEST> (dom (to-bitc geb-bool:and))
2 (2 bits, #x2, #o2, #b10)
GEB-TEST> (gapply (to-bitc geb-bool:and) (list 1 1))
#*1
GEB-TEST> (gapply (to-bitc geb-bool:and) (list 1 0))
#*0
GEB-TEST> (gapply (to-bitc geb-bool:and) (list 0 1))
#*0
GEB-TEST> (gapply (to-bitc geb-bool:and) (list 0 0))
#*0

[method] DOM (X <BITC>)

Gives the length of the bit vector the [<BITC>] moprhism takes

[method] CODOM (X <BITC>)

Gives the length of the bit vector the [<BITC>] morphism returns

11.4 Bits (Boolean Circuit) Transformations

[in package GEB.BITC.TRANS]

This covers transformation functions from

[method] TO-CIRCUIT (MORPHISM <BITC>) NAME

Turns a BITC term into a Vamp-IR Gate with the given name

[method] TO-VAMPIR (OBJ COMPOSE) VALUES CONSTRAINTS

[method] TO-VAMPIR (OBJ FORK) VALUES CONSTRAINTS

Copy input n input bits into 2*n output bits

[method] TO-VAMPIR (OBJ PARALLEL) VALUES CONSTRAINTS

Take n + m bits, execute car the n bits and cadr on the m bits and concat the results from car and cadr

[method] TO-VAMPIR (OBJ SWAP) VALUES CONSTRAINTS

Turn n + m bits into m + n bits by swapping

[method] TO-VAMPIR (OBJ ONE) VALUES CONSTRAINTS

Produce a bitvector of length 1 containing 1

[method] TO-VAMPIR (OBJ ZERO) VALUES CONSTRAINTS

Produce a bitvector of length 1 containing 0

[method] TO-VAMPIR (OBJ IDENT) VALUES CONSTRAINTS

turn n bits into n bits by doing nothing

[method] TO-VAMPIR (OBJ DROP) VALUES CONSTRAINTS

turn n bits into an empty bitvector

[method] TO-VAMPIR (OBJ BRANCH) VALUES CONSTRAINTS

Look at the first bit.

If its 0, run f on the remaining bits.

If its 1, run g on the remaining bits.

12 Polynomial Specification

[in package GEB.POLY]

This covers a GEB view of Polynomials. In particular this type will be used in translating GEB's view of Polynomials into Vampir

12.1 Polynomial Types

[in package GEB.POLY.SPEC]

This section covers the types of things one can find in the [POLY] constructors

[type] POLY

[class] <POLY> GEB.MIXINS:DIRECT-POINTWISE-MIXIN

[class] IDENT <POLY>

The Identity Element

[class] + <POLY>

[class] * <POLY>

[class] / <POLY>

[class] - <POLY>

[class] MOD <POLY>

[class] COMPOSE <POLY>

[class] IF-ZERO <POLY>

compare with zero: equal takes first branch; not-equal takes second branch

[class] IF-LT <POLY>

If the [MCAR] argument is strictly less than the [MCADR] then the [THEN] branch is taken, otherwise the [ELSE] branch is taken.

12.2 Polynomial API

[in package GEB.POLY.MAIN]

This covers the polynomial API

[method] GAPPLY (MORPHISM POLY:<POLY>) OBJECT

My main documentation can be found on GAPPLY

I am the GAPPLY for POLY:<POLY>, the OBJECT that I expect is of type NUMBER. GAPPLY reduces down to ordinary common lisp expressions rather straight forwardly

Some examples of me are

(in-package :geb.poly)

POLY> (gapply (if-zero (- ident ident 1) 10 ident) 5)
5 (3 bits, #x5, #o5, #b101)

POLY> (gapply (if-zero (- ident ident) 10 ident) 5)
10 (4 bits, #xA, #o12, #b1010)

POLY> (gapply (- (* 2 ident ident) (* ident ident)) 5)
25 (5 bits, #x19, #o31, #b11001)

[method] GAPPLY (MORPHISM INTEGER) OBJECT

My main documentation can be found on GAPPLY

I am the GAPPLY for INTEGERs, the OBJECT that I expect is of type NUMBER. I simply return myself.

Some examples of me are
```
(in-package :geb.poly)

POLY> (gapply 10 5)
10 (4 bits, #xA, #o12, #b1010)
```

12.3 Polynomial Constructors

[in package GEB.POLY.SPEC]

Every accessor for each of the CLASS's found here are from Accessors

[symbol-macro] IDENT

[function] + MCAR MCADR &REST ARGS

Creates a multiway constructor for [+]

[function] * MCAR MCADR &REST ARGS

Creates a multiway constructor for [*]

[function] / MCAR MCADR &REST ARGS

Creates a multiway constructor for [/]

[function] - MCAR MCADR &REST ARGS

Creates a multiway constructor for [-]

[function] MOD MCAR MCADR

MOD ARG1 by ARG2

[function] COMPOSE MCAR MCADR &REST ARGS

Creates a multiway constructor for [COMPOSE]

[function] IF-ZERO PRED THEN ELSE

checks if [PREDICATE] is zero then take the [THEN] branch otherwise the [ELSE] branch

[function] IF-LT MCAR MCADR THEN ELSE

Checks if the [MCAR] is less than the [MCADR] and chooses the appropriate branch

12.4 Polynomial Transformations

[in package GEB.POLY.TRANS]

This covers transformation functions from

[method] TO-CIRCUIT (MORPHISM <POLY>) NAME

Turns a POLY term into a Vamp-IR Gate with the given name

[method] TO-VAMPIR (OBJ INTEGER) VALUE LET-VARS

Numbers act like a constant function, ignoring input

[method] TO-VAMPIR (OBJ IDENT) VALUE LET-VARS

Identity acts as the identity function

[method] TO-VAMPIR (OBJ +) VALUE LET-VARS

Propagates the value and adds them

[method] TO-VAMPIR (OBJ *) VALUE LET-VARS

Propagates the value and times them

[method] TO-VAMPIR (OBJ -) VALUE LET-VARS

Propagates the value and subtracts them

[method] TO-VAMPIR (OBJ /) VALUE LET-VARS

[method] TO-VAMPIR (OBJ COMPOSE) VALUE LET-VARS

[method] TO-VAMPIR (OBJ IF-ZERO) VALUE LET-VARS

The PREDICATE that comes in must be 1 or 0 for the formula to work out.

[method] TO-VAMPIR (OBJ IF-LT) VALUE LET-VARS

[method] TO-VAMPIR (OBJ MOD) VALUE LET-VARS

13 The Simply Typed Lambda Calculus model

[in package GEB.LAMBDA]

This covers GEB's view on simply typed lambda calculus

This serves as a useful frontend for those wishing to write a compiler to GEB and do not wish to target the categorical model.

If one is targeting their compiler to the frontend, then the following code should be useful for you.

(in-package :geb.lambda.main)

MAIN>
(to-circuit
 (lamb (list (coprod so1 so1))
              (index 0))
 :id)
(def id x1 = {
   (x1)
 };)

MAIN>
(to-circuit
 (lamb (list (coprod so1 so1))
              (case-on (index 0)
                              (lamb (list so1)
                                           (right so1 (unit)))
                              (lamb (list so1)
                                           (left so1 (unit)))))
 :not)
(def not x1 = {
   (((1 - x1) * 1) + (x1 * 0), ((1 - x1) * 1) + (x1 * 0))
 };)

MAIN> (to-circuit (lamb (list geb-bool:bool)
                        (left so1 (right so1 (index 0)))) :foo)
(def foo x1 = {
   (0, 1, x1)
 };)

For testing purposes, it may be useful to go to the BITC backend and run our interpreter

MAIN>
(gapply (to-bitc
         (lamb (list (coprod so1 so1))
               (case-on (index 0)
                        (lamb (list so1)
                              (right so1 (unit)))
                        (lamb (list so1)
                              (left so1 (unit))))))
        #*1)
#*00
MAIN>
(gapply (to-bitc
         (lamb (list (coprod so1 so1))
               (case-on (index 0)
                        (lamb (list so1)
                              (right so1 (unit)))
                        (lamb (list so1)
                              (left so1 (unit))))))
        #*0)
#*11

13.1 Lambda Specification

[in package GEB.LAMBDA.SPEC]

This covers the various the abstract data type that is the simply typed lambda calculus within GEB. The class presents untyped STLC terms.

[type] STLC

Type of untyped terms of STLC. Each class of a term has a slot for a type, which can be filled by auxiliary functions or by user. Types are represented as SUBSTOBJ.

[class] <STLC> DIRECT-POINTWISE-MIXIN META-MIXIN CAT-OBJ

Class of untyped terms of simply typed lambda claculus. Given our presentation, we look at the latter as a type theory spanned by empty, unit types as well as coproduct, product, and function types.

[class] ABSURD <STLC>

The ABSURD term provides an element of an arbitrary type given a term of the empty type, denoted by SO0. The formal grammar of ABSURD is
```
(absurd tcod term)
```
where we possibly can include type information by
```
(absurd tcod term :ttype ttype)
```
The intended semantics are: [TCOD] is a type whose term we want to get (and hence a SUBSTOBJ) and [TERM] is a term of the empty type (and hence an STLC.

This corresponds to the elimination rule of the empty type. Namely, given $$\Gamma \vdash \text{tcod : Type}$$ and $$\Gamma \vdash \text{term : so0}$$ one deduces $$\Gamma \vdash \text{(absurd tcod term) : tcod}$$

[class] UNIT <STLC>

The unique term of the unit type, the latter represented by SO1. The formal grammar of UNIT is
```
(unit)
```
where we can optionally include type information by
```
(unit :ttype ttype)
```
Clearly the type of UNIT is SO1 but here we provide all terms untyped.

This grammar corresponds to the introduction rule of the unit type. Namely $$\Gamma \dashv \text{(unit) : so1}$$

[class] LEFT <STLC>

Term of a coproduct type gotten by injecting into the left type of the coproduct. The formal grammar of LEFT is
```
(left rty term)
```
where we can include optional type information by
```
(left rty term :ttype ttype)
```
The intended semantics are as follows: RTY should be a type (and hence a SUBSTOBJ) and specify the right part of the coproduct of the type TTYPE of the entire term. The term (and hence an STLC) we are injecting is TERM.

This corresponds to the introduction rule of the coproduct type. Namely, given $$\Gamma \dashv \text{(ttype term) : Type}$$ and $$\Gamma \dashv \text{rty : Type}$$ with $$\Gamma \dashv \text{term : (ttype term)}$$ we deduce $$\Gamma \dashv \text{(left rty term) : (coprod (ttype term) rty)}$$

[class] RIGHT <STLC>

Term of a coproduct type gotten by injecting into the right type of the coproduct. The formal grammar of RIGHT is
```
(right lty term)
```
where we can include optional type information by
```
(right lty term :ttype ttype)
```
The intended semantics are as follows: [LTY] should be a type (and hence a SUBSTOBJ) and specify the left part of the coproduct of the type [TTYPE] of the entire term. The term (and hence an STLC) we are injecting is [TERM].

This corresponds to the introduction rule of the coproduct type. Namely, given $$\Gamma \dashv \text{(ttype term) : Type}$$ and $$\Gamma \dashv \text{lty : Type}$$ with $$\Gamma \dashv \text{term : (ttype term)}$$ we deduce $$\Gamma \dashv \text{(right lty term) : (coprod lty (ttype term))}$$

[class] CASE-ON <STLC>

A term of an arbitrary type provided by casing on a coproduct term. The formal grammar of CASE-ON is
```
(case-on on ltm rtm)
```
where we can possibly include type information by
```
(case-on on ltm rtm :ttype ttype)
```
The intended semantics are as follows: [ON] is a term (and hence an STLC) of a coproduct type, and [LTM] and [RTM] terms (hence also STLC) of the same type in the context of - appropriately
- (mcar (ttype on)) and (mcadr (ttype on)).
This corresponds to the elimination rule of the coprodut type. Namely, given $$\Gamma \vdash \text{on : (coprod (mcar (ttype on)) (mcadr (ttype on)))}$$ and $$\text{(mcar (ttype on))} , \Gamma \vdash \text{ltm : (ttype ltm)}$$ , $$\text{(mcadr (ttype on))} , \Gamma \vdash \text{rtm : (ttype ltm)}$$ we get $$\Gamma \vdash \text{(case-on on ltm rtm) : (ttype ltm)}$$ Note that in practice we append contexts on the left as computation of INDEX is done from the left. Otherwise, the rules are the same as in usual type theory if context was read from right to left.

[class] PAIR <STLC>

A term of the product type gotten by pairing a terms of a left and right parts of the product. The formal grammar of PAIR is
```
(pair ltm rtm)
```
where we can possibly include type information by
```
(pair ltm rtm :ttype ttype)
```
The intended semantics are as follows: [LTM] is a term (and hence an STLC) of a left part of the product type whose terms we are producing. [RTM] is a term (hence also STLC)of the right part of the product.

The grammar corresponds to the introduction rule of the pair type. Given $$\Gamma \vdash \text{ltm : (mcar (ttype (pair ltm rtm)))}$$ and $$\Gamma \vdash \text{rtm : (mcadr (ttype (pair ltm rtm)))}$$ we have $$\Gamma \vdash \text{(pair ltm rtm) : (ttype (pair ltm rtm))}$$

[class] FST <STLC>

The first projection of a term of a product type. The formal grammar of FST is:
```
(fst term)
```
where we can possibly include type information by
```
(fst term :ttype ttype)
```
The intended semantics are as follows: TERM is a term (and hence an STLC) of a product type, to whose left part we are projecting to.

This corresponds to the first projection function gotten by induction on a term of a product type.

[class] SND <STLC>

The second projection of a term of a product type. The formal grammar of SND is:
```
(snd term)
```
where we can possibly include type information by
```
(snd term :ttype ttype)
```
The intended semantics are as follows: TERM is a term (and hence an STLC) of a product type, to whose right part we are projecting to.

This corresponds to the second projection function gotten by induction on a term of a product type.

[class] LAMB <STLC>

A term of a function type gotten by providing a term in the codomain of the function type by assuming one is given variables in the specified list of types. LAMB takes in the TDOM accessor a list of types - and hence of SUBSTOBJ - and in the TERM a term - and hence an STLC. The formal grammar of LAMB is:
```
(lamb tdom term)
```
where we can possibly include type information by
```
(lamb tdom term :ttype ttype)
```
The intended semantics are: TDOM is a list of types (and hence a list of SUBSTOBJ) whose iterative product of components form the domain of the function type. TERM is a term (and hence an STLC) of the codomain of the function type gotten in the context to whom we append the list of the domains.

For a list of length 1, corresponds to the introduction rule of the function type. Namely, given $$\Gamma \vdash \text{tdom : Type}$$ and $$\Gamma, \text{tdom} \vdash \text{term : (ttype term)}$$ we have $$\Gamma \vdash \text{(lamb tdom term) : (so-hom-obj tdom (ttype term))}$$

For a list of length n, this corresponds to the iterated lambda type, e.g.
```
(lamb (list so1 so0) (index 0))
```
is a term of
```
(so-hom-obj (prod so1 so0) so0)
```
or equivalently
```
(so-hom-obj so1 (so-hom-obj so0 so0))
```
due to Geb's computational definition of the function type.

Note that INDEX 0 in the above code is of type SO1. So that after annotating the term, one gets
```
LAMBDA> (ttype (term (lamb (list so1 so0)) (index 0)))
s-1
```
So the counting of indices starts with the leftmost argument for computational reasons. In practice, typing of LAMB corresponds with taking a list of arguments provided to a lambda term, making it a context in that order and then counting the index of the variable. Type-theoretically,

$$\Gamma \vdash \lambda \Delta (index i)$$ $$\Delta, \Gamma \vdash (index i)$$

So that by the operational semantics of INDEX, the type of (index i) in the above context will be the i'th element of the Delta context counted from the left. Note that in practice we append contexts on the left as computation of INDEX is done from the left. Otherwise, the rules are the same as in usual type theory if context was read from right to left.

[class] APP <STLC>

A term of an arbitrary type gotten by applying a function of an iterated function type with a corresponding codomain iteratively to terms in the domains. APP takes as argument for the FUN accessor a function - and hence an STLC - whose function type has domain an iterated GEB:PROD of SUBSTOBJ and for the TERM a list of terms - and hence of STLC - matching the types of the product. The formal grammar of APP is
```
(app fun term)
```
where we can possibly include type information by
```
(app fun term :ttype ttype)
```
The intended semantics are as follows: FUN is a term (and hence an STLC) of a coproduct type - say of (so-hom-obj (ttype term) y) - and TERM is a list of terms (hence also of STLC) with nth term in the list having the n-th part of the function type.

For a one-argument term list, this corresponds to the elimination rule of the function type. Given $$\Gamma \vdash \text{fun : (so-hom-obj (ttype term) y)}$$ and $$\Gamma \vdash \text{term : (ttype term)}$$ we get $$\Gamma \vdash \text{(app fun term) : y}$$

For several arguments, this corresponds to successive function application. Using currying, this corresponds to, given
```
G ⊢ (so-hom-obj (A₁ × ··· × Aₙ₋₁) Aₙ)
G ⊢ f : (so-hom-obj (A₁ × ··· × Aₙ₋₁)
G ⊢ tᵢ : Aᵢ
```
then for each i less than n gets us
```
G ⊢ (app f t₁ ··· tₙ₋₁) : Aₙ
```
Note again that i'th term should correspond to the ith element of the product in the codomain counted from the left.

[class] INDEX <STLC>

The variable term of an arbitrary type in a context. The formal grammar of INDEX is
```
(index pos)
```
where we can possibly include type information by
```
(index pos :ttype ttype)
```
The intended semantics are as follows: POS is a natural number indicating the position of a type in a context.

This corresponds to the variable rule. Namely given a context $$\Gamma_1 , \ldots , \Gamma_{pos} , \ldots , \Gamma_k $$ we have

$$\Gamma_1 , \ldots , \Gamma_k \vdash \text{(index pos) :} \Gamma_{pos}$$

Note that we add contexts on the left rather than on the right contra classical type-theoretic notation.

[class] ERR <STLC>

An error term of a type supplied by the user. The formal grammar of ERR is
```
(err ttype)
```
The intended semantics are as follows: ERR represents an error node currently having no particular feedback but with functionality to be of an arbitrary type. Note that this is the only STLC term class which does not have TTYPE a possibly empty accessor.

[class] PLUS <STLC>

A term representing syntactic summation of two bits of the same width. The formal grammar of [PLUS] is
```
(plus ltm rtm)
```
where we can possibly supply typing info by
```
(plus ltm rtm :ttype ttype)
```
Note that the summation is ranged, so if the operation goes above the bit-size of supplied inputs, the corresponding Vamp-IR code will not verify.

[class] TIMES <STLC>

A term representing syntactic multiplication of two bits of the same width. The formal grammar of [TIMES] is
```
(times ltm rtm)
```
where we can possibly supply typing info by
```
(times ltm rtm :ttype ttype)
```
Note that the multiplication is ranged, so if the operation goes above the bit-size of supplied inputs, the corresponding Vamp-IR code will not verify.

[class] MINUS <STLC>

A term representing syntactic subtraction of two bits of the same width. The formal grammar of [MINUS] is
```
(minus ltm rtm)
```
where we can possibly supply typing info by
```
(minus ltm rtm :ttype ttype)
```
Note that the subtraction is ranged, so if the operation goes below zero, the corresponding Vamp-IR code will not verify.

[class] DIVIDE <STLC>

A term representing syntactic division (floored) of two bits of the same width. The formal grammar of [DIVIDE] is
```
(minus ltm rtm)
```
where we can possibly supply typing info by
```
(minus ltm rtm :ttype ttype)
```

[class] BIT-CHOICE <STLC>

A term representing a choice of a bit. The formal grammar of [BIT-CHOICE] is
```
(bit-choice bitv)
```
where we can possibly supply typing info by
```
(bit-choice bitv :ttype ttype)
```
Note that the size of bits matter for the operations one supplies them to. E.g. (plus (bit-choice #*1) (bit-choice #*00)) is not going to pass our type-check, as both numbers ought to be of exact same bit-width.

[class] LAMB-EQ <STLC>

lamb-eq predicate takes in two bit inputs of same bit-width and gives true if they are equal and false otherwise. Note that for the usual Vamp-IR code interpretations, that means that we associate true with left input into bool and false with the right. Appropriately, in Vamp-IR the first branch will be associated with the 0 input and the second branch with 1.

[class] LAMB-LT <STLC>

lamb-lt predicate takes in two bit inputs of same bit-width and gives true if ltm is less than rtm and false otherwise. Note that for the usual Vamp-IR code interpretations, that means that we associate true with left input into bool and false with the right. Appropriately, in Vamp-IR the first branch will be associated with the 0 input and the second branch with 1.

[class] MODULO <STLC>

A term representing syntactic modulus of the first number by the second number. The formal grammar of [MODULO] is
```
(modulo ltm rtm)
```
where we can possibly supply typing info by
```
(modulo ltm rtm :ttype ttype)
```
meaning that we take ltm mod rtm

[function] ABSURD TCOD TERM &KEY (TTYPE NIL)

[function] UNIT &KEY (TTYPE NIL)

[function] LEFT RTY TERM &KEY (TTYPE NIL)

[function] RIGHT LTY TERM &KEY (TTYPE NIL)

[function] CASE-ON ON LTM RTM &KEY (TTYPE NIL)

[function] PAIR LTM RTM &KEY (TTYPE NIL)

[function] FST TERM &KEY (TTYPE NIL)

[function] SND TERM &KEY (TTYPE NIL)

[function] LAMB TDOM TERM &KEY (TTYPE NIL)

[function] APP FUN TERM &KEY (TTYPE NIL)

[function] INDEX POS &KEY (TTYPE NIL)

[function] ERR TTYPE

[function] PLUS LTM RTM &KEY (TTYPE NIL)

[function] TIMES LTM RTM &KEY (TTYPE NIL)

[function] MINUS LTM RTM &KEY (TTYPE NIL)

[function] DIVIDE LTM RTM &KEY (TTYPE NIL)

[function] BIT-CHOICE BITV &KEY (TTYPE NIL)

[function] LAMB-EQ LTM RTM &KEY (TTYPE NIL)

[function] LAMB-LT LTM RTM &KEY (TTYPE NIL)

[function] ABSURD TCOD TERM &KEY (TTYPE NIL)

Accessors of ABSURD

[accessor] TCOD ABSURD (:TCOD)

An arbitrary type

[accessor] TERM ABSURD (:TERM)

A term of the empty type

[accessor] TTYPE ABSURD (:TTYPE = NIL)

Accessors of UNIT

[accessor] TTYPE UNIT (:TTYPE = NIL)

Accessors of LEFT

[accessor] RTY LEFT (:RTY)

Right argument of coproduct type

[accessor] TERM LEFT (:TERM)

Term of the left argument of coproduct type

[accessor] TTYPE LEFT (:TTYPE = NIL)

Accessors of RIGHT

[accessor] LTY RIGHT (:LTY)

Left argument of coproduct type

[accessor] TERM RIGHT (:TERM)

Term of the right argument of coproduct type

[accessor] TTYPE RIGHT (:TTYPE = NIL)

Accessors of CASE-ON

[accessor] ON CASE-ON (:ON)

Term of coproduct type

[accessor] LTM CASE-ON (:LTM)

Term in context of left argument of coproduct type

[accessor] RTM CASE-ON (:RTM)

Term in context of right argument of coproduct type

[accessor] TTYPE CASE-ON (:TTYPE = NIL)

Accessors of PAIR

[accessor] LTM PAIR (:LTM)

Term of left argument of the product type

[accessor] RTM PAIR (:RTM)

Term of right argument of the product type

[accessor] TTYPE PAIR (:TTYPE = NIL)

Accessors of FST

[accessor] TERM FST (:TERM)

Term of product type

[accessor] TTYPE FST (:TTYPE = NIL)

Accessors of SND

[accessor] TERM SND (:TERM)

Term of product type

[accessor] TTYPE SND (:TTYPE = NIL)

Accessors of LAMB

[accessor] TDOM LAMB (:TDOM)

Domain of the lambda term

[accessor] TERM LAMB (:TERM)

Term of the codomain mapped to given a variable of tdom

[accessor] TTYPE LAMB (:TTYPE = NIL)

Accessors of APP

[accessor] FUN APP (:FUN)

Term of exponential type

[accessor] TERM APP (:TERM)

List of Terms of the domain

[accessor] TTYPE APP (:TTYPE = NIL)

Accessors of INDEX

[accessor] POS INDEX (:POS)

Position of type

[accessor] TTYPE INDEX (:TTYPE = NIL)

Accessor of ERR

[accessor] TTYPE ERR (:TTYPE = NIL)

Accessors of PLUS

[accessor] LTM PLUS (:LTM)

[accessor] RTM PLUS (:RTM)

[accessor] TTYPE PLUS (:TTYPE = NIL)

Accessors of TIMES

[accessor] LTM TIMES (:LTM)

[accessor] RTM TIMES (:RTM)

[accessor] TTYPE TIMES (:TTYPE = NIL)

Accessors of MINUS

[accessor] LTM MINUS (:LTM)

[accessor] RTM MINUS (:RTM)

[accessor] TTYPE MINUS (:TTYPE = NIL)

Accessors of DIVIDE

[accessor] LTM DIVIDE (:LTM)

[accessor] RTM DIVIDE (:RTM)

[accessor] TTYPE DIVIDE (:TTYPE = NIL)

Accessors of BIT-CHOICE

[accessor] BITV BIT-CHOICE (:BITV)

[accessor] TTYPE BIT-CHOICE (:TTYPE = NIL)

Accessors of LAMB-EQ

[accessor] LTM LAMB-EQ (:LTM)

[accessor] RTM LAMB-EQ (:RTM)

[accessor] TTYPE LAMB-EQ (:TTYPE = NIL)

Accessors of LAMB-LT

[accessor] LTM LAMB-LT (:LTM)

[accessor] RTM LAMB-LT (:RTM)

[accessor] TTYPE LAMB-LT (:TTYPE = NIL)

Accessors of MODULO

[accessor] LTM MODULO (:LTM)

[accessor] RTM MODULO (:RTM)

[accessor] TTYPE MODULO (:TTYPE = NIL)

[generic-function] TCOD X

[generic-function] TDOM X

[generic-function] TERM X

[generic-function] RTY X

[generic-function] LTY X

[generic-function] LTM X

[generic-function] RTM X

[generic-function] ON X

[generic-function] FUN X

[generic-function] POS X

[generic-function] TTYPE X

[generic-function] BITV X

13.2 Main functionality

[in package GEB.LAMBDA.MAIN]

This covers the main API for the STLC module

[generic-function] ANN-TERM1 CTX TTERM

Given a list of SUBSTOBJ objects with SO-HOM-OBJ occurrences replaced by FUN-TYPE and an STLC similarly replacing type occurrences of the hom object to FUN-TYPE, provides the TTYPE accessor to all subterms as well as the term itself, using FUN-TYPE. Once again, note that it is important for the context and term to be giving as per above description. While not always, not doing so result in an error upon evaluation. As an example of a valid entry we have
```
 (ann-term1 (list so1 (fun-type so1 so1)) (app (index 1) (list (index 0))))
```
while
```
(ann-term1 (list so1 (so-hom-obj so1 so1)) (app (index 1) (list (index 0))))
```
produces an error trying to use. This warning applies to other functions taking in context and terms below as well.

Moreover, note that for terms whose typing needs addition of new context we append contexts on the left rather than on the right contra usual type theoretic notation for the convenience of computation. That means, e.g. that asking for a type of a lambda term as below produces:
```
LAMBDA> (ttype (term (ann-term1 (lambda (list so1 so0) (index 0)))))
s-1
```
as we count indices from the left of the context while appending new types to the context on the left as well. For more info check LAMB

[function] INDEX-CHECK I CTX

Given an natural number I and a context, checks that the context is of length at least I and then produces the Ith entry of the context counted from the left starting with 0.

[function] FUN-TO-HOM T1

Given a SUBSTOBJ whose subobjects might have a FUN-TYPE occurrence replaces all occurrences of FUN-TYPE with a suitable SO-HOM-OBJ, hence giving a pure SUBSTOBJ
```
LAMBDA> (fun-to-hom (fun-type geb-bool:bool geb-bool:bool))
(× (+ GEB-BOOL:FALSE GEB-BOOL:TRUE) (+ GEB-BOOL:FALSE GEB-BOOL:TRUE))
```

[function] ANN-TERM2 TTERM

Given an STLC term with a TTYPE accessor from ANN-TERM1 - i.e. including possible FUN-TYPE occurrences - re-annotates the term and its subterms with actual SUBSTOBJ objects.

[function] ANNOTATED-TERM CTX TERM

Given a context consisting of a list of SUBSTOBJ with occurrences of SO-HOM-OBJ replaced by FUN-TYPE and an STLC term with similarly replaced occurrences of SO-HOM-OBJ, provides an STLC with all subterms typed, i.e. providing the TTYPE accessor, which is a pure SUBSTOBJ

[function] TYPE-OF-TERM-W-FUN CTX TTERM

Given a context consisting of a list of SUBSTOBJ with occurrences of SO-HOM-OBJ replaced by FUN-TYPE and an STLC term with similarly replaced occurrences of SO-HOM-OBJ, gives out a type of the whole term with occurrences of SO-HOM-OBJ replaced by FUN-TYPE.

[function] TYPE-OF-TERM CTX TTERM

Given a context consisting of a list of SUBSTOBJ with occurrences of SO-HOM-OBJ replaced by FUN-TYPE and an STLC term with similarly replaced occurrences of SO-HOM-OBJ, provides the type of the whole term, which is a pure SUBSTOBJ.

[generic-function] WELL-DEFP CTX TTERM

Given a context consisting of a list of SUBSTOBJ with occurrences of SO-HOM-OBJ replaced by FUN-TYPE and an STLC term with similarly replaced occurrences of SO-HOM-OBJ, checks that the term is well-defined in the context based on structural rules of simply typed lambda calculus. returns the t if it is, otherwise returning nil

[class] FUN-TYPE DIRECT-POINTWISE-MIXIN CAT-OBJ

Stand-in for the SO-HOM-OBJ object. It does not have any computational properties and can be seen as just a function of two arguments with accessors MCAR to the first argument and MCADR to the second argument. There is an evident canonical way to associate FUN-TYPE and SO-HOM-OBJ pointwise.

[function] FUN-TYPE MCAR MCADR

[function] ERRORP TTERM

Evaluates to true iff the term has an error subterm.

[function] REDUCER TTERM

Reduces a given Lambda term by applying explicit beta-reduction when possible alongside arithmetic simplification. We assume that the lambda and app terms are 1-argument

[accessor] MCAR FUN-TYPE (:MCAR)

[accessor] MCADR FUN-TYPE (:MCADR)

13.3 Transition Functions

[in package GEB.LAMBDA.TRANS]

These functions deal with transforming the data structure to other data types

One important note about the lambda conversions is that all transition functions except [TO-CAT] do not take a context.

Thus if the [<STLC>] term contains free variables, then call [TO-CAT] and give it the desired context before calling any other transition functions

[method] TO-CAT CONTEXT (TTERM <STLC>)

Compiles a checked term in said context to a Geb morphism. If the term has an instance of an error term, wraps it in a Maybe monad, otherwise, compiles according to the term model interpretation of STLC

[method] TO-POLY (OBJ <STLC>)

I convert a lambda term into a [GEB.POLY.SPEC:POLY] term

Note that [<STLC>] terms with free variables require a context, and we do not supply them here to conform to the standard interface

If you want to give a context, please call [to-cat] before calling me

[method] TO-BITC (OBJ <STLC>)

I convert a lambda term into a [GEB.BITC.SPEC:BITC] term

Note that [<STLC>] terms with free variables require a context, and we do not supply them here to conform to the standard interface

If you want to give a context, please call [to-cat] before calling me

[method] TO-SEQN (OBJ <STLC>)

I convert a lambda term into a [GEB.SEQN.SPEC:SEQN] term

Note that [<STLC>] terms with free variables require a context, and we do not supply them here to conform to the standard interface

If you want to give a context, please call [to-cat] before calling me

[method] TO-CIRCUIT (OBJ <STLC>) NAME

I convert a lambda term into a vampir term

Note that [<STLC>] terms with free variables require a context, and we do not supply them here to conform to the standard interface

If you want to give a context, please call [to-cat] before calling me

13.3.1 Utility Functionality

These are utility functions relating to translating lambda terms to other types

[function] STLC-CTX-TO-MU CONTEXT

Converts a generic (CODE ) context into a SUBSTMORPH. Note that usually contexts can be interpreted in a category as a $Sigma$-type$, which in a non-dependent setting gives us a usual PROD
```
LAMBDA> (stlc-ctx-to-mu (list so1 (fun-to-hom (fun-type geb-bool:bool geb-bool:bool))))
(× s-1
   (× (+ GEB-BOOL:FALSE GEB-BOOL:TRUE) (+ GEB-BOOL:FALSE GEB-BOOL:TRUE))
   s-1)
```

[function] SO-HOM DOM COD

Computes the hom-object of two [SUBSTMORPH]s

14 Mixins

[in package GEB.MIXINS]

Various mixins of the project. Overall all these offer various services to the rest of the project

14.1 Pointwise Mixins

Here we provide various mixins that deal with classes in a pointwise manner. Normally, objects can not be compared in a pointwise manner, instead instances are compared. This makes functional idioms like updating a slot in a pure manner (allocating a new object), or even checking if two objects are EQUAL-able adhoc. The pointwise API, however, derives the behavior and naturally allows such idioms

[class] POINTWISE-MIXIN

Provides the service of giving point wise operations to classes

Further we may wish to hide any values inherited from our superclass due to this we can instead compare only the slots defined directly in our class

[class] DIRECT-POINTWISE-MIXIN POINTWISE-MIXIN

Works like POINTWISE-MIXIN, however functions on [POINTWISE-MIXIN] will only operate on direct-slots instead of all slots the class may contain.

Further all DIRECT-POINTWISE-MIXIN's are [POINTWISE-MIXIN]'s

14.2 Pointwise API

These are the general API functions on any class that have the POINTWISE-MIXIN service.

Functions like TO-POINTWISE-LIST allow generic list traversal APIs to be built off the key-value pair of the raw object form, while OBJ-EQUALP allows the checking of functional equality between objects. Overall the API is focused on allowing more generic operations on classes that make them as useful for generic data traversal as LIST(0 1)'s are

[generic-function] TO-POINTWISE-LIST OBJ

Turns a given object into a pointwise LIST(0 1). listing the KEYWORD slot-name next to their value.

[generic-function] OBJ-EQUALP OBJECT1 OBJECT2

Compares objects with pointwise equality. This is a much weaker form of equality comparison than STANDARD-OBJECT EQUALP, which does the much stronger pointer quality

[generic-function] POINTWISE-SLOTS OBJ

Works like C2MOP:COMPUTE-SLOTS however on the object rather than the class

[function] MAP-POINTWISE FUNCTION OBJ

[function] REDUCE-POINTWISE FUNCTION OBJ INITIAL

14.3 Mixins Examples

Let's see some example uses of POINTWISE-MIXIN:

(obj-equalp (geb:terminal geb:so1)
            (geb:terminal geb:so1))
=> t

(to-pointwise-list (geb:coprod geb:so1 geb:so1))
=> ((:MCAR . s-1) (:MCADR . s-1))

14.4 Metadata Mixin

Metadata is a form of meta information about a particular object. Having metadata about an object may be useful if the goal requires annotating some data with type information, identification information, or even various levels of compiler information. The possibilities are endless and are a standard technique.

For this task we offer the META-MIXIN which will allow metadata to be stored for any type that uses its service.

[class] META-MIXIN

Use my service if you want to have metadata capabilities associated with the given object. Performance covers my performance characteristics

For working with the structure it is best to have operations to treat it like an ordinary hashtable

[function] META-INSERT OBJECT KEY VALUE &KEY WEAK

Inserts a value into storage. If the key is a one time object, then the insertion is considered to be volatile, which can be reclaimed when no more references to the data exists.

If the data is however a constant like a string, then the insertion is considered to be long lived and will always be accessible

The :weak keyword specifies if the pointer stored in the value is weak

[function] META-LOOKUP OBJECT KEY

Lookups the requested key in the metadata table of the object. We look past weak pointers if they exist

14.4.1 Performance

The data stored is at the CLASS level. So having your type take the META-MIXIN does interfere with the cache.

Due to concerns about meta information being populated over time, the table which it is stored with is in a weak hashtable, so if the object that the metadata is about gets deallocated, so does the metadata table.

The full layout can be observed from this interaction

;; any class that uses the service
(defparameter *x* (make-instance 'meta-mixin))

(meta-insert *x* :a 3)

(defparameter *y* (make-instance 'meta-mixin))

(meta-insert *y* :b 3)

(defparameter *z* (make-instance 'meta-mixin))

;; where {} is a hashtable
{*x* {:a 3}
 *y* {:b 3}}

Since *z* does not interact with storage no overhead of storage is had. Further if `x goes out of scope, gc would reclaim the table leaving

{*y* {:b 3}}

for the hashtable.

Even the tables inside each object's map are weak, thus we can make storage inside metadata be separated into volatile and stable storage.

15 Geb Utilities

[in package GEB.UTILS]

The Utilities package provides general utility functionality that is used throughout the GEB codebase

[type] LIST-OF TY

Allows us to state a list contains a given type.

NOTE

This does not type check the whole list, but only the first element. This is an issue with how lists are defined in the language. Thus this should be be used for intent purposes.

For a more proper version that checks all elements please look at writing code like

(deftype normal-form-list ()
  `(satisfies normal-form-list))

(defun normal-form-list (list)
  (and (listp list)
       (every (lambda (x) (typep x 'normal-form)) list)))

(deftype normal-form ()
  `(or wire constant))

Example usage of this can be used with typep

(typep '(1 . 23) '(list-of fixnum))
=> NIL

(typep '(1 23) '(list-of fixnum))
=> T

(typep '(1 3 4 "hi" 23) '(list-of fixnum))
=> T

(typep '(1 23 . 5) '(list-of fixnum))
=> T

Further this can be used in type signatures

(-> foo (fixnum) (list-of fixnum))
(defun foo (x)
  (list x))

[function] SYMBOL-TO-KEYWORD SYMBOL

Turns a [symbol] into a [keyword]

[macro] MUFFLE-PACKAGE-VARIANCE &REST PACKAGE-DECLARATIONS

Muffle any errors about package variance and stating exports out of order. This is particularly an issue for SBCL as it will error when using MGL-PAX to do the [export] instead of DEFPACKAGE.

This is more modular thank MGL-PAX:DEFINE-PACKAGE in that this can be used with any package creation function like UIOP:DEFINE-PACKAGE.

Here is an example usage:
```
     (geb.utils:muffle-package-variance
       (uiop:define-package #:geb.lambda.trans
         (:mix #:trivia #:geb #:serapeum #:common-lisp)
         (:export
          :compile-checked-term :stlc-ctx-to-mu)))
```

[function] SUBCLASS-RESPONSIBILITY OBJ

Denotes that the given method is the subclasses responsibility. Inspired from Smalltalk

[function] SHALLOW-COPY-OBJECT ORIGINAL

[generic-function] COPY-INSTANCE OBJECT &REST INITARGS &KEY &ALLOW-OTHER-KEYS

Makes and returns a shallow copy of OBJECT.

An uninitialized object of the same class as OBJECT is allocated by calling ALLOCATE-INSTANCE. For all slots returned by CLASS-SLOTS, the returned object has the same slot values and slot-unbound status as OBJECT.

REINITIALIZE-INSTANCE is called to update the copy with INITARGS.

[macro] MAKE-PATTERN OBJECT-NAME &REST CONSTRUCTOR-NAMES

make pattern matching position style instead of record style. This removes the record constructor style, however it can be brought back if wanted

(defclass alias (<substmorph> <substobj>)
  ((name :initarg :name
         :accessor name
         :type     symbol
         :documentation "The name of the GEB object")
   (obj :initarg :obj
        :accessor obj
        :documentation "The underlying geb object"))
  (:documentation "an alias for a geb object"))

(make-pattern alias name obj)

[function] NUMBER-TO-DIGITS NUMBER &OPTIONAL REM

turns an INTEGER into a list of its digits

[function] DIGIT-TO-UNDER DIGIT

Turns a digit into a subscript string version of the number

[function] NUMBER-TO-UNDER INDEX

Turns an INTEGER into a subscripted STRING

[function] APPLY-N TIMES F INITIAL

Applies a function, f, n TIMES to the INITIAL values
```
GEB> (apply-n 10 #'1+ 0)
10 (4 bits, #xA, #o12, #b1010)
```

15.1 Accessors

These functions are generic lenses of the GEB codebase. If a class is defined, where the names are not known, then these accessors are likely to be used. They may even augment existing classes.

[generic-function] MCAR X

Can be seen as calling CAR on a generic CLOS object

[generic-function] MCADR X

like MCAR but for the CADR

[generic-function] MCADDR X

like MCAR but for the CADDR

[generic-function] MCADDDR OBJ

like MCAR but for the CADDDR

[generic-function] MCDR X

Similar to MCAR, however acts like a CDR for [classes] that we wish to view as a SEQUENCE

[generic-function] OBJ X

Grabs the underlying object

[generic-function] NAME X

the name of the given object

[generic-function] FUNC X

the function of the object

[generic-function] PREDICATE X

the PREDICATE of the object

[generic-function] THEN X

the then branch of the object

[generic-function] ELSE X

the then branch of the object

[generic-function] CODE X

the code of the object

16 Testing

[in package GEB-TEST]

We use parachute as our testing framework.

Please read the manual for extra features and how to better lay out future tests

[function] RUN-TESTS &KEY (INTERACTIVE? NIL) (SUMMARY? NIL) (PLAIN? T) (DESIGNATORS '(GEB-TEST-SUITE))

Here we run all the tests. We have many flags to determine how the tests ought to work

(run-tests :plain? nil :interactive? t) ==> 'interactive
(run-tests :summary? t :interactive? t) ==> 'noisy-summary
(run-tests :interactive? t)             ==> 'noisy-interactive
(run-tests :summary? t)                 ==> 'summary
(run-tests)                             ==> 'plain

(run-tests :designators '(geb geb.lambda)) ==> run only those packages

[function] RUN-TESTS-ERROR

[function] CODE-COVERAGE &OPTIONAL PATH

generates code coverage, for CCL the coverage can be found at

CCL test coverage

SBCL test coverage

simply run this function to generate a fresh one

[generated by MGL-PAX]

geb's People

Contributors

Stargazers

Watchers

Forkers

cryptozenci junkicide deiver1056 omahs hidenori-shinohara bmorphism anoma jonaprieto sskav7

geb's Issues

Pasteable objects

It would be nice if we could give each other example code over the wired.

To do this I propose the following

We implement the following method

(defgeneric make-eval-form (object))

with the following instances

(defmethod make-eval-form ((object pointwise-mixin)) ...)
(defmethod make-eval-form ((object meta-mixin)) ...)
(defmethod make-eval-form ((object hash-table)) ...)
(defmethod make-eval-form ((object symbol)) ...)
(defmethod make-eval-from ((object number)) ...)
(defmethod make-eval-form ((object string)) ...)

we ideally want to carry over meta-data, however these should suffice to give a term which we can copy and paste to each other

Interpreter for bitc

When #108/#105 gets merged, there will be no interpreter for it.

This makes testing the semantics hard, we should make a followup pr that adds interpreting it, it should relatively easy to do

Geb to Poly Compilation Bug

The to-poly function taking Geb morphisms to the Poly category seems to be faulty. The issue this stems from is #93 and has to do with evaluating the identity function on Bool in STLC - (lamb (coprod so1 so1) (index 0)) - in the empty context.

In particular, the code given by

(to-circuit nil (lamb (coprod so1 so1) (index 0)) :name)

accompanied with the entry code and additional constraint for checking such as name 0 = 0 or name 1 = 1 will fail during the Vamp-IR verification stage.

The interpreters and uncurry allowed to pinpoint that the fault seems to lie in the to-poly compiler step taking Geb morphisms to Poly. In particular, evaluating the object of poly at 0 and 1 gives

(geb.generics:gapply (to-poly (uncurry (coprod so1 so1) (coprod so1 so1) (geb.lambda.trans:compile-checked-term nil (geb.lambda:lamb (coprod so1 so1) (geb.lambda:index 0)) ))) 0) 1/8

(geb.generics:gapply (to-poly (uncurry (coprod so1 so1) (coprod so1 so1) (geb.lambda.trans:compile-checked-term nil (geb.lambda:lamb (coprod so1 so1) (geb.lambda:index 0)) ))) 1) 3/8

(note this code is run in geb.trans) while the correct application should give

(geb.generics:gapply (to-poly (uncurry (coprod so1 so1) (coprod so1 so1) (geb.lambda.trans:compile-checked-term nil (geb.lambda:lamb (coprod so1 so1) (geb.lambda:index 0)) ))) 0) 1/8

(geb.generics:gapply (to-poly (uncurry (coprod so1 so1) (coprod so1 so1) (geb.lambda.trans:compile-checked-term nil (geb.lambda:lamb (coprod so1 so1) (geb.lambda:index 0)) ))) 1) 3/8

The use of gapply in Geb seems to suggest that the STLC to Geb part of the pipeline works fine, so we need to figure out what is going awry with to-poly and fix it.

`bitc` could be extended to support constraints

If we extend the bitc category which exposes VampIR APIs to Geb, then Geb's upcoming equalizers could either be erased by compile-time proofs or compiled to constraints which would alleviate the programmer's need to prove that constraints were satisfied. See #105 (comment) for some details.

Infer type information for STLC application term

Now that we have merged all of #70 (in particular, the new type information added to some STLC terms), we should be able to infer the type information for the STLC application term. We should do so, so that clients (Juvix) don't have to provide it explicitly.

Type for direct access to field elements

As @lukaszcz pointed out in #61 (comment), we should, in addition to the modular arithmetic of #61 , provide a separate type for direct access to field operations.

Geb input format changed

The latest version (on main) doesn't parse the files we generate anymore. It complains:

  no symbol named "FUNC" in "GEB.LAMBDA.SPEC"

The input format should be specified somewhere, and the specification updated with changes.

Geb generates incorrect function for the identity lambda-abstraction

I compile the following

(defpackage #:gg
  (:shadowing-import-from :geb.lambda.spec #:func #:pair)
  (:shadowing-import-from :geb.spec #:case)
  (:use #:common-lisp #:geb.lambda.spec #:geb))

(in-package :gg)

(defparameter *entry*
  (typed
    (lamb
      (coprod
        so1
        so1)
      (coprod
        so1
        so1)
      (index 0))
    (!->
      (coprod
        so1
        so1)
      (coprod
        so1
        so1))))

with

geb.image -i gg.lisp -e "gg::*entry*" -l -v -o gg.pir

The output is:

(...)
def entry x = {
  2 * (((1 * ((mod32 (2 * ((pwless32 (1 * (x + 0)) 1 ((1 * (x + 0)) / 1) (((1 * (x + 0)) - 1) / 1)) + (pwless32 (1 * (x + 0)) 1 (mod32 (1 * (x + 0)) 1) (1 + (mod32 ((1 * (x + 0)) - 1) 1))))) 2) + ((2 * ((pwless32 (1 * (x + 0)) 1 ((1 * (x + 0)) / 1) (((1 * (x + 0)) - 1) / 1)) + (pwless32 (1 * (x + 0)) 1 (mod32 (1 * (x + 0)) 1) (1 + (mod32 ((1 * (x + 0)) - 1) 1))))) / 1))) / 2) + ((1 * ((mod32 (2 * ((pwless32 (1 + (1 * (x + 0))) 1 ((1 + (1 * (x + 0))) / 1) (((1 + (1 * (x + 0))) - 1) / 1)) + (pwless32 (1 + (1 * (x + 0))) 1 (mod32 (1 + (1 * (x + 0))) 1) (1 + (mod32 ((1 + (1 * (x + 0))) - 1) 1))))) 2) + ((2 * ((pwless32 (1 + (1 * (x + 0))) 1 ((1 + (1 * (x + 0))) / 1) (((1 + (1 * (x + 0))) - 1) / 1)) + (pwless32 (1 + (1 * (x + 0))) 1 (mod32 (1 + (1 * (x + 0))) 1) (1 + (mod32 ((1 + (1 * (x + 0))) - 1) 1))))) / 1))) / 2))
};

At the end I add a constraint to test this:

entry x = x;

I run:

% vamp-ir plonk setup -m 14 -o params.pp
% vamp-ir plonk compile -u params.pp -s gg.pir -o circuit.plonk
% vamp-ir plonk prove -u params.pp -c circuit.plonk -o proof.plonk
> [input 0 for x here]
% vamp-ir plonk verify -u params.pp -c circuit.plonk -p proof.plonk

I get:

* Result from verifier: Err(ProofVerificationError)

By the way, the encoding of the identity function needs 2^14 parameters which seems a bit too much.

Error: "not a well-defined APP in said NIL"

What am I doing wrong here?

(defpackage #:test003
  (:shadowing-import-from :geb.lambda.spec #:pair #:right #:left)
  (:shadowing-import-from :geb.spec #:case)
  (:use #:common-lisp #:geb.lambda.spec #:geb))

(in-package :test003)

(defparameter *entry*
  (app
    (lamb
      (list
        (coprod
          so1
          so1))
      (case-on
        (index 0)
        (lamb
          (list
            so1)
          (index 1))
        (lamb
          (list
            so1)
          (left
            so1
            (unit)))))
    (list
      (right
        so1
        (unit)))))

Uncurry Pipeline Usage

Now that we tested out uncurry so that our compilation can be intuitively tested pointwise both in Geb and in Poly instead of passing through the additional isomorphisms, we have a question regarding how to actually implement it.

uncurry currently needs three arguments, two for domain and codomain of the exponential object and one for the morphism we are applying it two. The domain/codomain are needed since we don't have accessors to so-hom-obj.

In order to not burden the user with providing explicit types, we will have to figure out (at least initially until higher-order function translation to Vamp-IR is implemented) how to streamline this process.

Error node needs optimization to reduce introduced circuitry

The error node used by clients to throw a form of exception (see #90 and #129) currently introduces a lot of new circuitry through the addition of many Maybes. This will need optimization. @mariari has suggested introducing a crash type for cases where we don't need to pass errors back but can simply terminate the computation (ideally inducing VampIR to return some selected error code).

geb.image doesn't work (or I'm doing something wrong)

I have a file my.lisp:

(defpackage #:my
  (:shadowing-import-from :geb.lambda.spec #:func #:pair)
  (:shadowing-import-from :geb.spec #:case)
  (:use #:common-lisp #:geb.lambda.spec #:geb))

(in-package :my)

(defparameter *entry*
  (typed unit so1))

I run:

geb.image -i my.lisp -e "my::*entry*" -l

I get:

debugger invoked on a SB-KERNEL:CASE-FAILURE @52D72F01 in thread
#<THREAD "main thread" RUNNING {1001A50003}>:
  (->1 s-1) fell through ETYPECASE expression.
  Wanted one of (SIMPLE-STRING STRING SB-FORMAT::FMT-CONTROL).

I was unable to come up with an input for geb.image which wouldn't cause some kind of error.

Geb error with higher-order functions

Trying to compile:

(defpackage #:ho2
  (:shadowing-import-from :geb.lambda.spec #:func #:pair)
  (:shadowing-import-from :geb.spec #:case)
  (:use #:common-lisp #:geb.lambda.spec #:geb))

(in-package :ho2)

(defparameter *entry*
  (typed
    (app
      (!->
        (!->
          (coprod
            so1
            so1)
          (coprod
            so1
            so1))
        (coprod
          so1
          so1))
      (coprod
        so1
        so1)
      (lamb
        (!->
          (!->
            (coprod
              so1
              so1)
            (coprod
              so1
              so1))
          (coprod
            so1
            so1))
        (coprod
          so1
          so1)
        (app
          (!->
            (coprod
              so1
              so1)
            (coprod
              so1
              so1))
          (coprod
            so1
            so1)
          (index 0)
          (lamb
            (coprod
              so1
              so1)
            (coprod
              so1
              so1)
            (index 0))))
      (lamb
        (!->
          (coprod
            so1
            so1)
          (coprod
            so1
            so1))
        (coprod
          so1
          so1)
        (left
          so1
          so1
          unit)))
    (coprod
      so1
      so1)))

I get:


debugger invoked on a SIMPLE-ERROR in thread
#<THREAD "main thread" RUNNING {7006560003}>:
  Types should match for application: (× (× (+ s-1 s-1) (+ s-1 s-1))
                                         (+ s-1 s-1)
                                         (+ s-1 s-1)) (+ s-1 s-1)

Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL.

restarts (invokable by number or by possibly-abbreviated name):
  0: [CONTINUE] Retry assertion.
  1: [ABORT   ] Exit from the current thread.

(SB-KERNEL:ASSERT-ERROR (GEB.MIXINS:OBJ-EQUALP GEB.MIXINS:DOM TYPE) 2 GEB.MIXINS:DOM (× (× #1=(+ #2=s-1 #2#) #1#) #1# #1#) TYPE (+ #1=s-1 #1#) NIL "Types should match for application: ~A ~A" (× (× #1=(+ #2=s-1 #2#) #1#) #1# #1#) (+ #1=s-1 #1#))

Geb version: 0.2.0

Geb should use VampIR higher-order functions

Now that VampIR has higher-order functions, Geb should compile to them, as that should make them much more efficient than first-order functions translated from higher-order functions via Geb's currying/distributivity equivalence. (The equivalence will still be used to provide Lisp-style quote/unquote; it just won't be needed for higher-order function execution.)

@murisi provided examples of how to use VampIR higher-order functions:

https://github.com/anoma/vamp-ir/blob/main/tests/funcs.pir

`bitc` could be extended to support modular arithmetic

Once we have a Lisp port of #101 to address #61 , we might want to extend bitc to include modular arithmetic on n-bit-width natural numbers, and then make the natural-number backend use bitc. (Indeed, we could consider extending bitc first and porting to it directly.) Then we could continue to consider bitc as the single source of truth regarding what VampIR APIs are available to, and potentially used by, Geb, and the bitc backend itself would have knowledge of the whole program available for potential optimizations.

See this comment to #105 for some details.

Properly artifact between jobs

Currently I'm not sharing artifacts so the CCL tests are not uploaded :(

Make use of VampIR modulus function to decompose products

VampIR now exposes a modulus API; see for example:

https://github.com/anoma/vamp-ir-geb/blob/main/tests/geb.pir

Geb needs to use this to project out of a product.

Make Interfaces/ Open Exhaustion

Problem

Currently we have a fairly good exhaustion system for geb

(defmethod dom ((x <substmorph>))
  (assure substobj
    (typecase-of substmorph x
      (init         so0)
      (terminal     (obj x))
      (alias        (dom (obj x)))
      (substobj     x)
      (inject-left  (mcar x))
      (inject-right (mcadr x))
      (comp         (dom (mcadr x)))
      (pair         (dom (mcar x)))
      (distribute   (prod (mcar x) (coprod (mcadr x) (mcaddr x))))
      (case         (coprod (dom (mcar x)) (dom (mcadr x))))
      ((or project-right
           project-left)
       (prod (mcar x) (mcadr x)))
      (otherwise
       (subclass-responsibility x)))))

where exhaustion is checked at macro expansion time..

However the subclass-responsiblity is not really enforced. We can have an open extension to <substmorph>. For which we don't care about implementing all the interfaces, but some core subset of features. Like we may care about visualizing a particular extension, but we don't support some feature like metadata

Thus I propose the following

Proposal

We should implement the following interface

(definterface <name> <method-name>*)

(implements <class-name> <interface-tuple>*)

interface-tuple ::= interface-name | (interface-name :subclasses) | (interface-name :self)

(subclasses <class-name> <class-name>)

(pledge <class-name> <pledge-tuple>*)

(subclasses-must-pledge <class-name> <interface>*)

pledge-tuple ::= interface-name | (interface-name :self) | (interface-name :superclass)

(pledge-ignore <class-name> <tuple-name>*)

(missing-interfaces <class-name>)
(missing-methods <class-name> <interface>)

With this, we can define out an interface, saying we implement some set of methods. A class implements the interface if it properly fulfills the interface either by implementing it itself or relying on the superclass to do the work.

The pledge function is not strictly needed, as these interfaces can be put in the inheritance list of the class at class creation time, and we can compute later based on the subclass who has pledge to implement what interfaces.

If a class subclasses another one, we can check if the interface is fulfilled, if the interface covers it's subclasses, or is pledged to have it filled by the superclass, then we can remove it from the checked list.

This culminates in the missing-inteface/missing-methods api which tells us how many we are missing.

If we are missing a pledged system, we will get an error instead of a warning for the methods we've pledged.

This should make it easy to see what methods are not exhaustive in the open extension case.

CL is a multiple dispatch system, so we will only check a single specifier works as intended. If more are needed, then an extension to this system should be had

Implementing

The implementation work of this should be somewhat easy. Thanks to the MOP, we can do things like

(c2mop:specializer-direct-methods (find-class 'alias))

(c2mop:generic-function-methods #'geb-gui.graphing::graphize)

These methods should allow us to determine the applicability of methods.

Further we may be able to remove subclasses or rather we should be able to build some of this implicitly.

Further we should make these mixins and likely stealth-mixins if we declare it later.

Heap exhausted

Seems Geb loops allocating memory on this simple program:

(defpackage #:ho0
  (:shadowing-import-from :geb.lambda.spec #:func #:pair)
  (:shadowing-import-from :geb.spec #:case)
  (:use #:common-lisp #:geb.lambda.spec #:geb))

(in-package :ho0)

(defparameter *entry*
  (typed
    (app
      (!->
        (coprod
          so1
          so1)
        (!->
          (coprod
            so1
            so1)
          (coprod
            so1
            so1)))
      (!->
        (coprod
          so1
          so1)
        (!->
          (coprod
            so1
            so1)
          (coprod
            so1
            so1)))
      (lamb
        (!->
          (coprod
            so1
            so1)
          (!->
            (coprod
              so1
              so1)
            (coprod
              so1
              so1)))
        (!->
          (coprod
            so1
            so1)
          (!->
            (coprod
              so1
              so1)
            (coprod
              so1
              so1)))
        (index 0))
      (lamb
        (coprod
          so1
          so1)
        (!->
          (coprod
            so1
            so1)
          (coprod
            so1
            so1))
        (lamb
          (coprod
            so1
            so1)
          (coprod
            so1
            so1)
          (index 1))))
    (!->
      (coprod
        so1
        so1)
      (!->
        (coprod
          so1
          so1)
        (coprod
          so1
          so1)))))

Add modular-arithmetic types to Geb external API

The substobj and substmorph types in https://github.com/anoma/geb/blob/main/src/specs/geb.lisp should be extended with those required for built-in modular arithmetic.

Specifically, there will be a new object called something like fs n for each non-zero natural n (not for zero, because arithmetic mod 0 is Nat itself, and circuits can only support fixed-size natural numbers).

There will be the following new morphisms with the following signatures, where bool is coprod so1 so1, and fs <n> means for every non-zero natural number <n>:

For each natural number m including zero and less than n, const m : so1 -> fs n
inj : fs m -> fs n (injects one bounded type into another -- may wrap around if m > n; equal to id if m == n)
+ : prod (fs m) (fs n) -> fs p
* : prod (fs m) (fs n) -> fs p
- : prod (fs m) (fs n) -> fs p
/ : prod (fs m) (fs n) -> fs p
% : prod (fs m) (fs n) -> fs p
== : prod (fs m) (fs n) -> bool
< : prod (fs m) (fs n) -> bool

Because the arithmetic is modular, overflows just cause wraparound. Division and modulus by zero will produce errors at witness generation time in VampIR. (Once we support dependent types in Geb, we will be able to allow users to include proof content demonstrating that they are not dividing by zero.)

VampIR higher-order functions might be helpful in integrating this with #60 ; see https://github.com/anoma/vamp-ir/blob/main/tests/funcs.pir for examples.

Test compilation of all STLC forms to VampIR

Not all STLC forms yet have tests for compilation all the way to VampIR. I should add tests for all of them. This will depend on implementing at least

#57 , as well as fixing at least
#53 .

I will also need to work out the status of

#58 in the course of doing this.

Possibly-incorrect type error where Geb expects a product type

See this comment to #47. I'm not immediately sure whether this is supposed to produce a type error or not, but I will investigate it and fix it if it's supposed to typecheck. I'm not sure whether there's any relationship with #57 not being implemented yet or not.

Add functor/algebra iteration to Geb external API

Geb is designed internally for its recursive types to be (co)limits of (compositional) powers of polynomial functors, and it should expose an interface to clients to allow objects to be specified as n-fold compositional powers of polynomial functors, and hom-objects as algebras of polynomial functors.

The idea is that the combination of a polynomial functor f, an object a, a non-zero natural number n, and an algebra f a -> a allow a type to be defined with (aside from the addition of the fixed n) the same signature as a recursive one (the recursive type in this case would be the object component of the initial algebra Mu(f) of f, which f, as a polynomial endofunctor, is guaranteed to have), and a function with the same signature as a recursive one (where the algebra of type f a -> a is the function that would be passed to the catamorphism which serves as the elimination rule for Mu(f), but actually producing a type with a finite number of terms, and non-recursive function with signature f^n -> a, which can be executed on a polynomial circuit.

Specifically:

There will be a new (Lisp) type of polynomial endofunctors, poly (or something) on the category substobj/substmorph. It will have the same constructors as substobj plus one more: homf, the covariant hom-functor, which takes a substobj parameter. (All the constructors of substobj apply because the category of polynomial endofunctors also has all finite products and coproducts.)
There will be a binary composition operator on poly.
There will be a functor-iteration operator, something like iterf, which will take a poly and a natural number, and produce the nth iteration of the functor (f^0 is the identity, which is homf so1; f^1 is f; f^2 is f . f, etc.).

There will be an operator apply which takes a poly and a substobj and applies the (object component of the) endofunctor to the object (producing another object).

There will be an operator map which takes a poly and a morphism and applies the (morphism component of the) endofunctor to the morphism (producing another morphism).

There will be an alias alg which takes a poly and a substobj, and it produces the type of algebras: specifically, alg f a is hom(f(a), a).

Finally, there will be a bounded-depth "catamorphism", called something like catan: for each f : poly, n : Nat, a : substobj, and m : alg f a (so m is a morphism from f a to a), catan f n a m will produce a morphism from f^n(so0) (the nth iteration of f starting with the initial object of the subst category) to a. This is the interface that produces a function resembling a catamorphism from Mu(f) to a, but for bounded-depth data structures.

Edit: @lukaszcz pointed out that there's something missing from the above. It's supposed to be a finite prefix of a directed colimit, but the "directed" part means that there are injections f^n -> f ^ (S n), which I forgot to specify. Those should exist, as well as a convenience interface that composes an arbitrary number of them to produce f^n -> f^m for any n < m.

Code generator for Vampir repeats work

Currently my generator is quite bad and can only generate out a single expression.

Either I should improve my code generator, or just use Alucard, as Alucard does this all for me.

Add explicit hom-object type to STLC spec

The substobj type exposed to clients in https://github.com/anoma/geb/blob/main/src/specs/geb.lisp should be extended to include another binary constructor, called something like hom, which constructs the hom-object (the type of morphisms) from its first parameter to its second. (Currently, clients have to compute the hom-object themselves; they should not be subjected to this.)

Geb can straightforwardly compute the hom-object in its Lisp implementation as the types currently stand; it might take a bit of thought to integrate with the upcoming built-in natural number types (i.e. arithmetic mod n for each natural number n-- see #61 ).

VampIR higher-order functions might be helpful in integrating this with #61 ; see https://github.com/anoma/vamp-ir/blob/main/tests/funcs.pir for examples.

Docs Cleanup

After merging @agureev 's work we have the following documentation generation warnings

WARNING: redefining PERFORM (#<STANDARD-CLASS ASDF/LISP-ACTION:TEST-OP> #<SB-MOP:EQL-SPECIALIZER #<SYSTEM "geb/test">>) in DEFMETHOD
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-ADD CLASS>)
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-MULT CLASS>)
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-SUB CLASS>)
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-DIV CLASS>)
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-INJ CLASS>)
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-INJ CLASS>)
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-INJ CLASS>)
WARNING: redefining PERFORM (#<STANDARD-CLASS ASDF/LISP-ACTION:TEST-OP> #<SB-MOP:EQL-SPECIALIZER #<SYSTEM "geb/test">>) in DEFMETHOD
WARNING: redefining PERFORM (#<STANDARD-CLASS ASDF/LISP-ACTION:TEST-OP> #<SB-MOP:EQL-SPECIALIZER #<SYSTEM "geb/test">>) in DEFMETHOD
WARNING: redefining PERFORM (#<STANDARD-CLASS ASDF/LISP-ACTION:TEST-OP> #<SB-MOP:EQL-SPECIALIZER #<SYSTEM "geb/test">>) in DEFMETHOD
WARNING: redefining PERFORM (#<STANDARD-CLASS ASDF/LISP-ACTION:TEST-OP> #<SB-MOP:EQL-SPECIALIZER #<SYSTEM "geb/test">>) in DEFMETHOD
WARNING: redefining PERFORM (#<STANDARD-CLASS ASDF/LISP-ACTION:TEST-OP> #<SB-MOP:EQL-SPECIALIZER #<SYSTEM "geb/test">>) in DEFMETHOD
WARNING:
   No source location found for reference
   #<REFERENCE SO-HOM-OBJ GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC SO-HOM-OBJ)).

WARNING:
   No source location found for reference #<REFERENCE NUM GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC NUM)).

WARNING:
   No source location found for reference #<REFERENCE POS GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC POS)).

WARNING:
   No source location found for reference
   #<REFERENCE NUM-LEFT GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC NUM-LEFT)).

WARNING:
   No source location found for reference
   #<REFERENCE NUM-RIGHT GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC NUM-RIGHT)).

WARNING:
   No source location found for reference #<REFERENCE WIDTH GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC WIDTH)).

WARNING:
   No source location found for reference #<REFERENCE COD GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC COD)).

WARNING:
   No source location found for reference
   #<REFERENCE SO-HOM-OBJ GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC SO-HOM-OBJ)).

WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-ADD CLASS>)
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-MULT CLASS>)
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-SUB CLASS>)
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-DIV CLASS>)
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-INJ CLASS>)
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-INJ CLASS>)
WARNING: "[NAT][]" cannot be resolved.
(while documenting #<MGL-PAX:REFERENCE NAT-INJ CLASS>)
WARNING:
   No source location found for reference #<REFERENCE NUM GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC NUM)).

WARNING:
   No source location found for reference #<REFERENCE POS GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC POS)).

WARNING:
   No source location found for reference
   #<REFERENCE NUM-LEFT GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC NUM-LEFT)).

WARNING:
   No source location found for reference
   #<REFERENCE NUM-RIGHT GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC NUM-RIGHT)).

WARNING:
   No source location found for reference #<REFERENCE WIDTH GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC WIDTH)).

WARNING:
   No source location found for reference #<REFERENCE COD GENERIC-FUNCTION>:
   Could not find source location for ((DEFGENERIC COD)).

would be good to fix them all up

Natural Numbers (un)curry Blow-Up

The current pipeline has good optimization going for it, especially with the STLC reducer. However, abstractly, the user may compiler some code with lambda subterms which are neither on the top nor being applied to. This will cause a huge blow-up that may not even withstand operations with 5-bit natural numbers, much less 24 or 32-bit ones.

We need to resolve this by either thinking about implementing primitive function types or changing the computation strategies for hom-object structures in Geb.

Outline Geb compilation pipeline document

I'm filing this issue with the proposal that we update the description and comments as each of us likes to start building an outline of a document of the Geb compilation pipeline (potentially including not-yet-implemented features). Once we're satisfied with its shape and degree of completeness, we can write a document using that outline.

Mixin API for Categories

Followup from #64. We need a solid API for the base cat-obj category. Please read that issue for context

Geb should expose VampIR error conditions through its STLC API

@lukaszcz made an interesting observation and request:

We’re wondering if there is some failure/error mechanism in VampIR that could be exposed through GEB. This probably doesn’t make much categorical sense, but what we would like to have is some “error” node in STLC that would make the whole computation fail when evaluated. Or some other way of signalling an error. Is it possible to have something like this? This would be useful to e.g. signal that the recursion is too deep - otherwise you need to give some arbitrary element of the right type when you run out of “gas” after recursion unrolling. Or to signal that the user didn’t cover all cases in a match - otherwise one needs to return some arbitrary element of the right type in the unhandled cases. Or to compile debugging assertions.

In other words, we want some way of signalling to the user that a situation occurred which should’ve been impossible but we can’t or don’t want to prove its absence at compile time. Or how otherwise should such situations be handled? Does VampIR have any way of handling them?

To make it clearer, we view these “failure” nodes (that we have in our extended lambda-calculus Core language) more like a debugging facility than a formal part of the language. There is no way to handle failure programmatically. It’s just to signal the user that something went very wrong and their assumptions are not satisfied and to immediately crash the program instead of continuing evaluation with some arbitrary value.

I'll need to learn more than I currently know about VampIR errors and how it exposes them, so I'm pinging @lopeetall to let him know I'll probably be asking him for help. :)

Release Binaries on GitHub Releases

As part of the Juvix-Geb integration, we require access to Geb binaries. Currently, we are able to generate the binaries manually, but for the convenience of our CI process, we would like to request that Geb be tagged and released on GitHub Releases. As soon as we get this, we'd also update the Juvix codespaces to provide Geb as part of the toolchain.

Create a new release on GitHub Releases for each new version of Geb.
Add, if possible, binaries for Ubuntu and macOS to each release.

PS.

For testing, one possible way to incorporate Geb in our GitHub CIs is something like this:

      - name: Install Geb binary
        uses: jonaprieto/action-install-gh-release@2
        with:
          repo: anoma/geb
          tag: latest
          binaries-location: bin # in case you put the binaries in a folder named `bin`
          cache: true

Missing type/object for left and right morphisms

Please consider adding the Object information missing from the left and right morphisms.
Say left a is of object coprod A B, I expect to write in the future left a B, as the object for a can be inferred. We plan to use this info to have a simple type-checking/inference algorithm for the Geb backend of Juvix.

Improve documentation examples.

With the latest examples for the base geb morphisms and objects I was rather lazy in creating examples. It would be best if we diversified the examples making them unique and giving a different perspective on gebs design through each one

Common GEB standard library

Currently we do a mess of mixing serapeum, CL, and the GEB package. Really we should just define out our common-geb and use that.

We can include many common things we want to open. Rest we should just package local nickname as per what we find convenient.

Test failure in `WEAK-POINTERS-WORK`

When I run (asdf:test-system :geb) from the sbcl command line, I get one failure:

;; Failures:
   1/   6 tests failed in GEB-TEST::GEB-TEST-SUITE
   1/   2 tests failed in GEB-TEST::GEB-META
   1/   1 tests failed in GEB-TEST::WEAK-POINTERS-WORK
The test form   count
evaluated to    0
when            1
was expected to be equal under =.

Error node needs extension from `Maybe` to `Either E`

The new error node (see #90 and #129) currently introduces Maybes for places where it passes errors back to clients (see also #132, which proposes an extension to allow clients to choose to crash right away rather than catch and return errors). It will need to be extended to Either E, where E is a client-chosen type. This subsumes not only Maybe (where E is Unit) but also circuits where there are no failures (where E is Void), thus undoing the regression that we can no longer represent circuits that can be statically guaranteed not to fail, as well as allowing clients to distinguish among different, configurable classes of errors.

Potential CL syntax enhancement for ADT readability

@mariari and I have been discussing syntax for Geb's products and coproducts.

I think that it would be nice to view products a * b or a * b * c * d as something like (a, b) or (a, b, c, d), and coproducts a + b or a + b + c + d as [a | b | c | d] (I could be convinced that different symbols would be better). I think it would make it easier to read at a glance where the products were versus the coproducts, and it would make it manifest that * and + are associative, and it would make chains of products look like a single entity such as a record, and chains of coproducts look like a single entity such as a sum type, which I expect is the way that people will most commonly be thinking about them.

`bitc` could expose an intrinsic modulus to Geb (and Geb could expose it to clients)

The bitc category could be extended to expose to Geb the intrinsic modulus of a circuit, and Geb could in turn expose this to clients. This would allow that particular modulus to be done efficiently. See #105 (comment).

geb-morphism frontend

I am sick of writing terms by hand.

(def silly-example
  (comp (mcase nil->list
               (comp cons->list (cons-on-cons geb-bool:true)))
        cons->list *cons*))

is a pain to write, as I have to remember reverse order due to comp, and to evaluate this I have to call gapply on this value. We further can't AOT anything as we are just defining a term bare.

What we need is a DSL

I suggest this

(define-morphism silly-example ()
  *cons*
  cons->list
  (mcase nil->list
         (comp cons->list (cons-on-cons geb-bool:true))))

which reads the arguments as in forth, meaning it's in arrow order which is a more natural way to realistically work

The above expression should expand into something like

(def silly-example
  (optimze
    (comp (mcase nil->list
                 (comp cons->list (cons-on-cons geb-bool:true)))
          cons->list *cons*)))

(defun silly-example (value)
  (gapply silly-example value))

Further, I want more standard library increases, but this should be the first of many such changes

Changing Bitc object structure to a bit-vector or vector

Currently the BITC category uses a list to represents objects and transformations. This is bad, because it is more naturally expressed as a bit-vector.

Here are a few sample documentation for bit-vectors

https://novaspec.org/cl/f_bit-and

https://novaspec.org/cl/t_bit-vector

Further as #101 gets considered, we may want to move it to a general vector instead of just a bit one. Either way it's a better format for this code

Type error for uncomposable morphisms

We need to upgrade the comp functionality so that it does not allow to compose things with non-matching (co)domains and tell us exactly where the error occurs. This will make troubleshooting much easier.

Extensions through Mixins

The central question of open extension should rest on:

Should we

subclass extensions like #61, saying this is a subclass of <substmorph>
extend with a mixin service architecture?

Upon reflection of our current architecture I suggest we follow course 2., and in essence 1. is just 2. in disguise.

With 1. <substmorph> is already an abstract class, meaning it is in essence already an interface.

We can setup this architecture as follows:

cat-morph
cat-obj

Are the new interfaces. They may pledge a core set of functions like:

(dom ...)
(codom ...)
(curry ...)
etc. etc. etc.

Along with #63 we can enforce this through our interface idea. We can use stealth-mixins to implement this fact after class creation

Now, if we want to extend our core category, then we just implement the cat-morph and cat-obj interfaces.

Further the extensions that <substmorph> implements many may not be available in every extension set, and thus we can implement those as part of a new interface set of extensions.

For type checking purposes, if one makes an ADT with slots of a certain type, instead of making them on your concrete subclass, instead make them on the open type cat-morph and cat-obj instead. Our code was previously already doing this with <substmoprh and <substobj>

Thus we should change

(defclass inject-left (<substmorph>)
  ((mcar :initarg :mcar
         :accessor mcar
         :type <substobj>
         :documentation "")
   (mcadr :initarg :mcadr
          :accessor mcadr
          :type <substobj>
          :documentation ""))

into

(defclass inject-left (<substmorph>)
  ((mcar :initarg :mcar
         :accessor mcar
         :type cat-obj
         :documentation "")
   (mcadr :initarg :mcadr
          :accessor mcadr
          :type cat-obj
          :documentation ""))

One conceit of this style of code is that any recursive function must be apart of an interface, but that is fine, we already do that.

(defmethod so-card-alg ((obj <substobj>))
  ;; we don't use the cata morphism so here we are. Doesn't give me
  ;; much extra
  (match-of geb:substobj obj
    (geb:alias        (so-card-alg (obj obj)))
    ((geb:prod a b)   (* (so-card-alg a)
                         (so-card-alg b)))
    ((geb:coprod a b) (+ (so-card-alg a)
                         (so-card-alg b)))
    (geb:so0          1)
    (geb:so1          1)))

Perhaps we can make some general recursive functions, so we don't have to tediously do this for every core functionality, meaning we should be able to derive most of these functions from the core interface. I think @rokopt would have some good ideas on recurses for the data type in particular.

Improve the gui framework

Currently the gui framework implements a naive presentation framework where we present the object and morphisms wholesale.

This leads to an issue like

https://pomf2.lain.la/f/72jatrbs.png

where the object gets redrawn again, with a blank arrow to represent motion.

For objects, this works fine, as the diagram displays clearly, but this does not however work for morphisms, where they are forced to draw the objects, leading to the double draw issue.

Thus I propose the following model.

Share Model

There are two kinds of morphisms, ones that work with morphisms only, and ones that with objects only.

On Objects

If the morphism works on objects (substobj in the codebase), then we make a list:

(list the-input the-morphism-itself the-output)

where the-morphism-itself is the entire morphism. We will, in the presentation map this to it's canonical name (inject-left goes to ι₁) along side a drawn arrow, so the list can be printed directly with no further work.

On Morphisms

If the morphism works on morphisms, then the situation gets interesting, as we would like to share either the the-input or the-output or maybe even share them in elaborate ways! Using just a list structure would only work for composition, it would not hold up on case nor pair/bi.

To solve this problem generally, and to have users be able to extend this structure themselves we have a few APIs

The Object API.

The structure that gets returned, must implement the following functions.

first-object
last-object
take-first-object
take-last-object

first and last return the first and last object respectively, and the take-* variants mutate the structure to hold a new value.

The object in this case is not arbitrary, all values held by the structure, must be unique. Thus by checking that the inputs match each other, we can share the same unique object among all the structures that we care about.

By default we will have the following take the API:

Lists (Created by Composition, and the morphisms which take objects)
Splits (Created by bi)
Merges (Created by Case)

The carrier type will be a list of these in a row, with a share operation that will properly propagate the first into the last

along with a hashtable of the location of each drawn object, so that the same object can be reused in the drawing interface.

The Unique API

An unique value, can simply be seen as a reference over any value. However, we augment this structure with a simple property:

Any two different unique values must not be eq to each other. The unique can only be compared to itself.

Further the unique can talk about it's property, as it is its property. We can realize this in code simply, by just cloning the objects that come in. For the basic clone operation, we will ignore any object that can not be cloned. We will also have a stricter operation that is force-clonewhich will box values which can not be cloned generically (structs or numbers). By default we will not do this, as this could lead to some errors depending.

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.

anoma / geb Goto Github PK

geb's Introduction

The GEB Manual

Table of Contents

[in package GEB-DOCS/DOCS]

1 Links

1.1 code coverage

2 Getting Started

2.1 installation

2.2 loading

2.3 Geb as a binary

[in package GEB.ENTRY]

3 Glossary

4 Original Efforts

4.1 Geb's Idris Code

4.2 Geb's Agda Code

5 Categorical Model

5.1 Morphisms

5.2 Objects

5.3 The Yoneda Lemma

5.4 Poly in Sets

6 Project Idioms and Conventions

6.1 Spec Files, Main Files and Project Layout

[in package GEB.SPECS]

6.2 Open Types versus Closed Types

Methods for closed and open types

Potential Drawback and Fixes

6.3 ≺Types≻

7 The Geb Model

[in package GEB]

7.1 The Categorical Interface

[in package GEB.MIXINS]

7.2 Geneircs

[in package GEB.GENERICS]

7.3 Core Category

[in package GEB.SPEC]

7.3.1 Subst Obj

7.3.2 Subst Morph

7.3.3 Realized Subst Objs

7.4 Accessors

[in package GEB.UTILS]

7.5 Constructors

[in package GEB.SPEC]

7.6 API

7.6.1 Booleans

[in package GEB-BOOL]

7.6.2 Lists

[in package GEB-LIST]

7.6.3 Translation Functions

[in package GEB.TRANS]

7.6.4 Utility

[in package GEB.MAIN]

then: (commutes-left (dom morph)) ≡ (prod y x) u ` Γ, f : x × y → a

7.7 Examples

8 Extension Sets for Categories

[in package GEB.EXTENSION.SPEC]

9 The GEB GUI

[in package GEB-GUI]

9.1 Visualizer

9.1.1 Aiding the Visualizer

9.2 Export Visualizer

9.3 The GEB Graphizer

[in package GEB-GUI.GRAPHING]

9.3.1 The GEB Graphizer Core

[in package GEB-GUI.CORE]

9.3.2 The GEB Graphizer Passes

[in package GEB-GUI.GRAPHING.PASSES]

10 Seqn Specification

[in package GEB.SEQN]

10.1 Seqn Types

[in package GEB.SEQN.SPEC]

10.2 Seqn Constructors

[in package GEB.SEQN.SPEC]

10.3 seqn api

[in package GEB.SEQN.MAIN]

10.4 Seqn Transformations

[in package GEB.SEQN.TRANS]

11 Bits (Boolean Circuit) Specification

[in package GEB.BITC]

11.1 Bits Types

then: `(commutes-left (dom morph)) ≡ (prod y x)` u ` Γ, f : x × y → a