How do you feel now?

Egel has an atypical semantics, one of the most glaring differences with other languages is that combinators are not restricted to one arity. Evaluating an Egel script, therefore, in anthropomorphic terms, boils down to repeatedly asking any combinator: "Do you feel like rewriting yet?"

So far, the Egel interpreter employed a wasteful braindead scheme where every term node was treated like a potential redex, and a thunk was set up for that node. That works well since you cannot reduce a redex twice, but -of course- explodes an Egel script's bytecode and running time.

But it was a robust scheme, so I left it for a long while since there were more pressing issues.

Let's speed stuff up! For that, the aim is to only build thunks for potential redexes. It will be faster but at the same time, due to a lack of metainformation, there's no way around asking combinators whether they will reduce more often than is usual in other languages. Egel will remain sluggish in that regard.

A few rules: A combinator encodes a pattern-matching abstraction that will rewrite a graph to another graph where the latter is built from a combination of variable, constant, and combinator applications. It is useful to see any application as a potential redex, and we call a term in a head-redex position when it's the first member of an application tuple.

• The to-be-reduced combinator, on entry, is responsible for first determining the contents of a thunk.
• Every root node must be treated specially since it may inherit spurious arguments of that thunk.
• Pattern matching will break down a part of the thunk and bind variables.
• A constant will never rewrite, so should never build a thunk, whether it's in a head-redex position or not.
• A variable binds to a reduced term, since Egel has eager semantics, and should build a thunk only when it's in a head-redex position.
• A combinator should always build a thunk since it may always be rewritten.

That should be the rules for the new bytecode emitter.

Egel Distributed Programming

Egel is based on graph rewriting semantics, at any point the program forms a directed acyclic graph of combinators and evaluation is achieved by trampolining the root node. The Egel language is a bare-bones front-end to that semantics, roughly comparable to a lambda calculus with constants where constants compose.

Because of this semantics, a number of things are more 'easy' to implement than in more traditional languages. Egel is implemented in C++ without an explicit garbage collector, parallel evaluation is simply spawning of another root node, and the graph -or parts of the graph- can be serialized, shipped, or saved to disc.

Distributed programming involves picking up parts of the graph and shipping those to a remote node for evaluation. There are various manners in which the model allows for a distributed implementation but I went for a relatively straightforward solution, given the runtime I already had.

Servers, and clients, are implemented atop of Google's Protobuf. Preceding every call, the client does a best-effort scan of the graph and sends a bundle of referenced combinators, the code, to the server. After that, the term is sent and evaluated on the server which will send a term back. Referencing combinators that are not present for whatever reason (for instance, opaque objects like file handles or dynamically loaded c code) is undefined behaviour.

Now for some code, the following defines a server, it starts a service and then blocks waiting for remote calls.

import "egel_rpc.ego"

using System

def main = rpc_server "localhost:50001"

Given such a server, a client can ask for terms to be evaluated. Because the Egel language doesn't have process constructs, we capture what is to be evaluated remotely within a lambda.

import "egel_rpc.ego"

using System

def main = 
    let C = rpc_client "localhost:50001" in
    rpc_call C [_ -> [X -> X] ] 42

In the above example, a lambda is sent to server, that returns the identity function to the client, and the client applies that to the constant 42.

Another example, we generate a list of values on the server, and sum that list on the client.

import "prelude.eg"
import "egel_rpc.ego"

using System
using List

def main = 
    let C = rpc_client "localhost:50001" in
    rpc_call C [_ -> from_to 1 1000 ] |> sum

It works reasonably well but I am still wrinkling out the features.

Note: the Egel interpreter is a hobby project and in beta. It is roughly useable but slow and everything is still subject to change.

Recursion through delayed evalution impossible?

 So, I want to do something in agda, consider the following type:

data Genlist (A : Set) : Set where
  cons : A -> Genlist A -> Genlist A
  generator : ((tt : ⊤) -> Genlist A) -> Genlist A

The type captures the notion of finite but expandable lists. But because agda doesn't understand that delaying a computation can guarantee termination I need to bypass the type checker with a pragma.

  {-# TERMINATING #-}

  ones : Genlist Nat

  ones = generator (\x -> cons 1 ones)

Unfortunately, that also comes with the following cost. You can prove that the type isn't inhabited.

  data ⊥ : Set where

  uhh : ∀ {A} → Genlist A → ⊥

  uhh (cons _ x)    = uhh x

  uhh (generator x) = uhh (x tt)

The type system needed would, apart from allowing recursion with delayed computation, also need to keep track of how often you force a computation.

Oh, really?

 Okay, we have this in Agda:

module I where

open import Data.Unit
open import Relation.Binary.PropositionalEquality

private variable
A : Set

to : (⊤ → A) → A
to f = f tt

from : A → ⊤ → A
from x _ = x

to∘from : ∀ {A} (x : A) → to (from x) ≡ x
to∘from _ = refl

from∘to : ∀ {A} (x : ⊤ → A) → from (to x) ≡ x
from∘to _ = refl

We can abstract away from computation... This makes sense for a total specification language, all computations terminate with some answer and therefore you can substitute that answer.

But it is a bit suspect, and possibly restrictive, at the same time too.

Edit: It's more than suspect but absurd.

Dabbling with Agda

I am dabbling with Agda since I want to do something. Can you figure out what?

module Kripke where

open import Data.List.Base as List using (List; []; _∷_)

open import Data.List.NonEmpty as List⁺ using (List⁺; [_]; _∷_)

open import Agda.Builtin.Unit using (⊤; tt)

{- I want to study finite semantics for temporal logic formula over automata -}

{- Kripke structures, maybe switch to labeled transition systems -}

record Kripke (S : Set) (AP : Set) : Set where

  field

    initial : List⁺ S

    transition : (s : S) → List⁺ S

    interpretation : (s : S) → List AP

{- a tree could suffice to describe the semantics for an automaton

   but fails to capture the unravelling of an automaton in the type

   itself -}

data Tree (A : Set) : Set where

  leaf : List A -> Tree A

  branch : A -> List (Tree A) → Tree A

{- instead, the 'clever' idea is to use the following structure, any leaf node

   can be unravelled further into a tree with a generating function -}

data GenTree (A : Set) : Set where

  branch : A -> List (GenTree A) → GenTree A

  generator : ((tt : ⊤) -> GenTree A) -> GenTree A

{- so maybe first try it for lists -}

data GenList (A : Set) : Set where

  cons : A -> GenList A -> GenList A

  generator : ((tt : ⊤) -> GenList A) -> GenList A