WEBVTT

00:00.000 --> 00:12.000
All right, so welcome everybody.

00:12.000 --> 00:15.000
I thought this was going to be tight for it.

00:15.000 --> 00:16.000
20 minute talk.

00:16.000 --> 00:19.000
I think we're going to have to squeeze it in and 15 to leave some room for questions.

00:19.000 --> 00:21.000
So we aren't going to get going.

00:21.000 --> 00:23.000
This is a concurrent logic programming.

00:23.000 --> 00:27.000
This will be my exploration of many cameras in the language called

00:27.000 --> 00:29.000
Lang, specifically PCN.

00:29.000 --> 00:31.000
And I'll explain what that means.

00:31.000 --> 00:34.000
And I hope to get to the point where I can actually demo some of that for you.

00:34.000 --> 00:35.000
We'll see.

00:35.000 --> 00:37.000
My name is Stuart Dost.

00:37.000 --> 00:39.000
There's my get-up handle if you want.

00:39.000 --> 00:42.000
Last 10 years have been writing goal line professionally for the eBay,

00:42.000 --> 00:45.000
then at Norfolk, in Amsterdam, then at Sweden,

00:45.000 --> 00:47.000
respectively in Stockholm.

00:47.000 --> 00:50.000
And as a hobby, I write prologue.

00:50.000 --> 00:52.000
And for the last couple of years,

00:52.000 --> 00:54.000
it'd be more and more enthusiastic about the list.

00:54.000 --> 00:58.000
So mini-camera is basically the reason why.

00:58.000 --> 01:00.000
For a talk that's not about prologue,

01:00.000 --> 01:02.000
you're going to see a lot of prologue.

01:02.000 --> 01:04.000
So how many people have actually seen prologue before?

01:04.000 --> 01:06.000
And a little bit, there we go.

01:06.000 --> 01:07.000
All right, nice.

01:07.000 --> 01:08.000
Good.

01:08.000 --> 01:10.000
I have to thank the people earlier.

01:10.000 --> 01:12.000
I think it was Jonathan, and then before.

01:12.000 --> 01:13.000
And Neil's.

01:13.000 --> 01:15.000
I'd actually talk about prologue before.

01:15.000 --> 01:17.000
And I have to thank a few people as well.

01:17.000 --> 01:20.000
So Walter for introducing me to mini-camera in the first place.

01:20.000 --> 01:22.000
Ronald Evans would recommend this devroom,

01:22.000 --> 01:25.000
Peter Sachsen for our during the first draft of this talk,

01:25.000 --> 01:27.000
and Felix Pinkleman for creating,

01:27.000 --> 01:30.000
and answering all my questions, and I have seen.

01:30.000 --> 01:32.000
I'll start with this quote by Will Bird.

01:32.000 --> 01:34.000
It's been followed with mini-camera.

01:34.000 --> 01:36.000
This is on his website mini-camera,

01:36.000 --> 01:39.000
or comparing mini-camera and prologue.

01:39.000 --> 01:41.000
There's the prologue then again.

01:41.000 --> 01:43.000
And the quote is about parallelism.

01:43.000 --> 01:47.000
So can we add some parallelization to the mini-camera?

01:47.000 --> 01:49.000
And this just really caught my eye.

01:49.000 --> 01:52.000
It's only gone by fascinating about the hat and no idea about.

01:52.000 --> 01:57.000
And something that essentially nerds snipe me into a few years later

01:57.000 --> 01:59.000
getting this talk.

01:59.000 --> 02:02.000
So we'll do a few language introductions.

02:02.000 --> 02:05.000
I'd like to talk about slang in order to do that.

02:05.000 --> 02:07.000
I'm going to talk about micro-cannon

02:07.000 --> 02:10.000
because I'm going to embed it in flank to show you what it can do.

02:10.000 --> 02:12.000
And then in order to actually explain what the hell's going on,

02:12.000 --> 02:14.000
I'm going to start with some prologue.

02:14.000 --> 02:16.000
I hope that's okay.

02:16.000 --> 02:17.000
So let's start with prologue.

02:17.000 --> 02:19.000
It's a logic programming language.

02:19.000 --> 02:20.000
It's declarative.

02:20.000 --> 02:24.000
By default, most prologue contentages that for search,

02:24.000 --> 02:27.000
search strategy, as a pure core.

02:27.000 --> 02:30.000
And then there are a few mini-cannon implementations.

02:30.000 --> 02:34.000
And in particular, the one from amendrix is an inspiration

02:34.000 --> 02:39.000
for the way that I actually embed the micro-cannon in flank.

02:39.000 --> 02:43.000
So here's a meta-interpreter in prologue.

02:43.000 --> 02:46.000
And this is very minimal, I hope you agree.

02:46.000 --> 02:47.000
But it's also useful.

02:47.000 --> 02:50.000
We could also just say prove and then call which is a built-in.

02:50.000 --> 02:52.000
And then there's nothing that more to be done.

02:52.000 --> 02:54.000
But that one liner doesn't, that is actually hack on it.

02:54.000 --> 02:58.000
So here we have a meta-interpreter where we can

02:58.000 --> 03:01.000
and try and the behavior of prologue.

03:01.000 --> 03:04.000
And then if we start to hack on this, we could switch it around.

03:04.000 --> 03:07.000
So what we're seeing is, in order to prove something that's true,

03:07.000 --> 03:09.000
there's no work to be done.

03:09.000 --> 03:12.000
If I need to prove two things, then we're going to prove the first thing

03:12.000 --> 03:13.000
and then the second thing.

03:13.000 --> 03:15.000
And if I need to prove just a single thing,

03:15.000 --> 03:17.000
I'm going to use this built-in from prologue

03:17.000 --> 03:20.000
to give me matching rules that actually say something about the thing.

03:20.000 --> 03:23.000
I need to prove, and then we're going to try the things that it tells me

03:23.000 --> 03:25.000
that it needs to prove still.

03:25.000 --> 03:31.000
And so what I'm introducing here is a few terms.

03:31.000 --> 03:34.000
But I would like to focus on particular is that there's

03:34.000 --> 03:37.000
this junction and conjunction on the screen.

03:37.000 --> 03:41.000
So the conjunction here is that in order to prove two things,

03:41.000 --> 03:44.000
we have to prove this and have to prove that.

03:44.000 --> 03:48.000
And in order to prove anything, I have the choice of three

03:48.000 --> 03:51.000
different rules to prove it.

03:51.000 --> 03:54.000
And there's a disjunction between those three separate ways.

03:54.000 --> 03:59.000
Any of which would match would give us a proof hopefully.

03:59.000 --> 04:02.000
So this is very minimal, but it is useful.

04:02.000 --> 04:04.000
There's some stuff there that we could tweak.

04:04.000 --> 04:07.000
In particular, we have this depth first search strategy.

04:07.000 --> 04:10.000
We could tweak to a breadth first search, for example.

04:10.000 --> 04:12.000
And there's always targets for parallelization.

04:12.000 --> 04:15.000
And this is the thing that I'm going to focus on more.

04:15.000 --> 04:18.000
So if I need to prove this, I need to prove that.

04:18.000 --> 04:21.000
I could try to prove both at the same time.

04:21.000 --> 04:25.000
And if I prove, if I failed to prove, either one, I already know

04:25.000 --> 04:27.000
that the whole thing is not going to work.

04:27.000 --> 04:31.000
And the flip side in this junction, I could try and prove in three

04:31.000 --> 04:32.000
different ways.

04:32.000 --> 04:35.000
And if one returns a result, I know that I have a proof.

04:35.000 --> 04:38.000
And so I could do all of this at the same time, hopefully.

04:38.000 --> 04:42.000
And then the main difficulty is how to actually deal with any of those

04:42.000 --> 04:43.000
giving notes.

04:43.000 --> 04:45.000
Back in this different strategies for it.

04:45.000 --> 04:48.000
The other part of the parallel goes unification.

04:48.000 --> 04:50.000
That's not in this meta interpreter.

04:50.000 --> 04:55.000
If I'd like to have access to that, I need some extension to it.

04:55.000 --> 04:58.000
Skipping to microchannel, which is the most minimal version of

04:58.000 --> 05:01.000
Canon languages that I know about.

05:01.000 --> 05:03.000
It is more functional.

05:03.000 --> 05:07.000
The semantics deal with substitutions, goals and streams,

05:07.000 --> 05:08.000
which I'll get into a bit more.

05:08.000 --> 05:11.000
There isn't any backtracking.

05:11.000 --> 05:15.000
This is why the threats safety comment is there.

05:15.000 --> 05:17.000
It's also logically pure.

05:17.000 --> 05:22.000
An interesting thing that we're going to look at is it is able to deal with infinite answers.

05:22.000 --> 05:26.000
Here's a full implementation of microchannel and skin.

05:26.000 --> 05:28.000
The point is not to actually read this whole thing.

05:28.000 --> 05:31.000
The point is to see that this is still fairly minimal.

05:31.000 --> 05:34.000
But there's also actually unification in there.

05:34.000 --> 05:36.000
There is disjunction and conjunction in the board.

05:36.000 --> 05:39.000
And then there is some stuff over there that actually make that work.

05:39.000 --> 05:44.000
Some of which involves monads.

05:44.000 --> 05:48.000
Here are some examples of microchannel.

05:48.000 --> 05:52.000
So this is going to be some list representation.

05:52.000 --> 05:54.000
An empty state is here.

05:54.000 --> 05:56.000
So a state takes two components.

05:56.000 --> 05:59.000
There are substitutions, which are variable bindings.

05:59.000 --> 06:02.000
And then there's a variable counter to say how many variables have we already introduced.

06:02.000 --> 06:05.000
In the empty state, there are no variable bindings.

06:05.000 --> 06:08.000
And we haven't introduced any variables.

06:08.000 --> 06:10.000
Next we have a state that's full.

06:10.000 --> 06:14.000
So this is going to be equivalent to saying something like x equals five.

06:14.000 --> 06:18.000
So the variable zero is here, bound to the number five.

06:18.000 --> 06:23.000
And then the counter is up by one because if we've introduced variable number zero.

06:23.000 --> 06:26.000
Equal O is a goal.

06:26.000 --> 06:30.000
So a goal in microchannel is a function that takes a state.

06:30.000 --> 06:32.000
And it returns a stream of states.

06:32.000 --> 06:38.000
So the state is going to return all the potential states that make that goal true.

06:38.000 --> 06:40.000
And then applying that looks like this.

06:40.000 --> 06:46.000
So if we want to actually run the goal to equal the variable x to the number five.

06:46.000 --> 06:50.000
And we want to give it a previous state that's the empty state.

06:50.000 --> 06:52.000
There's an old previous work done.

06:52.000 --> 06:56.000
Then we have to actually introduce that x as a variable in scope.

06:56.000 --> 06:58.000
And then apply the function to that state.

06:58.000 --> 07:01.000
And if you would do this, that will return you exactly.

07:01.000 --> 07:03.000
You can see some extra brackets here.

07:03.000 --> 07:05.000
And this, but no, you like brackets.

07:05.000 --> 07:10.000
So there's a stream of states, which includes only one state.

07:10.000 --> 07:13.000
That's that we saw before x equaling five.

07:13.000 --> 07:17.000
Because there's only exactly one state in which equal x five is true.

07:17.000 --> 07:21.000
Given the empty state the previous state.

07:21.000 --> 07:23.000
Okay.

07:23.000 --> 07:27.000
So let's look at how dealing with infinite answers actually works.

07:27.000 --> 07:30.000
This is going to be, for me, the interesting example,

07:30.000 --> 07:32.000
between prologue and microcanon.

07:32.000 --> 07:35.000
So here we have some prologue to start with.

07:35.000 --> 07:40.000
We're going to declare a goal that says is something of five.

07:40.000 --> 07:43.000
And it's going to be an infinite goal because it's recursive.

07:43.000 --> 07:46.000
It's going to say this is true of x equals five.

07:46.000 --> 07:49.000
But it's also true if and it just loops back around.

07:49.000 --> 07:52.000
And so we can have an infinite way to prove that x is five.

07:52.000 --> 07:56.000
And the answer, if we're going to ask about these.

07:56.000 --> 08:01.000
And this five's goal is going to be an infinite stream of answers of five in prologue.

08:01.000 --> 08:07.000
There's an infinite, infinite alternation of giving more answers that we still make this true.

08:07.000 --> 08:09.000
We have sixes, which is equivalent.

08:09.000 --> 08:14.000
And then we have five in sixes, which is saying x is either coming from the five stream,

08:14.000 --> 08:18.000
or it's coming from the sixes goal, as you'd say in this case.

08:18.000 --> 08:22.000
And if we ask about five in sixes, we're only going to get five.

08:22.000 --> 08:27.000
So here's that for search from prologue because essentially it does deep into this recursion,

08:27.000 --> 08:30.000
giving you infinite answers and never even looks at this one.

08:30.000 --> 08:34.000
So this is a bit about how this junction then works in prologue.

08:34.000 --> 08:36.000
It's only going to explore that part.

08:36.000 --> 08:40.000
What we actually would want, or at least what I think we would like to see here,

08:40.000 --> 08:43.000
is an alternation of five in sixes, right?

08:43.000 --> 08:47.000
So it's going to be five or six in five in six, which is being infinite like that.

08:47.000 --> 08:57.000
And there's another thing here that if I, first of all, let's see if I'm lying to you.

08:57.000 --> 08:59.000
None of them, okay, good.

08:59.000 --> 09:02.000
So I'm swapping around the goals here on the fives.

09:02.000 --> 09:07.000
And what's happening here is that intuitively I'm doing the same thing, right?

09:07.000 --> 09:09.000
It's either that or that.

09:09.000 --> 09:13.000
And they should intuitively give you the exact same answer.

09:13.000 --> 09:17.000
And prologue, what's happening if we dive deep into the recursion here in fives,

09:17.000 --> 09:19.000
we're never even going to reach that x equals five.

09:19.000 --> 09:22.000
So we're just going to run out of memory.

09:22.000 --> 09:27.000
And again, intuitively I would just expect five, six alternating.

09:27.000 --> 09:31.000
So here we have the equivalent in mini-canon.

09:31.000 --> 09:36.000
So the syntax doesn't be different, but this semantic should be the same.

09:36.000 --> 09:40.000
And we're defining five as a disjunction over that equal statement.

09:40.000 --> 09:43.000
And then the recursive call, six is the same.

09:43.000 --> 09:46.000
Five and six is again a disjunction over those two goals.

09:46.000 --> 09:52.000
And if I run this asking five answers with an unbound variable x that I'm introducing there,

09:52.000 --> 09:56.000
then I'm going to get this list as a result.

09:56.000 --> 09:58.000
So this works.

09:58.000 --> 10:02.000
And for the more if I swap around those two goals there,

10:02.000 --> 10:06.000
there isn't any problem, we're still going to get the exact same result.

10:06.000 --> 10:11.000
And then here if I introduce sevens we're going to get

10:11.000 --> 10:13.000
still something weird.

10:13.000 --> 10:15.000
So five, six, five, seven, five, six, five, seven.

10:15.000 --> 10:18.000
When I would expect five, six, seven, five, six, seven.

10:18.000 --> 10:20.000
So there's some weirdness there.

10:20.000 --> 10:23.000
We're going to speed up even further and I'm going very fast.

10:23.000 --> 10:28.000
But this is how that's actually happening in microcanon.

10:28.000 --> 10:30.000
So there's a few different things.

10:30.000 --> 10:35.000
Streams can be delayed, which is basically putting a thunk around the goal.

10:35.000 --> 10:37.000
So that we notify to the evaluation.

10:37.000 --> 10:40.000
This is something to wait on, please pass priority to any other

10:40.000 --> 10:44.000
good streams that you might have to give results from.

10:44.000 --> 10:47.000
And so we have a macro for that called D.

10:47.000 --> 10:52.000
And then binary trampoline is the principle that we use to actually do this

10:52.000 --> 10:55.000
switching around based on this signifier.

10:55.000 --> 10:58.000
Now if you've done go for a while at some point and we're talking about

10:58.000 --> 11:02.000
streams and delays and swapping stuff around from different sources,

11:02.000 --> 11:04.000
you're thinking channels.

11:04.000 --> 11:08.000
And Walther has actually done some exploration of that for interested.

11:08.000 --> 11:13.000
Does the only previous answer I know to the quote that we saw from

11:13.000 --> 11:17.000
Will earlier looking at some parallelization of microcanon.

11:17.000 --> 11:19.000
But there's trouble, right?

11:19.000 --> 11:22.000
So if we just get around the monsters for example from all these streams,

11:22.000 --> 11:26.000
which ever finishes first for if we do this, then we're going to

11:26.000 --> 11:27.000
lose order.

11:27.000 --> 11:29.000
So there's a bunch of things that you need to think about

11:29.000 --> 11:31.000
and try to make.

11:31.000 --> 11:32.000
Now flang.

11:32.000 --> 11:36.000
So what is flang, flang is a concurrent logic programming language

11:36.000 --> 11:40.000
that I found a couple of months ago on hacker news, looked into it,

11:40.000 --> 11:43.000
and thought this is a great match for what I've been trying to do for a while.

11:43.000 --> 11:45.000
Because I'm mocked about whether they go implementation of

11:45.000 --> 11:48.000
mini-canon to do this, but I never really could figure it out.

11:48.000 --> 11:52.000
So a concurrent programming language in particular, it uses

11:52.000 --> 11:55.000
guarded horned pauses, which I'll show you.

11:55.000 --> 11:59.000
It's committed choice, which means that we only ever choose one of those

11:59.000 --> 12:02.000
these junctions and never backtrack.

12:02.000 --> 12:07.000
It's a very low level implementation or it's a very low level language

12:07.000 --> 12:11.000
and I have multiple high level languages which all compile to it.

12:11.000 --> 12:17.000
And then the really interesting part is that it uses delay on variables.

12:17.000 --> 12:22.000
So skipping up yet again for speeding up, if you'd say,

12:22.000 --> 12:27.000
here is a very pro-local language, this is called FGHC,

12:27.000 --> 12:30.000
which stands for hardcore pauses.

12:30.000 --> 12:35.000
What this does is we'll have a producer and a consumer stream,

12:35.000 --> 12:39.000
and I'm going to have a producer that's producing 10 different items.

12:39.000 --> 12:44.000
And only by defining the stream is the other one going to unblock.

12:44.000 --> 12:47.000
So basically we have two blocking processes because in main these things

12:47.000 --> 12:50.000
run immediately in parallel.

12:50.000 --> 12:52.000
And then the producer is going to define.

12:52.000 --> 12:55.000
So you see out here is that stream, it's going to define that stream.

12:55.000 --> 12:59.000
And as soon as this variable is defined, this thing will, sorry,

12:59.000 --> 13:01.000
the consumer will no longer block.

13:01.000 --> 13:05.000
So the consumer there is basically saying there's a disjunction here between things.

13:05.000 --> 13:08.000
And as long as they are not defined, the milk will actually execute.

13:08.000 --> 13:12.000
As soon as they are defined, you can see this pattern will match.

13:12.000 --> 13:15.000
That's the moment it will actually do anything.

13:15.000 --> 13:20.000
And then here is an equivalent notation in PCM.

13:21.000 --> 13:27.000
So this is a more imperative notation that's exactly the same kind of program.

13:27.000 --> 13:32.000
And this will write 10 to 0 in order as an output.

13:32.000 --> 13:35.000
So skip over that completely.

13:35.000 --> 13:37.000
What are they going to end up doing?

13:37.000 --> 13:39.000
And you're going to have to find me in the hallway afterwards,

13:39.000 --> 13:42.000
actually see the code, I think, as I'm running out of time again.

13:42.000 --> 13:48.000
But immature streams, we're using unblock logic variables.

13:48.000 --> 13:53.000
So instead of putting a funk around the goal and say, as soon as I actually want more answers out of this stream,

13:53.000 --> 13:55.000
I'm going to evaluate that function.

13:55.000 --> 13:59.000
Instead, what we're going to do is we're going to define the full output as a stream.

13:59.000 --> 14:02.000
And then anytime I want more answers out of that stream,

14:02.000 --> 14:06.000
I'm going to say that the head of that stream is now defined as a variable.

14:06.000 --> 14:11.000
And at that moment, the resolution principle will actually just try and find more answers

14:11.000 --> 14:14.000
and fill them in and give them back to me.

14:15.000 --> 14:18.000
So we're using two logic variables to do that.

14:18.000 --> 14:25.000
We're generalizing the binary trampolineing in the disjunction.

14:25.000 --> 14:28.000
And then there is some or parallelism going on.

14:28.000 --> 14:34.000
What I chose to do is to take one answer from each goal in a disjunction,

14:34.000 --> 14:38.000
put them in a buffer and then as soon as someone actually wants to get more answers out.

14:38.000 --> 14:41.000
That's the moment that you get them from the buffer.

14:41.000 --> 14:46.000
So that we actually have some work, let's see.

14:46.000 --> 14:56.000
I'm trying to figure out the same time that it makes sense to show you some of that in one minute sure.

14:56.000 --> 15:00.000
And let's see.

15:00.000 --> 15:02.000
What did I have?

15:02.000 --> 15:06.000
So here is a run.

15:06.000 --> 15:11.000
I should make this a little bigger.

15:11.000 --> 15:12.000
There we go.

15:12.000 --> 15:19.000
So here's me saying I want to have nine answers out of a disjunction over five six and sevens.

15:19.000 --> 15:25.000
And then if we try and do that,

15:25.000 --> 15:29.000
we get this five six seven list out.

15:29.000 --> 15:37.000
And then here.

15:37.000 --> 15:39.000
So here's that equals.

15:39.000 --> 15:43.000
The only goal that actually doesn't work assigning variables.

15:43.000 --> 15:48.000
And to mimic some heavy goals that you might actually want to parallelize,

15:48.000 --> 15:51.000
I'm adding a sleep statement here.

15:51.000 --> 15:54.000
So this will take a while.

15:54.000 --> 16:00.000
And then the thing to show is that if you put this as a.

16:00.000 --> 16:04.000
So Conron is included in the thank you.

16:04.000 --> 16:05.000
Yeah.

16:05.000 --> 16:06.000
Thank you.

16:06.000 --> 16:07.000
Thanks for.

16:07.000 --> 16:13.000
So what's happening here is this is taking three seconds instead of because we have a nine variable assignments here.

16:13.000 --> 16:14.000
And why three?

16:14.000 --> 16:17.000
Because it's taking basically from every infinite stream.

16:17.000 --> 16:20.000
It's taking one answer in that disjunction.

16:20.000 --> 16:22.000
And then buffering them up.

16:22.000 --> 16:25.000
There's actually tell the program that I want more answers out of this stream.

16:25.000 --> 16:27.000
It's going to give me one by one.

16:27.000 --> 16:28.000
I'll reach over here.

16:28.000 --> 16:29.000
Next speaker.

16:29.000 --> 16:30.000
Yeah.

16:30.000 --> 16:31.000
You can set up.

16:31.000 --> 16:32.000
Yes.

16:32.000 --> 16:33.000
All right.

16:33.000 --> 16:34.000
Questions.

16:34.000 --> 16:36.000
Thank you.

16:36.000 --> 16:37.000
Thank you.

16:37.000 --> 16:38.000
Thank you.

16:38.000 --> 16:39.000
Thank you.

16:39.000 --> 16:40.000
Thank you.

16:40.000 --> 16:41.000
Thank you.

16:41.000 --> 16:47.000
Why do you want to preserve the order?

16:47.000 --> 16:48.000
You.

16:48.000 --> 16:49.000
It's a good question.

16:49.000 --> 16:50.000
So you could decide that you don't.

16:50.000 --> 16:51.000
Yeah.

16:51.000 --> 16:52.000
Very good question.

16:52.000 --> 16:53.000
Oh yes.

16:53.000 --> 16:55.000
So the question is why do you care about the order?

16:55.000 --> 16:57.000
And the answer is you could decide multi.

16:57.000 --> 17:00.000
So I decided that that would be interesting and see what you have to change.

17:00.000 --> 17:07.000
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.

17:07.000 --> 17:10.000
And just whenever one is ready, you take one out.

17:10.000 --> 17:13.000
That would be a simpler implementation as well.

17:13.000 --> 17:19.000
So I decided to see what would need to be added if you did want to have the order in.

17:19.000 --> 17:21.000
And there's various things you could do.

17:21.000 --> 17:22.000
This buffer that I chose.

17:22.000 --> 17:25.000
This is, I think, one of those.

17:25.000 --> 17:27.000
Perfect fairness.

17:27.000 --> 17:28.000
Yeah.

17:28.000 --> 17:29.000
Exactly.

17:29.000 --> 17:30.000
That's what it was after there.

17:30.000 --> 17:31.000
Yeah.

17:31.000 --> 17:32.000
Yep.