Terminology

Since most of us come from a Haskell/ML background, the bulk of that terminology will be omitted here. However since most of us are unfamiliar with all the other inspirations Juvix is derived from, we lay out such terminology here.

This is probably the most confusing terminology we use. An image is a living changing environment, from which where we can take in new code inputted by the system and/or user and change the world the code lives in. There are many practical benefits of this, see the design section of this web-page for more.

Note that Image is used for more than just programming languages. One can view the kernel of an Operating system as an image (we often do download image files.), or if the operating system is Image based, the entire thing. The terminology also shows up in docker Images.

By effects we typically mean effect systems, and for our implementation we typically use the word, effect/effects, to mean algebraic effect/effects.

The key idea of effects is that a type doesn't only describe the shape of the final computation, but rather an approximation of the various effects it causes when we evaluate it.

Effects have a rather rich history starting in 1987 with the FX-87 programming language. to see the progression of the ideas see the following slide by Benjamin Pierce

Types and Programming LanguagesThe Next Generation (2003) page 36

Desugaring is a word synonymous with macro-expansion, or syntax expansion. It is a process by which we transform one syntax form to another by some abstract syntax transform. See the following example.

  ;; See the S-expression section for slightly more information on this
  ;; structure

  ;; Input generic structure

  (:do (%<- name-1 body-1)
       body-2
       body-3
       …
       (%<- name-n body-n)
       return)

  ;; Ouptut generic structure

  (>>= body-1
     (lambda (name-1)
       (Prelude.>> body-2
                  (Prelude.>> body-n
                             (… (Prelude.>>= body-n (lambda (name-n) return)))))))

In this example we desugared Haskell do syntax into the base monadic operation form.

Core is a term we use to mean a class of Intermediate representation (IR) Layers of the Juvix compiler. These classes of layers deal with the type theory, and is what our fronted syntax desugars into.

Currently there are over 3 layers of Core IR, Core.HR, Core.IR, Core.Erased, etc. You can find out more about those layers over in the overview section.

Interaction Nets are a novel graphical model (graphical as in graph based) of computation. Like all graphs, Interaction Nets, are composed of nodes, edges, and edges which is the spot where the edges connect to on a node. Each node has a single principled port. Each node may be of a different types (Cons is an unique node, so is plus, every operation you can think of is unique.) and have different rules. The rules are limited in that, they can only fire when two principled ports touch, and there is a rule talking about the reduction of these nodes.

Since the operations are limited to principled ports only, the system is trivially parallelizable. There are many other benefits as well. To see some example pictures, click on this wikipedia page here.

We often use the word Parameterization around the code-base pertaining to the various backends. In particular it is the abstraction (interface) around primitives the backend may have.

Such abstractions include but not limited to:

1. The primitive types in the code-base

2. Applying primitive types for type checking

3. A list of builtin values the backend may have

4. Abstractions over various literals in the fronted language

   • Ints, Strings, etc.

Form is a term often used in the lisp world. In Juvix we mean it much in the same way.

Juvix is interesting in that we have the ability to reason over the syntax abstractly. This form, for the sake of ease of use and simplicity, should be as minimal as possible. Thus we have chosen to use S-expressions as our Form.

An S-expression consists of an atom (think symbol, number, string etc.) or a list containing more S-expressions. They are often written as such

  ;; these are examples of atoms
  1
  a
  hi
  +

  ;; these are examples of lists
  (+ 1 2 3)
  (+ (+ 3 4 5) (+ 1 2 3))

They are quite versatile and offer a consistent interface of manipulation throughout the code-base.

A symbol is simply an identifier for some value in the language. For example in

  def foo = 3.

foo is the symbol that when evaluated becomes 3. Some symbols evaluate to themselves.

Symbols are not prefixed, to see more of those see the Name Symbol section on this page.

Name Symbols (Or NameSymbol as in the code-base) are qualified symbols. So instead of saying foo we could say Prelude.foo. There is a distinction, as resolution of non qualified symbols are a bit more implicit and don't explicitly talk about which resolution path they take unlike Name Symbols. There are also some forms (like def) that expect the name they take to be a symbol rather than a Name Symbol, these are often arbitrary choices that may change in the future.