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

Do-notation for chains of transformations

 A particular idiom kept appearing in Egel since I started using `|>` to form chains of transformations, I kept introducing an abstraction to set the chain up with an unknown initial argument.

I pondered on it for a while and introduced `do` syntactic sugar into Egel. The semantics of `(do f |> g |> h) x` is `x |> f |> g |> h` for example. That allows one to abstract from superfluous variables.

It works.  Below, an example taken from Advent of Code '22.

# Advent of Code (AoC) - day 5, task 2

import "prelude.eg"
import "os.ego"
import "regex.ego"

using System
using OS
using List

def input =
    let L = read_line stdin in if eof stdin then {} else {L | input}

val digits = Regex::compile "[0-9]+"

def parse_crates = 
    do map (do unpack |> chunks 4 |> map (nth 1)) 
    |> transpose |> map (filter ((/=) ' '))
def parse_moves = 
    map (do Regex::matches digits |> map to_int 
         |> [{M,F,T} -> (M, F, T)])

def move =
    [(CC,MM) -> foldl 
        [CC (N,F,T) ->
            CC |> insert (T - 1) 
                   (take N (nth (F - 1) CC) ++ nth (T - 1) CC) 
               |> insert (F - 1) 
                   (drop N (nth (F - 1) CC))]
        CC MM ]

def main =
    input |> break ((==) "") 
          |> [(CC,MM) -> (parse_crates (init CC), parse_moves (tail MM))]
          |> move |> map head |> pack

  

I am not sold on the donation, the abstraction also works as a strong visual reminder that a function is being expressed. But maybe it takes some getting used to. Also, it's a nice pun on Haskell monads and a reference to an old thought of mine that all you should need is function composition to chain actions, and that later became applicatives.

That billion dollar mistake. In Haskell...?

This is a short observation on 'the billion-dollar mistake' of Hoare, implementing null pointers in Algol W back in 1965. Dereferencing a null pointer usually causes a runtime error immediately terminating the program, and lots of programs crashed due to that.

This mistake is used ad nauseam to plead for safer languages, which made sense at the time since crashing programs had become the default. What is often not told is that runtime exceptions are standard and must be carefully handled in almost all languages. Let's take Haskell, one of the ostensibly claimed safest languages in the world.

Runtime exceptions can occur due to a variety of reasons, applying a partial function outside its domain is one of them. Let's try 'head []' in Haskell.

λ 
> head []
No instance for (Show a0)
arising from a use of ‘show_M340108553800667339831401’
The type variable ‘a0’ is ambiguous
Note: there are several potential instances:
instance Show a => Show (Const a b)
-- Defined in ‘Control.Applicative’
instance Show a => Show (ZipList a)
-- Defined in ‘Control.Applicative’
instance Show GeneralCategory -- Defined in ‘Data.Char’
...plus 44 others
In the expression:
show_M340108553800667339831401 (let e_1 = head [] in e_1)
In an equation for ‘e_134010855380066733983140134010855380066733983140111’:
e_134010855380066733983140134010855380066733983140111
= show_M340108553800667339831401 (let e_1 = head [] in e_1)
In the expression:
(let
e_134010855380066733983140134010855380066733983140111
= show_M340108553800667339831401 (let ... in e_1)
in e_134010855380066733983140134010855380066733983140111) ::
String_M340108553800667339831401

That didn't go too well, Haskell cannot figure out the particular type instance for an empty list. Okay, let's add an assertion.

λ 
> let x = head ([]::[Int]) in x
*Exception: Prelude.head: empty list

And boom, there you have it. Haskell terminates with a runtime exception. In fact, any Haskell program can have this potential 'bomb' in it. 

What, in the abstract, is the difference between 'nullptr.x' and 'head []'? Both terminate the program due to a runtime exception.

I fully agree that Haskell is a safer language than most imperative ones. But that 'billion dollar mistake'? That is in Haskell too.

Musings on Bell

"Why is a raven like a writing-desk?" So, I've officially joined the ranks of online science cranks with some musings on Bell's inequalities. I am actually pretty much a firm believer in his result, but it was a thought I wanted to expand somewhat further.

I've been right and wrong in the past. I was using a linear transformation from digital circuits to CNF in SAT solving and was pointing out that years before other people noticed that existed, turns out it was a rediscovery of Tseitin mid-sixties; I pointed out that all you need for embedding an impure program into a pure language is a form of composition, so the natural choice for that would be function composition over monads, and Haskell programmers are using applicatives instead. Then a host of small and big views on compiler construction, often as right as they were wrong.

So, the QM thing started off with the notion 'what if superposition is a form of oscillation?' Turns out that doesn't matter much and you need to prove Bell 'wrong' in both cases. A pretty tall order. Especially since this is way out of my field.

But I decided to write it down anyway, maybe it goes somewhere:
https://twitter.com/egel_language/status/1550579321160491013