Dear viewer, these subtitles were generated by a machine via the service Trint and therefore are (very) buggy. If you are capable, please help us to create good quality subtitles: https://c3subtitles.de/talk/548 Thanks!
Nicola Pooya,
who happened to be used
to be a postdoc researcher at the same
university.
I'm going to add it to university in
Copenhagen. So I'm really, really
thrilled about Nicola being here.
Nicola used to work for the domestic
project ITU, which
was a research project towards developing
electronic election technology
in the past.
Nicola was a PhD student
in the gallium research team at India
Party.
OK, I'm going to butcher this or work
on cool.
I'm cool
with focus on designing programing
languages and in particular
metaprogramming.
Today, Nicola will be
presenting and giving us a presentation
on the experimental language link
created in collaboration with researchers
from its university, Copenhagen
and the University of Chicago.
Math tremors.
So Miss French
was not my main language.
Please help me to welcome Nicola
Pooya.
Thank you very much.
I'm really happy to be
here today to
introduce this this new programing
language that I've been working
on the last
few months, but that comes from
research done earlier to
Premi.
Language design is something deep to my
heart, hurt heard.
We really need better programing
languages.
And here I'm addressing
a case where functional programing
certainly type the case where
it's not enough, the case where
this high level view and
Motlow view is lacking the precise
resource management.
So let's try to combine this
so as an introduction, let's speak of
optimizations.
So what do we want about optimizations
of a program?
This could be a manually done by the
programmer, all done automatically
by the compiler. We want those
optimizations to be improving the
program for performances.
This is the first requirement, but
it's also at the same time, very
difficult to guarantee because
systems are so complex today that
you might be removing
some lines of code and still your
program is slower,
this kind of effects.
But anyway, at least there's optimization
should be safe. You should not turn
a correct program into an incorrect
program. We already have way
too much incorrect programs everywhere.
There is no need for the compilers to
all optimizations in general to
to make more of it.
It's better if this optimizations are
automatic and automatically done by the
compiler. Still,
if it's done automatically, we should
it should be predictable data programmer
when it applies and when it doesn't.
Let's take a genuine case of
optimizations.
Let's say that you have two parts in your
program, F,
F and G, and that
F is reading some input data and
producing some incoming data and that
G is reading back this intermediate
data to put you some upward data.
This is happening all the time in the
program and
in some cases, many cases,
maybe the
two programs could be
combined together, melds together.
We're going to call that fusion, going to
say that we Fuze EFG such
that it reads the input data
and writes the exact same output data,
but is not allocating any
of the data.
So it's not always possible.
But what is language will do
is that it will guarantee you that it
happens when you think it does.
So if you think it should
Fuze and it doesn't, you get the needle
by the compiler.
And what do you what you can do
is change F to make it
a better producer of the data.
I mean, it's going to be a bit clearer
later on.
Well, you can change G to make it a
better consumer or you can just decide
that this cannot be
optimized the way and that we are going
to look at this data.
OK, so the critical
areas in which this kind of optimizations
are required and actually done
by hand all the time by deprogrammers
is the following numerical computation.
All the embedded systems that are so few
resources available, drivers
and colonels, and something also
dear to my heart, security and
cryptography, where normally we
want the programs to be fast.
But we also need the program
to behave independently
on the on this and the
secret data to avoid
timing side channel and
so on.
So what do we have?
OK, so we have terms and
we're not going to speak too much about
them. They can provide a form
of media programing that I'm not going to
try to speak too much about.
But you can think of something much
better and CBP much better than templates
in C++.
But also they are going to be used for
data like just like this, integers
or doubles in operations on that.
What we are going to talk a lot about is
all those processes and the here to
describe the behavior, the
actions we do on data that is
reading and writing or
data types are
here to enforce the
safe use of data by
terms, namely, we don't
want to mix anent and a boolean or
an intent to narrate
what decisions
they are, the types for the processes,
and they are here to enforce that.
We get the behavior we wanted.
That is, if we say that we should return
and we should not be writing something
else on writing on it.
We have dividend wipes
and dividend decisions which are not
going to discuss here because
it's a it's a another big
topic, but it's crucial that this has
been sought out before in
the language because this enables formal
verification and convenient formal
verification.
Last but not least, we have
dual citizens, which enables
fusion, the optimization
I was mentioning about, and we're going
to see what it means.
OK, so where does this language come
from? I took inspiration from
many languages, from purely functional,
strongly typed languages such as high
school or theories such as Martinello
of type theory and calculus of
constriction.
Also fully develop
programing languages for proving such as
that and interest
all the process about inherits from
the pack elkies.
For which we might know better, L.A.
was inspired also from the pack
Pachelbel's and some extent
and also there's there's a there's
more precisely all the research
on Sishen types and the logic has been
inspiring for me in this
new line of work developed by
me and colleagues at EITE
in Copenhagen, in Charmeuse in Sweden.
OK, so.
This is bad.
OK, so this is supposed
to be a nice summation.
Let's it's not big of a problem.
There is only one there, so let's pick
an example with a matrix multiplication.
I'm going to tell you something.
Oh.
OK, anyway, so
we have two matrices, A and B,
and then we want to multiply.
And what what we what we
know is that in a.
This is really not yet.
Someone told me so anyway,
so that's that's not
a big deal, I think.
So we have a room for
each room of A and each Kullen
of B, we are going to
two zip.
There's two there's two vectors
that which are of the same size to
produce a single
a single vector.
With the multiplication of dos and this
Victor, we are going to sum it up,
so the function of presentation
is to which we don't
really see here, but
anyway, so we are building
this vector that is the multiplication
of them and then sending it right away.
So we are building it for no good reason
for modularity.
It's nice way to express it
in that way.
OK, so at the end we should be able
to write this program
such that we think to
allocate this
in terms of depth and imagery, Victor,
but then it disappears.
OK, so here is the outline.
So.
We the first thing program, then we'll
talk more about types and the role as an
approximation tool, then we can
cover agility, allocation, fusion
and then back to this matrix
multiplication example.
OK.
So here is the first program,
it's called Devil and the Proc,
the keyword is marking the beginning
of a process.
Then we have we are declaring two
channels, A and B on
each and channels.
They have a station.
The station can be this question mark end
or back end.
Question mark means read and
bang means right.
So we must read
an end on a which we do
with this little arrow syntax.
We get the name X to what
we've read in a the Kuhnen
in the dot indicates the sequence
and then we do a write.
On me and we are writing X
plus X.
OK, the timing of this language
is ensuring that we are doing a
single read and a single right on those
channels. OK, now let's
make a new process that is feeding
twenty one as the input value.
So it's a new process that has a
single channel on which
we should write an on B
and now we allocate a channel A
on which we are going to write a twenty
one into A and then we can call
our double program defined previously
with A and B.
OK, notice now the equals
sign, it means that it's a definition,
therefore we can always replace
double by the definition.
So we get the following program where
we just placed in the the
double the definition of double.
So here we see the location,
the assignment, the right and
then the right.
Now it's a good case where Phusion
a Treville case where Phusion can apply
and it's going to replace
this allocation.
Right. Right.
And read by a single local definition
and this local definition that these are
really just at the level of
of the static
level. So they can be
and will be expanded away, which
gives us this final program, which is
just writing
42 directly into B.
OK, so with this simple program
we've seen already clear processes,
their channels, allocation, read
and write.
OK, let's speak about types and
type systems.
OK, so if you believe that type system,
I'm just here to reject program
some kind of a bad code, telling you that
you're perfectly fine program has to be
rejected or that you think that Java
C sharp of C++, what
we have as good examples of type systems
or finally, you might prefer dynamic
typing and say that unit
testing can successfully replace
a type system.
In all these cases, I would say to you,
you're wrong, or at least that you should
think again, OK?
Actually, I think a good type system
should be a positive thing.
It should explain you why and where
your program can or will fail
it. You also empower the compiler.
The compiler for optimization is exactly
the case that I'm describing with this
fusion thing.
It is critical that we have the right
types for this to happen.
And another example is
that sometimes you can make the type so
precise that it automates
the program, that is the type is so
precise that there is no need to write a
program anymore.
But here, let's let's remember
it is that a time is an approximation,
and this approximation is here in
particular to enable an abstraction.
So our end
is an approximation for
five and seven.
For instance, but
an integer that is odd would
be a more precise date or an integer
that is prime would be a more precise
type or an integer that is equal to
five would be an even more precise type.
So we could have a wide range
of of approximations
for this types.
As I say, the types are here for
the data and solutions are here
for the behavior.
So we will see what
this approximation means for the.
OK, let's let's take another
example, we have
a process, Detmold,
which is reading to input A
and B and writing two outputs
DNA.
So where is the division of energy
and is the modulus of
of A and B..
So we're going to try this
as a process and we'll see that processes
can be combined entirely and then
sequentially.
Moreover, we're going to give a type of
opposition to this process and we'll
see how this gives a way to have
a precise control on the interface.
Finally, remember
that all the time.
These channels must be used exactly
once.
OK, so this slide is a bit scary.
I've put actually six programs,
six versions of the programs at the same
time.
And five versions of the type
so that we can go through some
of them.
So the type is in green
there and this is the first program that
that does this read and write all in
sequence.
This one with this pipe there,
it's it's saying that we do this in Bali,
the tourists tourism dollar and then
the tourists and they
are all in sequence, but in different
order are some sequential,
some symbolism.
We can do many variations.
And all all of these
are accepted with this same type,
which says that we should return a read,
be right on the and right on
on that note, as this
braces, this tell you that you
have the choice of the processing order,
meaning that all of this are valid.
OK, now you can be more precise
about the kind of processes that you want
to write. For instance, if you
say that with the Square
Kohnen, you can enforce
that. These channels are used in order
from left to right.
Only this program remains valid.
This is making the life of the
one using your process much easier,
as we'll see later with
duality.
OK, you could say I want
all this channels to be used in parallel,
used independently, except
that it won't be actually useful for this
situation because we would have to
write the division in the Majilis
without adding access to the
to the inputs.
We can be slightly more
fine grained saying that we
use these brackets that mean indata.
To end this couldn't in this bracket,
couldn't we say in sequence to say we
want the breeds to be done in parallel
and then the rights to be done in it,
which gives this only this this middle
program is valid.
We can have variations
like that. So this was
what we should get from this is
at least remember this this there's
different choices. We have like any order
from left to right and all in it.
OK.
So now we've we've been thinking
of this channels a bit like if they were
if this was memory and this is exactly
my intent. But just for a moment, let's
think of it as a political if
I am writing an end, then
the other side should be ready
to receive an end.
So there is this duality and this
jollity will work also with this
with this kind of
array of strict or Topal types.
If if one side
is as the choice
of the order, then
the other side has absolutely no choice.
So the duel to the
if we have a session as the duel is going
to be written with a distilled it.
So if we send in the
duel is going to be receiving a.
Braises the duel is getting to the
races, that means any processing order,
the duel is going to be the most
possessing order that is completely
invalid.
And this is from left to right, and
the duel is still something from left to
right, but we have to Julys inside.
OK, so just a quick example to see how
this goes.
So we have
this this this pair of
an end and a pair
of a double and an end together with
this annotation that tells us that
what we should do with it, that is we
should write an end.
But we can do this now.
I'll do this later, because this is this
braises.
But at least we have to receive the
double and then received an input.
OK, so now let's see what the other
guy has to do in front of us.
So we put the tilde and then we work
through the definition that is the
Brace's become brackets, the
banks become the
question marks, the
end of our sequence stays in order
and the question marks becomes the
resulting thing is that the
opposite process must receive
an end independently from
writing this novel.
And in this order in particular,
it cannot read an end
and then send it back on this
one.
This would create a deadlock, this
language when used with this panel
and concurrency sitting
is deadlock free.
OK, allocation infusion,
so.
OK, so let's be let's
let's beat this general sitting
where we have to put
his effigy
and they are following something, Joe.
So it could be anything,
any station s and they happen to
be following as and the it
so this new syntax,
which as this square brackets,
which reminds you that
it must be used in Dallin
Falsies C and
D to be used in parallel and use
independently.
This is a case
where fusion is guaranteed
to be able to happen.
So in all these settings where you manage
to make the two parts of the program B
offered dual sition, then you're
guaranteed that you can remove this
allocation away.
Maybe you want the same thing, but you
don't want the parallelism
now.
So we have this other
syntax.
You again,
with the same gelati requirement,
but you can put the processes in
sequence.
This is slightly more
restrictive because you really
have to do all that has to be done
with C before D
at the same time, this enables
the real location, the location
that cannot be fuzed.
OK, so let's pick an example.
So we have to possesses FMG
and they they are
they both uses, they are both using
braces.
And here I am introducing a new
annotation.
This this carat 100, this
this is to show that we don't only have
tuples but arbitrary arrays.
So here this guy
is is going to write integers,
100 integers in some order
that we do not know.
Maybe it goes from left to right.
Let's say this other process wants
to read all of this one hundred
ends, but in potentially different
order.
And if we don't if we don't change FMG,
then we have no other choice than to have
some intermediate data
that is allocated.
Then we run f it to write
all of the locations in
the order it was, and she
is going to read all the integers
in order she wants.
So
this is a case where if you don't put the
log flag here, the new
will complain and say the compiler will
complain and say, OK, I confused
that.
So you have to acknowledge the fact that
this is going to be really allocated.
If you don't want that, you can change
if you can change, if
to say, OK, I actually can work
a bit more and and right.
There's 100 NS in Berlin.
If you can do that, then the whole thing
views or you might
want to change and say, actually
I could read them entirely fine
in this case, does reviews or other
changes to offend you.
OK, so we have allocation
so we can go back to matrix
multiplication.
So
I'm not going to get into the details of
this of this operations.
But what do we have to to
to get is that we can write a zip
function in and
then write it on a much more general
function that works not only for doubles
and not only for multiplication, but any
free times and any operation F
and in the very sugary version
of this language, we can write it as
short as this.
OK, the summation also
could be done just
for doubles and in addition,
but in functional programing, we tend
to prefer
right once and for all communicators
such as this for lift again
and skipping the the the
details.
But we can see that it's
using a temporary viable to accumulate
this this
results of which then
becomes the additional doubles.
So now we can
put together the zip function
and the Sende function and
we have this intermediary data
that is this victor in the middle
that I was mentioning.
Which are
the theory tells us that we can fix
it to way.
So effused version
here, menu refused version,
is this where
we see that this is this
is mixing the summation,
the summation with the zero
and the plus and the multiplication
in a single function?
So some kind of conclusion,
we get to combine precision and
which you're never going
to get and we get a cost free
abstraction, this particular
optimization, which is which is
quite general, it subsumes
various kinds of linings
and other fusion
of InterMune intermediary data.
It is predictable, safe
and automatic.
So this
this this language and the
two chain that goes with it is completely
open source.
And I
and I hope you will
have a look try, helped
contribute, feel
free to ask questions,
bodybags and so on.
Thank you.
Anybody with questions for Nicola,
please go to one of the four
microphones on the side.
OK, so we're starting with the microphone
over there.
Yes,
yes.
Is it possible to use this language, for
example, to synthesize logic or
asynchronous logic, maybe plotless logic?
And in a logic,
I'm not sure I get the question to use
it for what? Synthesizing logic to
actually do your computation in hardware?
To synthesize a logic, synthesize
logic, not logic, logic tickets.
Yeah, I mean, so this language
and the tool chain with it is really
new, right? So this is there
is still plenty of burg's, plenty of not
fully implemented features.
But the theory
can can clearly do this kind of things
and we can have a very
high level way of writing things
like that.
But I think the
the main domain to which it applies
is a situation where
performance is really critical.
So I don't know, maybe this is the
case, but otherwise maybe high school
is good enough.
OK, one question over here.
So I was wondering about
the different annotations you could do
in the function definition where you
could say, like in which order you want
to read it or if you want to read in
parallel or in Syria.
I was wondering, couldn't most of those
be deduced by the compiler anyway,
if you could do that or not, because
you specified the flow and it's a pure
function. So I was wondering if it's
not redundant to have six
different functions for different ways of
accessing data?
Yeah, so
as a as a first step
in type systems, it's always easier
to check that the types are right than
to try to guess and what we
say infer what are the right types.
So and
it's not always what you want, but it's
true that we can
we could infer quite
a lot of types actually the way
the the the type Chicca
works on processes is actually
Bottom-Up.
It starts from the leaves of your program
and and is growing up the type
and then checking up that it matches
your definition.
But it is actually quite important
to have a way to
not give the most precise time
to to have some leeway when you
defining a type to have something
slightly more proximities and then
you say, oh, I can use them in any order.
And then you say, yes, but I'm going to
say left, right, for
now.
Right. So, OK.
So can I have a process that
produces like one Intertrust
at a time and have them consumed by a
process that just takes one integer and
just read them all in serial?
Or do I have to define separate versions
of my consumer?
So maybe.
So one thing we cannot really do now
is to have a process
that will be parametric on the
kind of order processing
order we have.
But at the same time, we cannot rewrite
the code in a positive way.
So it's not necessarily
working.
OK, I'm sorry.
No dialogs, please ask more questions
on the other side.
One question over here.
Thanks for the talk. Very interesting
stuff. I was wondering and I listen to
this idea of
dataflow language pops in my head.
So it has been like a massive
periodization of data processing
being in your vision.
Kind of, yes.
So functional programing is already
dead dataflow in
many ways. The thing is that typically
functional programing sort of
it's a success in many ways, but
it fails at being precise enough
about when and how much
allocation is made.
And this is what I'm trying to fix here
so that you know that by default, maybe
you will use fusion most of the time
everywhere. And it just like gets
out of the way,
just like Gizzi would optimize
your functions.
But the cases where it fails instead of
just getting slow for no reason,
then you at least see precisely where
this issue appears in your program.
And so you can decide to choose between
allocating or changing a program.
So you know where there's issues.
So toolkit to actually make that
work eventually.
OK, one question over here.
This microphone in the blue jacket,
what does the
compiler produce needed for executables?
I mean, yeah, so it's
so so it's quite early, but
it's producing C-code,
for instance.
The does the C backhanders is
the only one I have.
So there is this little language.
There is some operations that stays in
the same language.
And the final one so far
is the C and it's not complete.
It's not nice, it's not
optimal, but it's it's
producing precise code that
is quite possible.
So it's not inconceivable to
bare metal called.
Yes. Something I've not mentioned is that
I've I've looked at the code and
that was work that was on the radio
badge. And I found one instance of matrix
multiplication. So I extracted the
matrix multiplication from
leading into C and put
on the on the on the device.
And you can we can actually change maybe
the camera to see the
wibble animation.
Can we change the current?
OK, there's one more question on
this side, please.
So you're saying that link has dependent
types.
Does this extend to linear types
as well? Can you quantify overprocessed,
for example?
Yeah. So let's make the distinction
between what can be done with the
type system. That is, what can I
check and then what can I
translate into C
or reliable code.
So what can I check is
indeed we have normal
dependent types but we have dependencies.
Incision's that means I can say
I'm receiving and
receiving an end X
and then if X is
below 10 then
I'm supposed to receive a boolean.
Otherwise I'm supposed to send something
else so we can have the protocol can
depend on actual data.
We can also look again in the checking,
send and receive possesses,
sessions, types, functions
and pretty much anything that
can have a type.
OK, we have time for one more question
from the Internet, is there a question
from the Internet?
The Internet is silent.
That's a rare thing.
OK, then we
go with you. You're the last one tonight.
Thank you.
When you thought about
implementing this language, did
you try to come up with
an implementation instead as
a library or
an extension to GHC
Eskow?
Is it possible?
No, it's without dependent types,
but there's a real good question.
So we don't.
So the dividend types
is is an addition.
Right. So so we could have this language
with other different types.
It would be interesting already
and would be easier to integrate into
Haskell, for instance, the
main the main issue
is that this is linearity in this
descending Alsatians.
It's really difficult to implement as an
embedded DSL.
So this could be a deeply
embedded DSL with quazi quotations,
for instance, in high school.
So this is, I guess, a future project.
Like to me, it seemed simpler
to just write a new language,
but I agree that that's
potentially a bigger project
would be to integrate it into
long ago address.
Thank you. OK, thank you.
Please, a round of applause
for the California.