Lambda the Ultimate

Session types greatly augment purely functional programming. Session types enable pure functions to directly model process networks and effects.

We can adapt session types to pure functions by first reorganizing function calls of form `(A, B, C) -> (X, Y)` to a form that uses distinct, labeled input and output parameters, like `fn(in A, in B, in C, out X, out Y)` which we can easily rewrite to a sequential session type `?A ?B ?C !X !Y`. I'm assuming the parameters are easily distinguished, either by distinct data type or by augmenting with named parameters (such as `a:int` vs `b:int`).

Sequential session types conveniently represent that intermediate outputs are available before all inputs are provided. A simple reordering to `?A !X ?B ?C !Y` would correspond to a conventional function type `A -> (X, (B, C) -> Y)`. However, in contrast with the conventional type, the session type is recognizably a subtype of `?A ?B ?C !X !Y` or even of `!X ?A !Y ?B !D`. Thus, we can eliminate most adapter code to relax ordering in the caller. Further, a functional language designed for session types can easily support a direct programming style, e.g. based on imperative reads and writes to single-assignment parameters, thus avoiding the noise of continuation-passing style.

Sequential sessions already demonstrate a trivial model of interaction: the caller can observe the intermediate output `X` before computing inputs `B` and `C`. We can also model 'plain old structured data' types as unidirectional sessions, e.g. a type `!x:int !y:int !z:int` is essentially a record value with labels x, y, z.

Session type systems usually also support choice and recursion.

We can adapt 'choice' to pure functions by assigning a choice-label to a choice parameter and this label determines which subset of choice-specific parameters we'll use. A simple example:

type IF = &{ add: ?x:int ?y:int !r:int
           | negate: ?x:int !r:int
           }

With this definition in scope, the session type `?method:IF` could represent an external choice of 'method'. The choice-label `add` or `negate` might be assigned to implicit parameter `method.case`, and the label chosen will determine whether we further use parameters `in method.add.x : int`, `in method.add.y : int`, and `out method.add.r : int` or `in method.negate.x : int` and `out method.negate.r : int`. This is an exclusive choice, so a compiler could safely 'overlap' memory for these five parameters, similar to a C union. But unlike a conventional union or variant, the choice determines both inputs and outputs. Choice session types can conveniently model object-oriented interfaces or singular request-response interactions.

Aside: Session type systems distinguish external choice (&) vs internal choice (⊕). In the adaptation to functional programming, whether a choice is external or internal is based on whether the 'choice parameter' like 'method' in is input or output. However, it's convenient to represent some choices from the 'external choice' perspective. Thus, use of `&` above allows the type to be syntactic sugar for `{ add: !x:int !y:int ?r:int | negate: !x:int ?r:int }`. When we later provide this type as input, via `?method:IF`, the label is input and all the `!` and `?` types are flipped.

Recursive session types can further augment our functions with unbounded trees or streams of interactions. Conceptually, they allow functions to have an unbounded set of parameters, each with a unique 'path' name. A demand-driven stream type might have a form: `type Stream x = &{quit | more: !hd:x ?tl:Stream x}`. Whether a demand-driven stream has more elements is chosen by the receiver, not the sender. (Session types can also model normal streams, push-back streams, and others.) In context of recursion, our pure function logically has parameters of form `more.tl.more.tl.more.hd`, where `(more.tl)*` may recur in the parameter name an arbitrary number of times.

Use of recursive session types is similar to conventional functional programming with tree-structured data. A compiler or garbage collector can recycle memory for parameters that become irrelevant to further computation. Session types can represent many useful evaluation strategies such as call-by-need or bounded-buffer pushback. Intriguingly, session types can model 'algebraic effects' via recursive streams of request-response choice sessions.

Beyond sequencing, choice, and recursion, we can also extend functional programming with 'concurrent' sessions to represent partitioned data dependencies. For example, with function type `(A,B,C) -> (X,Y,Z)` it's possible to have a data dependency graph of form `(A,B) -> X; (A,C) -> Y; (B,C) -> Z`. It can be convenient to represent this precise data dependency graph in our session type. Fortunately, it's a simple extension to add concurrent types (though concise description, avoiding redundant expression of dependencies like `A`, is non-trivial).

Session types give us a rich model for interaction with pure function calls.

Implicitly, these interactions are between the 'call' and 'caller'. Fortunately, it is not difficult for a session-typed functional programming language to support 'delegation' such that we tunnel handling of interactions to another function call. When we begin to delegate long-lived sessions (e.g. recursive streams) between functions, the program begins to take a form of a 'process network' where pure functions are the processes and delegation models the wiring between them. Use of session types and delegation for purely functional process networks will subsume Kahn Process Networks (KPNs), which are limited to simple streams as the only interaction between processes. With session types, we can effectively model processes that rendezvous, coroutines, processes that have clear bounds on input and output, clear termination behavior.

As a summary, session types for purely functional programming supports:

• a more convenient alternative to continuation passing style
• function types able to directly represent object-oriented interfaces
• a surgically precise alternative to 'call-by-need' vs 'call-by-value'
• streaming request-response interactions for rendezvous or effects
• process networks that tunnel interactive sessions between function calls
• process models and interactions more flexible than Kahn Process Networks
• opportunity to fuse loops and optimize dataflow within the network
• type safety, subtyping, and progress guarantees for all of the above

Session types greatly improve this does not compromise functional abstraction or functional purity, except insofar as unbounded interactions with functions are not what we usually imagine from the mathematical connotations of 'function'.

I have not searched hard for prior art on the subject of session types exposing partial evaluation of pure functions as a basis for interaction and deterministic concurrency. I would not be surprised to discover all this is known in obscure corners of academia. But to me, who has recently 'discovered' this combination, this seems like one of those 'obvious in hindsight' features with an enormous return on investment, which all new functional programming languages should be seriously pursuing.

It's been four years in development, and it'll still be another few years before it's ready to be used in the real world, but we've taken the wraps off the development of the Ecstasy language and pushed a public repo.

The "real" documentation including a full language spec isn't done, but the blog is meant to be a good introduction to the ideas, and relatively easy to chew: https://xtclang.blogspot.com/2016/11/welcome-to-ecstasy-language-first.html

The partial language spec, a text form of the BNF, and other docs are here: https://github.com/xtclang/xvm/tree/master/doc

At a few hundred thousand lines of code so far in the prototype, it's not a small project, but if you're interested in the workings of it: https://github.com/xtclang/xvm

Building this has been some of the most fun that I've ever had as a developer. Finally getting to _use_ it and see it actually running is one of those "sunlit summits".

Peace,

Cameron.

Those of you who apply advanced PL ideas to operating systems might be interested in the upcoming PLOS 2019 workshop. See the abbreviated CFP below, and please consider submitting a short paper!

Thanks! ---

Eric.

Historically, operating system development and programming language development went hand-in-hand. Today, although the systems community at large retains an iron grip on C, many people continue to explore novel approaches to OS construction based on new programming language ideas. This workshop will bring together researchers and developers from the programming language and operating system domains to discuss recent work at the intersection of these fields. It will be a platform for discussing new visions, challenges, experiences, problems, and solutions arising from the application of advanced programming and software engineering concepts to operating systems construction, and vice versa.

Please visit the Web site for more info: http://plos-workshop.org/2019/

I'd like to announce both:

1) the open-source categorical query language CQL and visual IDE:

https://www.categoricaldata.net

based on David Spivak's functorial data migration sketch from his book/course "7 sketches on compositionality:

https://ocw.mit.edu/courses/mathematics/18-s097-applied-category-theory-january-iap-2019/index.htm

2) funding opportunities of up to $1.5M USD for start-ups who want to apply category theory (and especially, the other 6 sketches) to business problems:

https://conexus.ai/ventures

Previous discussion on Hacker News and Haskell-Reddit:

https://news.ycombinator.com/item?id=20376325#20377243
https://www.reddit.com/r/haskell/comments/bs5aiu/mit_spinout_offering_up_to_15m_to_ventures_in/

I propose an algorithm to match facts against rule sets (or against fact sets) which has a time complexity logarithmic with respect to the size of the knowledge base, measured in terms of rules + facts in working memory. As far as I am aware, the current state of the art is polynomial, with RETE derivatives.

There is a description of this algorithm in a reference implementation I have published, in Python (sorry), whose docs can be checked here:

Thanks!

A pretty printing algorithm which works for strict languages with an example implementation in ocaml.

I'm building a relational language where I wish to treat everything as a relation. The main point is to provide a common core of relational operators (aka: Queries) that work across all. A "relation" here is a table with a header of fields, columns and rows.

I have a container that match directly this, that internally is an array:

Now, I have other containers that are Key/Value like a hashmap and BTreeMap, and single value like Generators, ranges and vectors. Only generators, as being read-only forward-only can be say to output a fixed schema.

You can say a hashmap, for example, is a relation that look like:

And a vector one like

With all of them, I wanna provide the same operations like:

table ?where #age = 18
kv    ?where #key =1 
array ?where #it = 2

Now my dilema is what to do for some operations that add or remove columns, like joins and projection:

table ?select *, #age + 10 as older
kv    ?select *, #value |> String.Upper as name
array ?select *, it * 10 as calc

What could be the best option here?

1- Say that kv/array have fixed schemas and can't grow or shrink their headers

2- Say a KV only have fixed the KEY and the value header is flattened, so it become:

[key, value, name]

The problem is not what OUTPUT. I could just output tuples. Is how REPRESENT the relation if it be more than the KV.

So, If I have 10 columns, what is the best option to put inside a KV? Consider that the relational model allow to rename columns, and add and remove them.

Another problem is that KV like Btree allow to model... trees. If I think instead of Btree as a index behind a table, the language lost the ability of "naturally" model trees. BTW, I wanna to have AGDTs.

P.D: Other potential question is: What kind of container could work alike "table" but also alike hashmaps/trees? How model a type that allow several "backends"?

P.D: Originally here: https://www.reddit.com/r/ProgrammingLanguages/comments/awkdrb/for_a_relational_language_how_treat_kv_and/ but not good answers... so I ask here with a bit of more details.

Streaming Language Rewrite Processing (SLRP) is a low-level computing model that is essentially characterized by limited-memory processors rewriting a much larger input stream. Computation under this condition requires multiple passes, but is highly amenable to pipelining and partitioning, and thus parallelism. SLRP processors may have side channels to external devices that we drive through ‘effectful’ rewrite rules.

TLDR: SLRP is a very promising alternative to the von Neumann architecture. SLRP offers advantages for security, concurrency, distribution, and scalability. However, SLRP performs poorly for data plumbing and loops because there is no pass-by-reference within the stream. This weakness can be mitigated by effects, shunting a region of the stream to a remote device and keeping a small placeholder – a reference.

The article develops a Turing complete foundation for a SLRP machine code based on concatenative combinatory logic, and sketches several extensions. The challenge is that the operands for a combinator may be larger than a processor's memory, e.g. for a copy operator `c[X] == [X][X]` the value `[X]` might be larger than what our processor can remember. Thus, a processor cannot simply copy and paste. To solve this involves divide-and-conquer tactics, and a notion of open-ended blocks.

We very recently published a long-ish article on the ParaSail programming language (ParaSail = Parallel Specification and Implementation Language) in the relatively new Journal on the Art, Science, and Engineering of Programming, Volume 3, Issue 3:

ParaSail: A Pointer-Free Pervasively-Parallel Language for Irregular Computations

There is also a new (version 8.0) release of the ParaSail binaries (Linux, Mac, and partial Windows) and sources at:

http://parasail-lang.org

A direct download is available at: http://bit.ly/psl8rel

DZone has published 3 my articles:

• Abstraction Tiers of Notations (Part 1)
• A New Generation of Programming Languages (Part 2)
• On Evolution of Database Languages, Part 3

Few key points from them:

• Abstractions are not created equal and they could be sorted by tiers depending on structural elements they use and the way these elements are used.
• The tiers are closely tied to cognitive development stages as described by J. Piaget and M.L. Commons.
• Each new tier of the abstractions is built upon constructs of the previous tier.
• Adoption of new tier causes major generation of the general-purpose programming language to appear.
• Basing on the model, the next generation of general-purpose programming languages will be likely System-Oriented Programming. That will use ‘system’ as a new category of type that could be instantiated. Current dependency injection frameworks are early and incomplete attempts to implement this new abstraction.
• Basing on the model, the evolution of the database languages should be parallel to the evolution of general-purpose programming languages, with the same abstraction tiers adopted.

Note, I’ve described some elements of this model in some discussions on LtU previously.