tags: Alucard

On a Circuit Backend vs DSL

Before we can get onto the question, let us first talk about the interface of Alucard.

The following concepts of Alucard are had

• Function application
• Function Creation
• a binder creator through def
• structs through deftype
• arrays with length and type determining the type
• Prolog style constraints

Let us proced analyzing each feature for both a backend and a DSL

Function Application

when we define a new function (defcircuit bar ((private x int)) x), we end up creating a function with the type bar : int -> int. However on the language level this is really.

bar : Alu int -> Alu int. We create a function type that takes an Alu term of type int and gives back an Alu term of type int.

Thus if we apply this to the rest of the constructs we get fairly nice typing.

This is rather intersting, as it has a few implications.

If we embed the language in an DSL, the barrier between the DSL and the language are obvious, the types dictate that we must take an Alu type. Meaning that function types aren't allowed, but banal types like numbers (which are Alu types) are allowed. If we instead have circuits as a backend, this works wonderfully as well, as we have distinguished parts which should go to the circuit backend versus the normal x86.64 backend.

Thus for Function application, both are equal

Function Creation

For Alucard, I give a custom function definition. This is needed as I need to freeze information.

Under a normal backend, we can reuse the same toplevel definition as the term is like any other, we can simply use the type of the given terms to determine where the values go.

See structure types for a more through deconstruction of some issues.

For this I'll give it a was, and argue it's equally as good depending on how you design the host language.

Binder creation

Binder creation is creating local names, in alucard this is done through def

(def ((foo (+ 3 5)))
  (in-range? foo 20))

What is interesting, is that this is different from let in the language.

(let ((bar (+ 20 30)))
  (def ((faz (array-of bar bar)))
    ...))

The let is the CL let, replacing each use of bar with the definition (+ 20 30). This is quite bad as unlike the host lanugage, we really want bar to be a refernece to the value (+ 20 30). With some hacking around, we can tag each value as unique and then cache the result. The main issue is that the host language's let takes more work and is not obvious. See Issue 30 on Alucard for more information

If we were doing this on a normal compiler, this issue does not exist. We would treat a let as a let, and assume same calling conventions. If the value is an alucard value, we note it's Alu a or a and send it to the appropriate primitives, and depending where it gets used that determines how we compile the term (More on this in the next section).

Structure Types

In Alucard I define my own custom defstruct macro. Under a better language this is not needed, as one would be able to augment the languages defstruct with extra capabilities. For example, slot accessors (fields) in CL are done via method lookup. Meaning that we can dispatch the lookup functions based on the type. And thus reach equivalent calling convention compatability.

For a conventional backend this would arguably be much easier. As we have access to the format of the type, we can make two versions, one that is of type Alu record-type and one of type record-type. We can share accessors, and all the same semantics. This would allow us to switch the representation given the backend we wish to compiler to.

The main issue with both of these, is that we radically change the format of the structure based on the backend. This means that understanding the compilation behavior and semantics is harder than doing it how I did in Alucard (which is making a new structure type definer and have it clearly be tied with Alucard).

Further, for a normal backend style, we have serious issues with generation. Records in circuits are very expensive if we don't inline the packing away. Meaning that if we compile a function let fi point = point.x + point.y, to have the type sig fi : Alu point -> int. Do we have to generate out multiple versions of this function to maintain calling compatability with the rest of the language?

sig fi : Alu int -> Alu int -> Alu int
sig fi : point -> int
sig fi : Alu point -> Alu int

This creates some confusing issues, as we are punning the same type for multiple backends, without a clear way of handling it.

If we decide to separate the two, then the issue is alleviated, but we end up having repeat type declarations in a language without macros. Macros allow us to sidestep this issue as we can make a version which defines out both, or allows us to derive the Alucard version along with transformers (see alien types in Factor and Lisp) to convert between the two.

I'd argue the DSL has some benefits here, as the separation between the use cases is more obvious, and thus the repeat code or transforming between the two seems less awkward.

Arrays

Arrays in Circuits in Alucard are represented both by their type and their length. This is very important for packing reasons.

For a DSL with its own type theory or harkening off a type theory of the meta language tha can type such things all is well.

For a standalone backend this is also fine. However a big caveat is that the type system must be able to understand numbers as apart of a type, thus it forces the hand of the type system.

Both are equally valid ways of tackling the problem, with the latter forcing the hand of the host language.

Prolog Style constraints

Circuits are unique in that prolog style constraints show up. These are impossible to really get out of the host language, as very basic functions will be compiled this way.

For a DSL, this is perfectly fine, as a DSL can bend the rules of the host language.

For a backend this is interesting. I think this can easily be done. We can look at Shen Lisp, which integrates prolog into it's own System. If the host lanugage can produce this, then we can easily make an interface style dispatch, where for x86.64 we compile to the logic matching, and for circuits we have a more efficient representaiton.

the dispatch function can be on Alucard numbers, and thus this should not disrupt the user code in theory.

(defprolog member
  X [X | _] <-- ;
  X [_ | Y] <-- (member X Y);)

(prolog?
  (member X [1 2 3])
  (member X [3 4 5])
  (return X))

> 3

Further considerations

We should also Consider the following quesitons

• Are circuits always domain specific?
• What kinds of restrictions and freedoms ought we have in the host language

The first question is important as STARKS and Nova (RECURSIVE SNARK) show that there exists more general models of circuits. In these models, the backend has the same capabilities as x86.64 just with funky performance metrics.

Final Results

Concept	Backend	DSL	Note
Function Application	✓	✓
Function Creation	✓?	✓?
Binder creation	✓?	OK
Structure Types	Awkward without Macros	✓	see 1
Arrays	✓	✓	see 2
Constraints	✓ In theory	✓

1. For Backend, it's either awkward or hard to do. Depends on how the language is.

2. It's a check mark if the type system allows this type information, otherwise it's a special case and forces the type theories hand on certain ideas.