A Vision for Relational Programming in miniKanren - William E. Byrd

MiniKanren is an embedded constraint logic programming language designed for writing programs as relations, rather than as functions or procedures. Unlike a function, a miniKanren relation makes no distinction between its inputs and outputs, leading to a variety of fascinating behaviors. For example, an interpreter written as a relation can also perform code synthesis, symbolic execution, and many other tasks. Core miniKanren has only 3 operators:

1. Unification: a two-way pattern matcher. It can be thought of as a type of equality operator. It matches variables on both sides.

   [== 5 5]
   

   This asserts that 5 is equal to 5, and will return False if it isnt. However, if a variable we dont know like `(== x 5)` is put in, x is also 5. This is an assertion. Just like the lisp I am building, each line is seperate. `(eq x 5) and (eq x 6)` is not inconsistent, because they are different branches.

2. fresh: fresh introduces scoped logic variables; goals inside a fresh form are implicitly conjoined.

3. conde: Disjunction. This is similar to lisps cond operator. It allows us to get multiple answers. We can see the result of each clause independently. Each clause represents an alternative logical branch; results are interleaved fairly during search.

   (fresh (y)
   (conde
   ((== x 5))
   ((== x 6))
   )
   

   Will give True, and True. Although the information appears inconsistent.

To move beyond simple scalars (like 5 or 6), we use recursive relations to define grammars. A Lambda Calculus term consists of three parts: Variables, Abstractions (Lambdas), and Applications.

x #variable. . We use the symbolo constraint to ensure a logic variable represents a scheme symbol.
\lambda x. y #abstraction
(f arg) # application

Because these are relations, we can use the same code for three distinct purposes by changing which parts of the call are "logic variables" (unknowns).

• (LC-syn '(lambda (x) x)) Returns Success.
• (LC-syn q) Returns an infinite stream of all possible valid Lambda Calculus terms.
• (LC-syn '(lambda (x) ,q)) and this fills the hole with valid bodies.

(\(\Gamma \vdash e : \tau\)) The "Vision" concludes by showing that an interpreter/type-checker written relationally can perform type synthesis.

• Environment (\(\Gamma\)): A mapping of variables to types.
• Expression (\(e\)): The program code.
• Type (\(\tau\)): The resulting type (e.g., Int, Bool, or a function type).

Now, if you provide an expresion, it returns the type. If you provide a type, it generates all expressions that inhabit that type. This is achieved through the turnstile relation which recursively matches the structure of the expression against the typing rules of the language. OFFENDING LINE: https://google.com