Proposal: Geb

tags: Juvix juvix-project

Summary

"Geb" (the name is an homage to Hofstadter's Gödel, Escher, Bach; despite being an acronym, it's pronounced as a single syllable and written with only an initial capital letter) is a small programming language which supports:

• Metaprogramming
• Effects
• Dependent types
• Programming languages and mathematical logics as built-in types
• Composition of languages and logics, with individual components defined as universal constructions
• Embeddable within other languages, using its effects to call out of the embedded Geb code to a host language
• Alternative syntaxes – there is a precise specification of which functions an interpreter must support, but no constraint on what syntax a given interpreter should provide, and between any two valid syntaxes, there is a single correct mechanical translation (an isomorphism)
• Category theory as both its internal and its external language, providing both its own implementation and code written in it with access to the huge domain of functions and theorems which have been developed in category theory since its inception

Geb's own logic is weak enough to be typechecked in first-order logic and interpreted in second-order logic, and the language definition is small, so it should be cheap enough to write an interpreter in a given language that we could write interpreters in several of the languages that we use. Because Geb's specification is small and consists entirely of (category-theoretic) universal constructions, code written in it can be unambiguously portable across interpreters. Because its internal logic is so weak, it is a sub-language of almost any other general-purpose programming language.

This potentially provides us an opportunity to build a library of formally-verified code, written in the minimal logic of Geb, which could be executed on many different components of Anoma. For example:

• An Agda interpreter, for internal use by mini-Juvix, particularly for compiler verification
• A mini-Juvix interpreter, or the explicit use of Geb's type system as a sub-system of mini-Juvix's, to provide user code written in mini-Juvix with metaprogramming, effects, and category-theoretic functions and theorems
• As an interface into mini-Juvix for Witch, using Geb's dependently-typed effects
• A Common Lisp interpreter, for Alucard, which might have use for its verifiable metaprogramming
• A Rust interpreter, for strategic ledger and/or crypto code (as well as any validity predicates still written in Rust) for which formal verification would be a worthwhile investment
• There might be some way of using Geb within zk-SNARKs (see below) because its syntax and semantics are both specified by universal constructions, and specifically are encoded as polynomials

Potential applications

Further ambitions

Modestly, I aim with Geb to provide a universal, unambiguous language for defining any other programming language, as well as translations among any other programming languages. "Programming language" itself is a first-class notion within Geb, and Geb itself is a value within Geb's type system.

I don't think this is in theory as instantly implausible as it might sound, in light of the three ways of looking at both logic and programming – logic, type theory, and category theory, as connected by the Curry-Howard-Lambek isomorphism – and of the universality of the Turing machine:

• Gödel showed ninety years ago that even logics barely sufficient to axiomatize the natural numbers can also axiomatize not only themselves but all logics that can be specified computably (I therefore will often refer to such logics as "metalogics").
• MacLane and Eilenberg showed that it is possible to define (many!) universal constructions: definitions of mathematical notions which, although they might have countless surface formulations, may fundamentally always all be treated as the same thing, with the exact same semantics.
• Martin-Löf showed that programming languages may be equated with (defined by) their type theories, and the Curry-Howard-Lambek isomorphism connects type theories with logic and category theory, so when defining languages, we may mix and match notions from logic and category theory with those of programming languages in whatever ways turn out to be most expressive for our specific purposes.
• Turing showed that a universal computer exists, although it sacrifices the potential to be viewed as a consistent logic. But we can, of course, reason logically, and potentially consistently (we can only say "potentially" because Gödel annihilated the notion of absolute consistency), about Turing machines. Turing machines may also have type theories which, although they admit inconsistency and do not ultimately prevent any particular algorithm from being expressed, can vary widely in which programs and patterns they tend to encourage and discourage. Indeed, the most popular languages as of today are all Turing machines, and are distinguished (at the language level – of course there are also wide variations in implementations, libraries, communities, and more) by which classes of programs they make it natural to express, which errors they emphasize preventing, which hardware they allow to be taken fullest advantage of, and other such practical, rather than theoretical, differences.
• Backus's Turing Award lecture proposed the use combinators and algebras of programs to replace the lower-level specification of computation through lambda calculus.

All of this suggests to me the possibility of making a language which is universally useful to the designers of languages and logics – as it must be extremely general, it is specifically not aimed at the direct expression of "business logic" (that is, it is not intended for direct use by application developers); it does not even have a built-in notion of "name" or "definition".

Geb's "Hippocratic oath"

To aspire to universality requires offering something to any language that outweights the cost. This means both finding commonalities that can be factored out among all realistic languages, and imposing so few costs that scarcely anyone would consider them to outweigh the value of being able to share that common code, and thereby automatically begin language development with many useful features available. In the service of this, it is my goal to impose no cost besides the inevitable one of learning the language.

How is it possible to ensure no cost is imposed? It seems to me that Geb must be:

• Minimal: The language must make no assumptions except for those which must be made just by doing language design at all.
• Universal: The language must be defined using only universal constructions, in the category-theoretical sense: any interpretation of any concept defined by Geb must be isomorphic to any other interpretation. This would mean in particular that its specification would be unambiguous: if any two interpreters of it differed in behavior, then (at least) one would be provably wrong.

Loosely, I would say that this must mean it is a requirement of Geb to make no decisions! It must define only those concepts which it is inevitable to define to do language design. A language designer who builds a language upon Geb must never later discover that they have thereby committed to the definition of any concept whose definition could have been anything else.

Technical summary

Later (both in the document and chronologically) I will detail the exact construction of Geb, but for context while considering its potential uses, here is a summary of aspects of the construction:

• It is a dependent type theory whose specification is largely category-theoretical: in particular, it has no names or contexts. This is especially important for defining precise semantics of metaprogramming, which expands the number of possible interpretations of "scope" such that I'm not confident that either names or contexts could be defined in a way that could sensibly be called "universal". There is a history just of hygienic macros which consumes over a hundred pages; I take this as evidence that consensus how names and contexts ought to be managed in metaprogramming is not easily attained.
• In logical strength, it is equivalent (I think) to second-order logic. It is possible that there might be an even weaker specification (Friedman's Grand Conjecture suggests that even elementary function arithmetic might suffice, but I am not sure whether this could be done in a way convenient to programmers. If so, however, then the weaker the better!).
• In presentation, it resembles Lawvere's The Category of Categories as a Foundation for Mathematics: accepting the notion that a category is a good model for a programming language, it posits that the category of categories is a good model for a language for building languages.
• Geb is closed under products and coproducts, and has an initial and a terminal object, but is not Cartesian closed, since it can evaluate only up to second-order functions.

See also the Geb HackMD for LaTeX-paper-style technical documentation.

Purposes

I hope for Geb to serve many purposes within Juvix and even more
broadly in Anoma. For example:

1. A uniform S-expression representation is already in progress; we want to be able to decompose expressions uniformly for tracing, debugging, and assertions, which we can not do with Haskell ADTs. Geb's requirements and specifications can guide which S-expression representation is most likely to be convenient long-term, in particular for metaprogramming.
2. Geb makes the S-expressions into a programming language of their own, and thus allows us not only to represent pipeline steps as transformations of S-expressions, but to write pipeline steps in S-expressions. We can thereby obtain a homoiconic pipeline despite its being written in Haskell.
3. Furthermore, as Geb has (erased) dependent types, we can statically prove correctness properties of pipeline steps (and other Juvix code) insofar as we can write it in Geb.
4. That also means we can metaprogram pipeline steps.
5. We can also represent mutually-recursive pipeline steps using Geb types, as the pipeline step executor can use the Haskell Geb interpreter to interpret Geb types.
6. Geb coinductive types could be used to specify infinite pipelines whose termination is nevertheless guaranteed by their performing structural induction on finite (inductive) S-expressions.
7. Because Geb is a minimal subset of dependent type theories, it is a subset of whatever form of QTT Juvix will eventually become, so any pipeline step (or other Juvix code) that we write in Geb becomes a step towards a fully self-hosting Juvix.
8. Geb offers a potential new subset of Juvix's user-facing type system – one which we can implement quickly once Geb is fully and precisely specified by the Idris interpreter, and which far extends our current type system, to include polymorphic, recursive, and dependent types.
9. Geb provides an interface for Witch (see the technical specifiation for how Geb represents algebraic effects, and the Witch proposal).
10. Geb's being small and clearly specified by a single interpreter in a dependently-typed language (Idris) offers the possibility of using in other languages in particular perhaps Rust for the ledger).
11. As a subset of practically any dependent type theory, Geb could be used as a generic stable compiler internal interface for parts of the compiler which depend only on generic properties of dependent types rather than of QTT specifically. To whatever degree we could achieve this, we would protect those parts of the compiler from changes in the type theory, and thereby give us more flexibility to make such changes, because we discover new opportunities or flaws.
12. Geb defines precise correctness conditions for compilers, which we can use in validating Juvix itself.
13. Geb allows the precise specification of backend semantics, which we could use to validate Juvix's compilation to LLVM and other places.
14. Geb could in the future allow Juvix to compile multiple, including user-defined, languages/type theories, making it into a library for general mathematical logic and programming language development.
15. Geb can serve as a type theory playground which, by allowing type theories to be defined as extensions of itself, also allows them to inherit its features such as metaprogramming and algebraic effects, which derive from its reflection.
16. In that context, it can be used to check soundness proofs for type theories themselves.
17. Geb can be used to define precise algebraic effects semantics, and prove that Witch provides them.
18. Geb allows strongly, dependently-typed metaprogramming so that its extensions can be written in itself and have properties about themselves proven in itself.
19. Geb will allow the replacement of structure generator and other Haskell-generating code with a language that will be a subset of Juvix, and offers dependent types.
20. Geb allows the precise specification of required behavior of an interpreter, such as in Haskell, Rust, or Idris, or operating system.
21. The way in which datatypes are defined in Geb provides **automatic "datatypes à la carte".
22. Having a uniform representation of all expressions (in all languages!), and a Lisp-like one at that, might help support specification of image semantics.
23. Geb allows the precise specification of correctness of transformations on the real-world effects of the code being transformed.
24. Being a uniform, category-theoretically-universal construction for the representation of languages and logics might allow Geb to be used as a protocol for the exchange of formal knowledge, for example by giving it an ipld content identifier.
25. I don't have nearly enough domain knowledge to be confident, but I can imagine that it might be possible, because the specification and compilation of Geb is so regular, to prove that a given Geb term had been type-checked as a given type by a known Geb compiler using ZK-snarks, providing zk-snark verified installation – users could ensure that they were installing only programs that had provided proofs of the properties that they desired, without having to compile those programs themselves (which might be infeasible, for example in large-scale cases such as installing a mobile-phone operating system on a mobile phone).
26. I'm not sure about this, but I'd like to investigate whether it's possible to use type constructor tensor products to reduce duplicated code in annotated structures such as the TermClosure in PR 1080.

Technical specification

Geb may be viewed as a syntax which interprets a second-order logic as a minimal dependent type system which reflects all type systems and thereby allows languages themselves, and interactions between them, to be treated as first-class objects. Specifically, we begin with a second-order logic, which we call the "core logic", defined categorially as follows:

• An initial object (which is first-order)
• A terminal object (which is first-order)
• Finite products (of the same order as their arguments)
• Finite coproducts (of the same order as their arguments)
• Exponential objects for first-order objects, where the exponential objects themselves are second-order
• An object which reflects the objects of the category, in the sense that Gödel used the natural numbers to reflect propositions of arithmetic theories: logically, therefore, this is equivalent to specifying that the category has a natural numbers object; Geb express the reflection algebraically rather than numerically because it is intended more for programmers than for mathematicians. Reflected objects are introduced by the Gödel operator for objects.
• For each pair of objects, an object which reflects the morphisms from one of the pair of objects to the other, in the same sense that Gödel used functions on the natural numbers to reflect axioms and theorems of arithmetic theories. Reflected morphisms are introduced by the Gödel operator for morphisms, and eliminated, by evaluation, by the "Turing operator".
• For each polynomial endofunctor, where the polynomial endofunctors are defined in terms of the reflection objects as morphisms from first-order types to the reflector objects, an initial algebra and a terminal algebra, with corresponding evaluators (fixpoints and co-fixpoints)

Having defined that category, we then define Geb as a syntax for it – in effect, interpreting some of the types of that category as representing programming languages. Specifically:

• A constructor is a second-order morphism with a second-order domain and a first-order codomain. We call this a "constructor" because we will interpret a constructor as a typechecker for a datatype constructor, where the second-order domain is the constructor's parameter (its being second-order means that it can include functions, which allows the constructor to call other constructors to typecheck input types) and the first-order codomain is the output type's parameter.
• We may build products and coproducts of constructors, but we may also define two constructor tensor products corresponding to mutually-recursive types and to datatypes à la carte.
• A (programming) language (/logic) is defined as a free extension of Geb (which is exactly equivalent to the above second-order logic) through constructors for its objects and morphisms. This makes Geb, the minimal language for defining languages, into a protocol which all languages share for the definition of languages themselves. A language (or logic) is identified by the constructors of its objects and morphisms. Languages may be viewed as Geb's universe hierarchy – but it is not a hierarchy; since it includes all recursively axiomatizable languages, most pairs of them are incomparable.
• Because all objects and morphisms of all languages are reflected (not, of course, interpreted!) as objects and morphisms of Geb, it is sensible to specify semantics of languages which include computation (effects) within Geb, which is only a logic.
• Furthermore, because of that reflection, it is possible to speak of morphisms from one language to another. This is how Geb represents handlers for algebraic effects: it is possible to evaluate a morphism from language A to language B precisely when language B can implement, in terms of its own object and morphism constructors, the object and morphism constructors of language A.
• Dually, well-typed metaprogramming emerges from the morphisms among the reflector objects.
• It is possible to specify the correctness of transformations in terms of equivalence of effects.
• It is possible to specify the correctness conditions for an interpreter (or compiler) for Geb itself, as Geb is simply one of the langugages which it reflects: the minimal one, with no free constructors for objects or morphisms beyond the "built-in" ones inherited from second-order logic.

Implementation plan

• The most urgent step is to implement the first interpreter, in Idris so that we may thereby prove its soundness, and some properties of it.
• The interpreter gates most of the rest, but it is possible in parallel to port the S-expression representation to Haskell for use in Juvix.
• Once the Idris interpreter is shown to work, we should port the Idris interpreter to Haskell.
• That will allow us to write pipeline steps in Geb (within Haskell), enabling us to metaprogram them and use dependent types to prove their correctness.
• We can also port Geb to Juvix's type system – meaning, making it available to users. Since it is a minimal system practically guaranteed to be a subset of any theory that will end of being Juvix's (i.e. anything remotely resembling QTT), this will not risk future breakage of backwards compatbility (as far as semantics are concerned – we will have to think some about the syntax, unless we want to be particularly conservative and expose the Geb type system only through built-in introduction and elimination functions).
• We can integrate with Witch through Geb's means for specifying algebraic effects and handlers through cross-language morphisms (see the Technical specification).
• As the interpreter ought to be small (especially without proofs), we could port the interpreter to Rust (perhaps among other languages) to allow the use of dependent types in Ledger / Distributed Systems code.
• Test the extensibility of Geb within itself, and the transitivity of that extensibility, for:
  • Defining new logics: Use Geb to define higher-order logic
  • Transitively defining new logics: Then use higher-order logic to define some other logic (weaker or stronger, or both)
  • Defining new programming languages: Define some programming language within Geb; particularly important examples:
    • A Turing machine
    • A non-deterministic machine
    • A language with run-time type errors (strong but dynamic types)
  • Defining logics/languages through effectful compilers/interpreters: An example would be Witch, which will allow a programmer to depend upon external proof assistants and/or interactivity (see perhaps Chris Martens's logic for interactive sytems?)

Work breakout / timeline

Phase 1: Initial release

Phase 1 provides:

• First-order dependent and quotient types
• Metaprogramming
• Abstract syntax

This is the point I need to get to to deserialize the project, allowing multiple people to work on it.

Task	Duration	End date	Status
Complete Idris encoding of polynomial endofunctors	2 days	Thu June 2
Add dependent endofunctors to encoding	3 days	Tue June 7
Implement bounded monotone functions in dependent endofunctors	3 days	Fri June 10
Implement equalizers and coequalizers for bounded monotone functions	5 days	Fri June 17
Add dependency to bounded monotone functions	5 days	Fri June 24
Encode theory of first-order (enriching) category in terms of dependent bounded monotone functions	10 days	Fri July 8
Idris-internal S-expressions for initial abstract syntax	5 days	Fri July 15

Phase 2: Portability

Phase 2 provides a simple concrete syntax which can be used to share Geb code amongst different host languages, and documents on how to use it.

Once this phase is complete, it will be possible to start writing parsers/interpreters/compilers for other host languages/environments, so our own applications of Geb, which could be in any or all of original Juvix, mini-Juvix, the ledger, validity predicates, and Alucard, as we choose, could begin (as described in phase 5) any time after this phase, and could be done in parallel with phases 3 and 4.

Task	Duration	End date
Some study of parsing packages	2 days	Tue July 19
Simple S-expression parser in whatever package we choose	3 days	Fri July 22
Idris parser for testing syntax in initial interpreter	5 days	Fri July 29
Documentation and examples / code cleanup (removal of obsolete false starts!)	5 days	Fri Aug 5

Phase 3: Full language

This phase provides:

• Full mathematical context for the theory of Geb
• Effects (as categories)
• Integration with host environments (in particular, including the Anoma network or the ledger) through effects
• Different logics (as higher categories)
• Multiple programming languages within a single language (also as categories)
• Integration point for proof assistants (through effects)
• Deserialization: after this phase, not much will depend on other things; work could be done in parallel

This and future phases will be written in Geb itself, though I will also be writing Idris interpretations for the new categories in tandem, for validation and as an example to any other interpreters/compilers that I or anyone decide to write in order to use Geb in other projects.

Task	Duration	End date
Representation of category theory enriched over the category developed in Phase 1	15 days	Fri Sep 2 (I'm adding a week assuming that the retreat will interrupt this development)
N-order and higher-order logic categories, with Idris interpretations	10 days	Fri Sep 16
Infinite data types through terminal coalgebra adjuction	10 days	Fri Sep 30
Turing-complete programs through arbitrary-evaluation adjuction	10 days	Fri Oct 14
Type theories, logics, and programming languages "à la carte" through definition of categories via adjunctions	15 days	Fri Nov 4
Documentation and examples	15 days	Fri Nov 25

Phase 4: Language ergonomics

This phase provides some foundational features to allow Geb to feel like what programmers generally expect from a programming language.

Because work can be done in parallel in this and following phases, and also wouldn't need continuous attention anymore but could be done in intermittent chunks, I'll provide some (vague) estimates of duration, but no end dates.

Task	Duration
Definitions and global contexts through a (mixin) category which is under a reader monad	10 days
Record/ADT-like data access through profunctor optics	10 days
Mixin category for monads	10 days
Richer syntax exposing the distinctive features of Geb	15 days
Integration with various IDEs (Language Server Protocol, emacs, …?)	20 days? (depends on how many we want to do)

Phase 5: Initial applications

This phase illustrates possible early uses of Geb, in particular by Heliax.

Task	Duration
Integration of full Geb definition into the work that I've done on Juvix to allow Geb to integrate with it (this would provide a full compiler containing Geb – it's one that we're discarding, but it might be useful for experiments and extracting useful code from)	10 days
Agda parser/interpreter to allow the use of Geb in mini-Juvix	15 days
Rust parser/interpreter to allow the use of Geb in the ledger and/or for validity predicates written in Rust	15 days
Common Lisp parser/interpreter to allow the use of Geb in Alucard	10 days

Phase 6: Ongoing library/community development

This phase is not only deserialized, but also possible to do intermittently – a day here or there by anyone as they have time and interest. If Geb becomes established, this represents the kind of work that "never" ends. Therefore I won't even provide durations or specific tasks for this phase, only broad ideas of the kinds of work that could be done.

• Libraries for / examples of validity predicates
• Ongoing examples / documentation
• Paper publication(s)
• Community engagement through conferences / online presentations / blogs
• Libraries for category theory and other foundational mathematics/logic, to provide generic theorems and functions to all Geb code
• Integration with proof assistants, through development of Witch – initially for mini-Juvix, but because of Geb's portability to other languages, the results would also apply to any other languages for which we (or anyone else) wrote interpreters
• Encoding of foundational computer science in category theory, for globally-shared representations of it
• Encoding of other formalizable disciplines in Geb, to allow globally-shared representations of them as well (presumably by domain experts, which will only happen if Geb catches on, of course!)
• Integration of logics, which Geb can verify formally and provide universal representations of, into the Anoma network for use by validity predicates, in particular for forms of coordination such as distributed negotiation, trust, and causal and other kinds of modeling
• Research into and possible implementation of the use of zk-snarks on Geb programs, for example for verification of compilation of programs by trusted compilers – I'm not sure whether this will turn out to be possible or not, but Geb programs are fundamentally polynomials, which vaguely suggests to me the possibility (I just don't know enough about zk-snarks to say how real it is)

"Compiler perspective" guide

This section is intended as a guide to syntax and evaluation of Geb for compiler writers, initially for the "Heliax compiler squad" meeting. (See also See also the HackMD.)

Background

Understanding Geb requires that, while it is a programming language, it is also an embedding language for potentially any other programming language, as well as, by virtue of being a minimal language (among languages capable of expressing metalogic), able to be embedded within other programming languages.

One view of it is therefore as a protocol for interoperation amongst programming languages.

Another view of it is as a specification language for programming languages, one which dictates precisely what it means for an implementation of a language to be correct and no more – if the specification of a language does not dictate precisely which machine-language instructions that expressions must be compiled to, then Geb does not specify it either.

The way in which these multiple roles are expressed is that Geb makes explicit in its syntax and semantics that it may be used in any of the three equivalent ways related by the Curry-Howard-Lambek isomorphism: a logic, a programming language (type system), or a category. (This is true of all languages; the difference between Geb and other languages with which I am familiar is that Geb makes it explicit.)

One consequence of this in the Geb syntax is that the signature of an expression includes more than a type: it includes a programming language and a type of that language. (A programming language may be parameterized, so a single expression might be valid within a family of programming languages.)

Among the three concepts related by Curry-Howard-Lambek, the one in which Geb itself is specified (including by Geb itself) is category theory. Therefore, an expression's language is denoted by a category, and its type by an object of that category (in the case of a type declaration) or a morphism of that category (in the case of a function declaration).

The category which comprises Geb's core logic – which is (necessarily, to meet its goal of being minimal, hence embeddable in any practical general-purpose programming language) a simple first-order-recursive arithmetic – has two different expressions in Geb's syntax, between which there is a categorial equivalence (an adjunction whose unit and counit are both natural isomorphisms):

• An ordinary one-category, in which context it serves two purposes:
  • The category over which all categories (in other words, all programming languages) defined in Geb are enriched: this is a category-theoretic formulation of the notion of "representing" types and terms of languages within Geb
  • The category in which all categories defined in Geb are specified: in this context, Geb may be viewed as the "background logic" used in Geb for reasoning about programming languages (for example, for users to prove properties of their programs, and for compilers to verify properties of their transformations)
• A two-category, in which context it serves to define programming languages; in particular, one category in this two-category is Geb itself

One consequence of Geb's category-theoretic expression is that its abstract syntax is a combinator calculus, not a lambda calculus. (As an embedding/specification language, it can specify and contain sublanguages which are lambda calculi, but the native logic of Geb itself is not one.) Its syntax therefore resembles Backus's FP or FL than, say, Lisp or Haskell – although Geb is homoiconic, like Lisp and unlike FP or FL.

Also crucial is that the only syntax specified for Geb is abstract: which category-theoretic notions are expressions of Geb. There is no specification of a concrete syntax, such as a BNF. Concrete syntaxes are entirely up to individual Geb interpreters/compilers; they are required only to be isomorphic to the abstract syntax, so there is an infinite variety of valid concrete syntaxes for Geb. (One application would be to specify a particular concrete syntax or collection of concrete syntaxes as an open standard; because of the isomorphism, individual compilers/interpreters could then translate back and forth between their own concrete syntaxes and one of the open-standard ones, and then it would be possible to translate mechanically between any two Geb implementations' via the composition of their isomorphisms with the open standard.)

Syntax

The syntactic elements of Geb correspond to the core constructions of category theory, as follows.

Category (programming language)

There are a few built-in categories which can be used as the "category" component of a declaration. All the built-in categories are defined by which universal properties they contain (the objects and morphisms are precisely the ones whose existence is required by those universal properties); the built-in categories are as follows, with the universal properties they contain:

• Unrefined0
  • Initial object
  • Terminal object
  • Products
  • Coproducts
  • Exponentials
• Refined0
  • All of the objects in Unrefined0, plus:
    • Equalizers
    • Coequalizers
• Unrefined1
  • All of the objects in Unrefined0, plus:
    • Initial algebras of polynomial endofunctors of Unrefined0
• Refined1
  • All of the objects in Refined0, plus:
    • Initial algebras of polynomial endofunctors of Refined0

Refined1 is the core logic of Geb itself, so as a category it might also be referred to as Geb (this is one of the senses in which Geb is homoiconic).

Other categories may be constructed from the built-in categories by the applications of the following category constructors.

As a two-category, Geb is cartesian closed, so we may form the terminal category 1, and for any two categories C and D we may form:

• Product[C, D]
• Functor[C, D]

In addition, because Geb includes the core concepts of category theory as explicit elements of its syntax and semantics, and because those concepts themselves form categories, we may also form, for any categories C and D, the following categories:

• NaturalTransformation[C, D]
• Adjunction[C, D]

To provide notions such as the category of morphisms of a category (which is also known as its arrow category) and the slice categories of a category (which are used in the standard category-theoretic definition of dependent types), we provide a category constructor which generalizes those notions and others, namely the comma category; for any functors F and G we may form:

• Comma[F, G]

Besides the arrow and slice categories, another important special case of the comma category is the category of terms – for any object X, we may form a category whose objects are morphisms from the terminal object to X, and whose morphisms are, for each pair of morphisms a, b : 1 -> X, all of the endomorphisms f : X -> X such that f . a = b. One way of defining that category (for an object X in a category C) is as Comma[F, G] where:

• F is the functor from the terminal category to C whose value (on its only input) is the terminal object of C
• G is the inclusion functor into C from the full subcategory of C whose only object is X

A consequence of being able to define the category of terms is that any of the ways of defining an object (see below) may therefore also be used to define a category (by defining the object and then constructing its category of terms).

Object (type)

Each built-in category or category constructor has ways of constructing objects of that category. Objects are inductively constructed by the application of universal properties.

The built-in categories (Unrefined0, etc.) have precisely the object constructors listed in the "Category" syntax section above. Those categories also, however, comprise the built-in logic of Geb, and as such must not only be typecheckable but also interpretable by any Geb interpreter. The reference interpreter (the one being written in Idris-2) provides direct access to what could be viewed as Geb's "assembly" language through additional constructors for the built-in categories which reflect the way that the interpreter internally represents objects and morphisms of those categories. Specifically:

• Equalizers are implemented internally by predicates which, when we view objects as types, can be viewed as excluding terms from types. An object of Refined0 may therefore be constructed from a pair of an existing object and a decidable predicate on that object (a decidable predicate on the object is a morphism from the object to Bool, or more generally to any Either type).
• Coequalizers are implemented internally by normalization functions. When we view objects as types, these may be viewed as automatically converting the terms of a type into a "normal form", thus ensuring that any terms which normalize to the same term are treated the same way by any functions defined on the type. An object of Refined0 may therefore be constructed from a triple of an existing object, a decidable predicate on that object, and a function from terms which do not satisfy the predicate to terms which do satisfy the predicate. The predicate, therefore, decides which terms are considered "normalized", and the function converts non-normalized terms to normalized terms.

XXX objects of constructed categories (functor applications)

Morphism (function)

XXX morphisms of built-in categories
XXX morphisms of constructed categories (functor applications)

Functor (polymorphic datatype)

All functors definable in the core logic of Geb are polynomial; as such, they are constructed inductively from the following constructors:

• Coproduct (of a list of functors)
• Covariant hom-functor (represented by a specified object)
• Dependent coproduct (specified as a functor to a functor category, where the dependency can be viewed as being on a type if the domain of the functor is the category of terms of that type)
• Dependent covariant hom-functor (where the domain depends on a category by being a functor from that category rather than a single object, and, as with the dependent coproduct, can be viewed as depending on a type if the domain of the functor is a category of terms)

Natural transformation (polymorphic function)

Adjunction (computation rule)

Evaluation

See also:

• Compiling to Categories
• Categorical Combinators, Sequential Algorithms, and Functional Programming
• Generic Programming With Adjunctions

Built-in adjunctions

Integrations

Embedding Geb within other languages

Parser + interpreter

Parser + compiler

Library

Embedding other languages within Geb