LtU Forum

Process Network for Effects, Monad Alternative

Monads are an awkward effects model in context of concurrency. We get incidental complexity in the form of futures or forking threads with shared memory. The running program becomes entangled with the environment, which hinders persistence and mobility and debugging. So I sought alternatives in literature.

Kahn Process Networks (KPNs) seem like a very good alternative. From an external perspective, they share a lot of similarities to monads, except we get more than one input (continuation) and output (effect) port and thus can model concurrent operations without relying on effects or environment support. Internally, KPNs have a lot of similarities to free monads: we can compose KPNs to handle effects internally, translate them, etc.. Use of KPNs as first class values allows for dynamic structure and mobile processes.

The main feature missing from KPNs is the ability to work with asynchronous inputs. But it is not difficult to add time to the model, and thus support asynchronous messaging and merges in a style similar to functional-reactive or flow-based programming (and somewhere between the two in terms of expressiveness). I doubt this is a new idea.

I've written about these ideas in more detail on my blog:

Reactive KPNs with open ports or channels also make a better FRP than most, having a far more direct API for pushing inputs and pulling outputs deep within a network.

Defining recursive function as a monad (or other solutions)

Is it possible to create recursive function using monads in a functional language?

definition of monad in a functional language should look like: "a->(a->b)->b". Is it possible to have "a" as a parameter, get "b" as a result and recursively repeat it until some condition is satisfied? I've been strugling over factorial example, but I don't see a clear solution.

The reason I'm asking is that I'm defining a language where functions are passed around together with applied parameters. If I repeatedly call a function by a recursion, new data sums with previous data that was there before the recusion was applied. So finally I'd get a set of all intermediate results, while I'm interested only in the final result. I'm not even sure if monads would work in this environment with data stitched to function calls.

Actually, a solution I can use is first to create a set of parameters of each recursion step, and then to call some kind of fold function over the set that produces a single result. But I want to explore other possibilities, so I'm interested in monadic or other solutions.

Thank you for your time.

Eliminating left recursion

Does anyone have a reference to a correct algorithm which eliminates left recursion from a grammar? The one in Wikipedia is incorrect. Lots of youtube videos and lecture notes Google finds are also incorrect. All make the same mistake, they forget that a production A = N A X is left recursive if N is nullable. Requiring the grammar to be null free would be absurd since the algorithm itself inserts epsilon productions.

I also wish to extend the requirement to an attribute grammar of the form usually used in practice, with an extra symbol kind for AST construction, etc, which cannot be eliminated and yet recognises the empty string.

BTW: I'm looking for the basic algorithm. Lost my copy of the Dragon Book ;(

Splitting witnesses up


I have an idea for an academic paper, and am seeking help for prior art and research.

My idea is about proof witnesses, and what to do when a group of witnesses contradict each other (software bug/logical inconsistency), and repairing the proof. Without going into details on the algorithm, the metaphor is simply to split witnesses up, using a mathematical plane to draw a group of witnesses into two groups: definitely lying (the witness whose account is proven contradictory/false), and somewhat certain (witnesses with similar testimonies who have not yet been proven contradictory/false, but might once asked further questions or may be proven "good enough" given the new questions/evidence we've asked the witness about). My idea comes from witness interrogation techniques in the real world.

Since I haven't been active in PLT for several years, my knowledge of what to search for and keywords to use on ACM and IEEE search engines is pretty weak, and I could use some tips.

Thank you very much!

Any recent developments on "active libraries" that I'm missing?

I'm interested in libraries that guide compilers for optimizations, but it
seems like there isn't much literature on this topic.

- Papers like "Generative Programming and Active Libraries" which usually just
briefly talk about the idea and give the same examples like Blitz++.

- There's a thesis, "Active Libraries and Universal Languages", which as far as
I can see is a bit too light on the practical examples and implementation.

Two implementations that work well:

- I think Haskell libraries that use GHC's rewrite rules are "active libraries"
in this sense

- The stream fusion library described in POPL'17 paper "Stream Fusion, to
Completeness" is an example that's a recent work and one that works really
well (although it has problems like leaking `code` type to the user in
functional arguments).

These are pretty much all I can think of as examples. I'm looking for recent
developments and other practical examples (i.e. ones that work well and/or used
widely). Any pointers would be appreciated.

Resources for implementing higher-kinded types?

I’m working on a language and I would like to implement polymorphism over type constructors (for functor, applicative, monad, etc.) but I’m uncertain how to proceed.

Can anyone recommend tutorial-style resources or sample implementations of this? I’ve read that higher-order unification is involved, and that inference is undecidable without certain restrictions. Is that accurate? Would it be difficult to retrofit a (more or less) standard implementation of Hindley–Milner?

Seeking contributors to psyche-c

Dear guys,

I would like to announce an open-source tool that we are developing: psyche-c. It completes missing parts of C programs, so that you can have a fully compilable program. In other words, it does type inference and stub generation for missing functions. The tool has an online interface, which you can use:

For instance, if you feed it with this program, taken from Sedgewick's book:

void TCdfsR(Graph G, Edge e) {
link t;
G->tc[e.v][e.w] = 1;
for (t = G->adj[e.w]; t != NULL; t = t->next) if (G->tc[e.v][t->v] == 0)
TCdfsR(G, EDGE(e.v, t->v));

Then psyche-c will give you back these declarations:

typedef struct link {int v;struct link* next;}* link ;
typedef struct Graph {int** tc;struct link** adj;}* Graph ;
typedef struct Edge {int v;int w;} Edge ;
struct Edge EDGE (int,int) ;

Notice that is reconstructs recursive types that are pretty complicated. We have used psyche-c to reconstruct missing code in the GNU Core Util programs and in all the Sedgewick's examples (on graphs), for instance. Psyche-c is good for code completion, as a helper to debug programs, and even to reduce compilation time. It uses a unification based type-inference engine, and has a few tricks to parse C, even when missing declarations. If you would like to contribute, the code is available at



How to name the inverse functions of constructors

I am working on the design of a language (Albatross) which allows for static verification. It has a strong functional core. One of the most important types in a functional language is the inductive or algebraic type. One of the most prominent examples is a list. E.g. a list type in Albatross is declared as follows.

    (^) (head:A, tail:LIST[A])

It has the constructor [] to create an empty list and the constructor ^ to construct a new list by prefixing an already constructed list (tail) with a new element (head).

From a nonempty list we can extract the head and the tail with the following functions.

head(l:LIST[A]): A
         l as _ ^ _
        -> inspect
           case h ^ _ then

tail(l:LIST[A]): LIST[A]
         l as _ ^ _
        -> inspect
           case _ ^ t then

The functions head and tail reverse the effect of the constructor ^. I am looking for a name on how to describe these type of functions.

The most immediate ideas are _desctructors_ or _unconstructors_ which I don't find very appealing. A better name might be _inverse constructors_ which seem to precisely describe what they are, but sound a little bit clumsy.

Does anyone have a good idea on how to name these animals?

Some background information on why I need these type of functions:

Algebraic data types are a great tool, but they are not always the appropriate tool. E.g. in order to describe natural numbers their implementation is straighforward but awfully inefficient (this is one of the big problems when you want to extract source code from Coq). There are two ways to describe natural numbers with an efficient implementation. Either as machine numbers with modulo arithmetic or as arbitrary sized numbers where the components are machine numbers.

Machine numbers are not objects of algebraic type. But they are similar. The have constructors (zero and successor) and an induction law. Furthermore they have discriminator functions (n = 0) to decide how the number has been constructed and an inverse constructor (predecessor).

As soon as a type has an induction law (which implicitely defines the constructor functions), discriminator functions and inverse constructors the compiler can treat these types like inductive types in order to define recursive functions (which are guaranteed to terminate), do pattern matching etc. The discriminator functions and inverse constructors are necessary for the compiler in order to be able to compile pattern matching expressions into executable code.

In my opinion these pseudo algebraic/inductive types will be a great tool. Therefore I need good notions and names to express properties well.

Thanks for any help.

Language Description

Best value for overloading?

There exist various approaches to overloading, including:

* type classes of various kinds
* traits
* implicits [2]
* multimethods
* other systems [1,3]

What seems to offer the best value for investment effort, expressiveness, and type safety?

For instance, multimethods are pretty flexible and uniformally allow a form of type-based and case-based overloading, but it seems quite difficult to capture accurate types with all the expressiveness we expect of ML functions, eg. first-class functions require intersection types and subtyping.

Type classes and traits seem more or less equivalent, but have problems with overlapping and named instances, a problem shared by [1] I believe. Implicits seem promising, and properly handle named and overlapping instances.

[1] A Second Look at Overloading
[2] The Implicit Calculus: A New Foundation for Generic Programming
[3] A Theory of Overloading

List of POPL 2017 papers with crowd-sourced preprint links has a list of POPL 2017 papers with crowd-sourced links to the preprints. The deadline for camera-ready version (a version provided by the researchers that takes reviewers' comment into account) is only on November 7th, so one should expect more preprints to be available after that.

Feel free to mention any paper that catches your interest. If you are very curious in a particular work that does not have an online preprint, sending an email to the authors to ask them whether they plan to have a preprint accessible online can help a lot.

XML feed