All right, so welcome everybody.
I thought this was going to be tight for it.
20 minute talk.
I think we're going to have to squeeze it in and 15 to leave some room for questions.
So we aren't going to get going.
This is a concurrent logic programming.
This will be my exploration of many cameras in the language called
Lang, specifically PCN.
And I'll explain what that means.
And I hope to get to the point where I can actually demo some of that for you.
We'll see.
My name is Stuart Dost.
There's my get-up handle if you want.
Last 10 years have been writing goal line professionally for the eBay,
then at Norfolk, in Amsterdam, then at Sweden,
respectively in Stockholm.
And as a hobby, I write prologue.
And for the last couple of years,
it'd be more and more enthusiastic about the list.
So mini-camera is basically the reason why.
For a talk that's not about prologue,
you're going to see a lot of prologue.
So how many people have actually seen prologue before?
And a little bit, there we go.
All right, nice.
Good.
I have to thank the people earlier.
I think it was Jonathan, and then before.
And Neil's.
I'd actually talk about prologue before.
And I have to thank a few people as well.
So Walter for introducing me to mini-camera in the first place.
Ronald Evans would recommend this devroom,
Peter Sachsen for our during the first draft of this talk,
and Felix Pinkleman for creating,
and answering all my questions, and I have seen.
I'll start with this quote by Will Bird.
It's been followed with mini-camera.
This is on his website mini-camera,
or comparing mini-camera and prologue.
There's the prologue then again.
And the quote is about parallelism.
So can we add some parallelization to the mini-camera?
And this just really caught my eye.
It's only gone by fascinating about the hat and no idea about.
And something that essentially nerds snipe me into a few years later
getting this talk.
So we'll do a few language introductions.
I'd like to talk about slang in order to do that.
I'm going to talk about micro-cannon
because I'm going to embed it in flank to show you what it can do.
And then in order to actually explain what the hell's going on,
I'm going to start with some prologue.
I hope that's okay.
So let's start with prologue.
It's a logic programming language.
It's declarative.
By default, most prologue contentages that for search,
search strategy, as a pure core.
And then there are a few mini-cannon implementations.
And in particular, the one from amendrix is an inspiration
for the way that I actually embed the micro-cannon in flank.
So here's a meta-interpreter in prologue.
And this is very minimal, I hope you agree.
But it's also useful.
We could also just say prove and then call which is a built-in.
And then there's nothing that more to be done.
But that one liner doesn't, that is actually hack on it.
So here we have a meta-interpreter where we can
and try and the behavior of prologue.
And then if we start to hack on this, we could switch it around.
So what we're seeing is, in order to prove something that's true,
there's no work to be done.
If I need to prove two things, then we're going to prove the first thing
and then the second thing.
And if I need to prove just a single thing,
I'm going to use this built-in from prologue
to give me matching rules that actually say something about the thing.
I need to prove, and then we're going to try the things that it tells me
that it needs to prove still.
And so what I'm introducing here is a few terms.
But I would like to focus on particular is that there's
this junction and conjunction on the screen.
So the conjunction here is that in order to prove two things,
we have to prove this and have to prove that.
And in order to prove anything, I have the choice of three
different rules to prove it.
And there's a disjunction between those three separate ways.
Any of which would match would give us a proof hopefully.
So this is very minimal, but it is useful.
There's some stuff there that we could tweak.
In particular, we have this depth first search strategy.
We could tweak to a breadth first search, for example.
And there's always targets for parallelization.
And this is the thing that I'm going to focus on more.
So if I need to prove this, I need to prove that.
I could try to prove both at the same time.
And if I prove, if I failed to prove, either one, I already know
that the whole thing is not going to work.
And the flip side in this junction, I could try and prove in three
different ways.
And if one returns a result, I know that I have a proof.
And so I could do all of this at the same time, hopefully.
And then the main difficulty is how to actually deal with any of those
giving notes.
Back in this different strategies for it.
The other part of the parallel goes unification.
That's not in this meta interpreter.
If I'd like to have access to that, I need some extension to it.
Skipping to microchannel, which is the most minimal version of
Canon languages that I know about.
It is more functional.
The semantics deal with substitutions, goals and streams,
which I'll get into a bit more.
There isn't any backtracking.
This is why the threats safety comment is there.
It's also logically pure.
An interesting thing that we're going to look at is it is able to deal with infinite answers.
Here's a full implementation of microchannel and skin.
The point is not to actually read this whole thing.
The point is to see that this is still fairly minimal.
But there's also actually unification in there.
There is disjunction and conjunction in the board.
And then there is some stuff over there that actually make that work.
Some of which involves monads.
Here are some examples of microchannel.
So this is going to be some list representation.
An empty state is here.
So a state takes two components.
There are substitutions, which are variable bindings.
And then there's a variable counter to say how many variables have we already introduced.
In the empty state, there are no variable bindings.
And we haven't introduced any variables.
Next we have a state that's full.
So this is going to be equivalent to saying something like x equals five.
So the variable zero is here, bound to the number five.
And then the counter is up by one because if we've introduced variable number zero.
Equal O is a goal.
So a goal in microchannel is a function that takes a state.
And it returns a stream of states.
So the state is going to return all the potential states that make that goal true.
And then applying that looks like this.
So if we want to actually run the goal to equal the variable x to the number five.
And we want to give it a previous state that's the empty state.
There's an old previous work done.
Then we have to actually introduce that x as a variable in scope.
And then apply the function to that state.
And if you would do this, that will return you exactly.
You can see some extra brackets here.
And this, but no, you like brackets.
So there's a stream of states, which includes only one state.
That's that we saw before x equaling five.
Because there's only exactly one state in which equal x five is true.
Given the empty state the previous state.
Okay.
So let's look at how dealing with infinite answers actually works.
This is going to be, for me, the interesting example,
between prologue and microcanon.
So here we have some prologue to start with.
We're going to declare a goal that says is something of five.
And it's going to be an infinite goal because it's recursive.
It's going to say this is true of x equals five.
But it's also true if and it just loops back around.
And so we can have an infinite way to prove that x is five.
And the answer, if we're going to ask about these.
And this five's goal is going to be an infinite stream of answers of five in prologue.
There's an infinite, infinite alternation of giving more answers that we still make this true.
We have sixes, which is equivalent.
And then we have five in sixes, which is saying x is either coming from the five stream,
or it's coming from the sixes goal, as you'd say in this case.
And if we ask about five in sixes, we're only going to get five.
So here's that for search from prologue because essentially it does deep into this recursion,
giving you infinite answers and never even looks at this one.
So this is a bit about how this junction then works in prologue.
It's only going to explore that part.
What we actually would want, or at least what I think we would like to see here,
is an alternation of five in sixes, right?
So it's going to be five or six in five in six, which is being infinite like that.
And there's another thing here that if I, first of all, let's see if I'm lying to you.
None of them, okay, good.
So I'm swapping around the goals here on the fives.
And what's happening here is that intuitively I'm doing the same thing, right?
It's either that or that.
And they should intuitively give you the exact same answer.
And prologue, what's happening if we dive deep into the recursion here in fives,
we're never even going to reach that x equals five.
So we're just going to run out of memory.
And again, intuitively I would just expect five, six alternating.
So here we have the equivalent in mini-canon.
So the syntax doesn't be different, but this semantic should be the same.
And we're defining five as a disjunction over that equal statement.
And then the recursive call, six is the same.
Five and six is again a disjunction over those two goals.
And if I run this asking five answers with an unbound variable x that I'm introducing there,
then I'm going to get this list as a result.
So this works.
And for the more if I swap around those two goals there,
there isn't any problem, we're still going to get the exact same result.
And then here if I introduce sevens we're going to get
still something weird.
So five, six, five, seven, five, six, five, seven.
When I would expect five, six, seven, five, six, seven.
So there's some weirdness there.
We're going to speed up even further and I'm going very fast.
But this is how that's actually happening in microcanon.
So there's a few different things.
Streams can be delayed, which is basically putting a thunk around the goal.
So that we notify to the evaluation.
This is something to wait on, please pass priority to any other
good streams that you might have to give results from.
And so we have a macro for that called D.
And then binary trampoline is the principle that we use to actually do this
switching around based on this signifier.
Now if you've done go for a while at some point and we're talking about
streams and delays and swapping stuff around from different sources,
you're thinking channels.
And Walther has actually done some exploration of that for interested.
Does the only previous answer I know to the quote that we saw from
Will earlier looking at some parallelization of microcanon.
But there's trouble, right?
So if we just get around the monsters for example from all these streams,
which ever finishes first for if we do this, then we're going to
lose order.
So there's a bunch of things that you need to think about
and try to make.
Now flang.
So what is flang, flang is a concurrent logic programming language
that I found a couple of months ago on hacker news, looked into it,
and thought this is a great match for what I've been trying to do for a while.
Because I'm mocked about whether they go implementation of
mini-canon to do this, but I never really could figure it out.
So a concurrent programming language in particular, it uses
guarded horned pauses, which I'll show you.
It's committed choice, which means that we only ever choose one of those
these junctions and never backtrack.
It's a very low level implementation or it's a very low level language
and I have multiple high level languages which all compile to it.
And then the really interesting part is that it uses delay on variables.
So skipping up yet again for speeding up, if you'd say,
here is a very pro-local language, this is called FGHC,
which stands for hardcore pauses.
What this does is we'll have a producer and a consumer stream,
and I'm going to have a producer that's producing 10 different items.
And only by defining the stream is the other one going to unblock.
So basically we have two blocking processes because in main these things
run immediately in parallel.
And then the producer is going to define.
So you see out here is that stream, it's going to define that stream.
And as soon as this variable is defined, this thing will, sorry,
the consumer will no longer block.
So the consumer there is basically saying there's a disjunction here between things.
And as long as they are not defined, the milk will actually execute.
As soon as they are defined, you can see this pattern will match.
That's the moment it will actually do anything.
And then here is an equivalent notation in PCM.
So this is a more imperative notation that's exactly the same kind of program.
And this will write 10 to 0 in order as an output.
So skip over that completely.
What are they going to end up doing?
And you're going to have to find me in the hallway afterwards,
actually see the code, I think, as I'm running out of time again.
But immature streams, we're using unblock logic variables.
So instead of putting a funk around the goal and say, as soon as I actually want more answers out of this stream,
I'm going to evaluate that function.
Instead, what we're going to do is we're going to define the full output as a stream.
And then anytime I want more answers out of that stream,
I'm going to say that the head of that stream is now defined as a variable.
And at that moment, the resolution principle will actually just try and find more answers
and fill them in and give them back to me.
So we're using two logic variables to do that.
We're generalizing the binary trampolineing in the disjunction.
And then there is some or parallelism going on.
What I chose to do is to take one answer from each goal in a disjunction,
put them in a buffer and then as soon as someone actually wants to get more answers out.
That's the moment that you get them from the buffer.
So that we actually have some work, let's see.
I'm trying to figure out the same time that it makes sense to show you some of that in one minute sure.
And let's see.
What did I have?
So here is a run.
I should make this a little bigger.
There we go.
So here's me saying I want to have nine answers out of a disjunction over five six and sevens.
And then if we try and do that,
we get this five six seven list out.
And then here.
So here's that equals.
The only goal that actually doesn't work assigning variables.
And to mimic some heavy goals that you might actually want to parallelize,
I'm adding a sleep statement here.
So this will take a while.
And then the thing to show is that if you put this as a.
So Conron is included in the thank you.
Yeah.
Thank you.
Thanks for.
So what's happening here is this is taking three seconds instead of because we have a nine variable assignments here.
And why three?
Because it's taking basically from every infinite stream.
It's taking one answer in that disjunction.
And then buffering them up.
There's actually tell the program that I want more answers out of this stream.
It's going to give me one by one.
I'll reach over here.
Next speaker.
Yeah.
You can set up.
Yes.
All right.
Questions.
Thank you.
Why do you want to preserve the order?
You.
It's a good question.
So you could decide that you don't.
Yeah.
Very good question.
Oh yes.
So the question is why do you care about the order?
And the answer is you could decide multi.
So I decided that that would be interesting and see what you have to change.
If you don't, so you could imagine that you have a disjunction over these three different streams that give you infinite five six and sevens.
And just whenever one is ready, you take one out.
That would be a simpler implementation as well.
So I decided to see what would need to be added if you did want to have the order in.
And there's various things you could do.
This buffer that I chose.
This is, I think, one of those.
Perfect fairness.
Yeah.
Exactly.
That's what it was after there.
Yeah.
Yep.