Hindley-Milner for chemlambda

 Some notes about Hindley-Milner in #chemlambda . It turns out that is pretty simple to do something very intuitive.

The starting point is the mol file which encodes a graph molecule.

Let me recall how this works.

The ingredients of a molecule are some nodes, which have ports. Nodes can be red, green, yellow or blue (until now, but you are free to add your own) and they appear as, say, 4px atoms with various colors.

Their ports are yellow if they are “in” ports and “blue” if they are out ports.

There is more.

Because the trivalent nodes (i.e. nodes with 3 ports) are always either with two “in” ports and 1 “out” port, or the other way (invert “in” with “out”) there is a need to differentiate the two “in” (or the two “out”) ports of a trivalent node, that is why one is at “left”, represented by a 2px atom.

So, for example, the application node appear as
A [ left.in , in, out]
and in the mol file is represented by a line which looks like this:
A 14 abc 3
where the first argument is “A” (application) and 14 is the value of the port left.in, abc is the value of the port in and 3 is the value of the port out.
A mol file is a list of such lines, which satisfies the condition that every port value appears at most twice, and if it appears twice then it has to be once in a in port and one in a out port.

That’s it.

Oh, maybe is good to say that the L (lambda) node has one in port and two out ports (and not two in ports and one out port!) and it appears as
L a b c
where a is “in”, b is “left.out” and c is “out”. For example if you want to write Lx.T then probably the L node will appear as

L a x y

and “a” will be a port value which appears as the out port value of “T”, whatever that means in your particular example.

Two colors are enough to distinguish the main nodes

• A green, two ports in one port out
• FO green, two ports out, one port in  (that’s a fanout node)
• L red, two ports out, one port in
• FI red, two ports in, one port out (that’s a fanin node)

When represented in the chemlambda gui, you don’t see any port variable, and they indeed not matter, their only scope is to represent an edge from a port in to a port out or a free in edge, or a free out edge.

Now, let’s go to types. In the previous post  I gave a link to

https://chorasimilarity.wordpress.com/2013/08/29/example-decorations-of-ski-combinators-in-simply-typed-graphic-lambda-calculus/

where is explained a simple procedure. Just take a graph (on graphic lambda calculus, therefore easily to translate into chemlambda) and give labels to all the edges, then use the “function” constructor -> and express relations between the edge labels according to the rules at each node. You get a magma, with the operation -> and generators the edge labels. If the magma is free then the term represented by the graph is well typed.

With the nodes FI and the FOE which are present in chemlambda, one has to use a FUN constructor, as previously, and a PAIR constructor.

The edge labels (which are type names, repeat: names, not types, so there is no problem related to polymorphism)  are of course, exactly the port variables from the mol file which represents the graph.

So the first thing to do is to translate the mol file into another file, line by line. Like this: use the same style and introduce the “type node”

FUN left.in in out

(which represents c=a->b like this: FUN a b c)

and the “type node”

PAIR left.in in out

(which represents c=(a,b) like this PAIR (a,b,c) )

Use also the FO node as previously.

Then translate

• A a b c  –>> FUN b c a
• L a b c  –>> FUN b a c
• FI a b c –>> PAIR b a c
• FOE a b c –>> PAIR b c a
• FO a b c –>> FO a b c

and delete all other nodes (like T, termination, or FRIN or FROUT)

The translation changes some properties of the ports, in the sense that some ports which were “in” become “out” ports, and conversely.

So what happens is that even if each port value appears at most twice in the new file, the following are possible for those values “a” which appear twice:

• if it appears once as a “in” and once as a “out”, do nothing more
• if it appears twice as a “in”, then delete the two occurrences and replace them by new names a1 and a2 and add “FO a a1 a2” to the file
• if it appears twice as a “out” then add a new 2 valent node, call it
  EQ left.in in , so add  “EQ a a”

EQ nodes represents relations between generators, the generators are  the port values.

By this simple procedure starting from the mol file, the rest consists only in giving the local moves for the new graphs obtained.

Which can be these local moves other than the translations of the old moves of chemlambda? That is the essence of the HM algorithm, as seen in chemlambda, of course. (Mind that in chemlambda may not stop, because chemlambda molecules are not representing lambda terms in general, even if any lambda term has a correspondent in chemlambda).

Lots of interesting things may happen, even if restricted to molecules which represent lambda terms. If the term has no normal form, of course the algorithm does not stop, for example.

Wait, what algorithm?

The algorithm has two ingredients:

• the moves, which are translations of the chemlambda moves (that’s pretty intriguing, that even if the translation is bad, i.e. non invertible, the translated moves are still good, in the sense that it does not happen that for the same left pattern there are two different right patterns proposed)
• and the reduction strategy which is left at your choice, from “stupid” (the one I’m currently using) to more intelligent artificial chemistry style or Actor Model ones, as described here.

The meaning of this is that one can imagine a whole lot of different HM kind of algorithms for (a limited) type inference, which can be as sequential or as concurrent as you want.

What could be the purpose of this HM like algorithm for chemlambda?

It is a mean to extract some very limited “objective” information from the molecule, even if in the process of reduction. Usually it will make no global sense (meaning that the algorithm will not stop, roughly) and moreover the algorithm will not be much less resources consuming than the reduction algorithm itself (which shows that already, theoretically, the chemlambda reduction algorithm, whichever variant of the reduction strategy you choose, should be very fast in it’s class).

I shall come back to this with lots of pictures and details, recurrently.
If you don’t make sense about what I’m talking about then go visit the chemlambda github repo and follow the links. https://github.com/chorasimilarity/chemlambda-gui