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/384 Thanks!
So thanks.
Yeah, my name is Rachel.
I'm one of the people who occasionally
hack on the compiler.
Yeah. And today I'm going to talk a
little bit about programing with the
types and address.
So this talk is for people who
don't really know what the dependent
types are and are curious about it.
If you know what cockies or ACDA, then
you will be probably bored.
So yeah, I can't help, but maybe
there is something new for you, who
knows.
So I will be talking about obviously
dependent types and a thing that's called
the Curry Howard correspondance.
One question is this large enough?
You know, OK, let's make the bigger
better.
OK, so
I think that's called the Currey our
correspondence, which is in my opinion, a
very powerful mental model to reason
about types as propositions.
So we'll introduce that and we'll talk a
little bit about constructive logic
and how we can model this
in the type system so we can have more
expressive types.
I'll do a little bit of life coding and
hopefully everything will work out right.
I don't know. Sometimes things fail, so
please don't laugh at me.
And in the end I will talk about effects
and typewriters. So it was just a purely
functional programing language.
Therefore, we have to have some
mechanism to deal with side effects,
stuff like IO, writing
to files, communicating with the outside
world, stuff like that.
And we reflect that and the type system.
And another thing is that
which is a pretty nice thing
is typewriters.
So we can do side effects on
the type level.
That might sound a little bit weird if
you are.
Yeah. Work with language like C++
or other ones.
Why should we have type system
effects on the type level?
But I hope I can convince you that this
is a pretty nice thing to have.
So what is it? Reciters is a purely
functional programing language that is
developed by Aaron Brady.
It's developed on GitHub and
so you can download the code, go crazy
with it. Simple request.
That's what I did. A lot of fun and
it's currently intended as a research
tool. So please don't use this in
production. I've seen people who
wanted to do that. I wanted to do that
too. But you will figure out pretty
quickly that you shouldn't do it.
Say it's a purely functional programing
language. If you're familiar with Haskell
or similar languages, it will
feel pretty much at home to you.
Of course, it's your to type.
This is this is why we're interested in
it. And the syntax is pretty close
to Haskell. So some minor
differences here. And there are,
of course, different semantics, but we're
not going to talk about that too much
here. And what I find
particularly appealing about the language
is that it's it focuses on
general purpose programing.
So if you've got a system like Sakurada,
it's more like a proof existence.
So you want to prove mathematical
theorems or theorems of actual software
and character, but you don't really
want to write a web server or
similar stuff and that that gets a little
bit hairy.
So this is actually one of
the major selling points of interest.
In fact these slides are written in
address, that computer JavaScript.
That's the project I've been working on
for a couple of years now.
So you can try it out and
write some JavaScript Web
applications or notes.
If you don't want to write pure
JavaScript, which is.
Yeah, don't want to.
So another thing that's pretty
interesting is its totality checking so
we can check if
an algorithm actually terminates.
Ah, that might sound a little weird as
well because halting problem.
But if we don't have things like general
recursion and just reduce
ourselves to use print of recursion,
then we can actually prove that an
algorithm terminates.
We also have interactive proving with
tactics. I'm not going to talk about
that, but it's there.
Obviously, we have a lot less tactics
than COK, which has an insane
amount of tactics.
So what's the motivation?
Why do we want more expressive
type systems? Because there are a lot of
very exciting type systems out there.
So I get to make the smaller but
only for this slight excuse me.
Cell types are
a very, very effective way to keep
our program behavior in check
so we can guarantee
that some things don't happen at runtime
when our type system is, well, checking
all these things so you can have a
function that you can guarantee
that this function only gets an integer
and not a string.
That's pretty much
the least thing a type system can do for
you, but it's something so
when you have a very powerful programing
language.
So this is not a risk. This is C++,
which has a very, very powerful type
system.
The template system by itself is too
incomplete. It's completely insane.
And so in this example, I'm
I'm just trying to model a
conditional branch, something if then
else on the type level might seem
a little bit contrived, but we'll get to
an example where this is.
A useful thing to do,
so you and see
if then else is a pretty simple thing,
but just to have it on the type level,
we got to write this weird code
over there.
And that leads to a very interesting
observation that when you are programing
in a static type programing language,
you're usually working in two different
languages.
So you're working and the value language
that you programed most of the
time. And so you write all your programs
on the value level and you've got the
type level language that is used
to program on your type level.
And that's a completely different
language. You have to learn two
languages. You get two for the price of
one, which is not very good because
you have to duplicate a lot of stuff
that you want to reuse on the type level
like this branch.
So we want to unify that.
We just want to work with terms.
And that is something where dependent
types are quite handy, especially IDers.
So what are dependent types?
This is a little bit of a watered down
view of what types are.
This is not like the full blown whatever
lambda cube, yada yada yada stuff.
So this is just very, very simple.
If you want to know the whole story, read
up on the Lamba Cube on stuff like sorts
and kinds.
But I just want to give you a basic
idea of what this is.
And first of all, we got to talk about
what a dependency is so
we can have values that depend on values.
That's a pretty simple thing.
We do that all the time. That's a
function.
So we can write a function.
We could put a value into that and
we had a result. And that result depends
on the value that we feed into the
function.
That's a very simple function over there.
That's the increment function is just
takes a natural number and gives us a
natural number. It gives us the
successor.
You can see that the
up there this is
excuse me.
So this is the type signature
to make this a little bit larger.
So that's better.
And this is the implementation.
So it just takes an argument X
incremented by one.
So very simple function on.
Another thing that might be interesting
to you, if you don't know programing
languages like Haskell, we do functional
applications just by saying nothing.
So no parentheses.
This is function application.
So normally you write F parents,
whatever, and we don't do it that way.
So that's some sort of dependency that we
want to have. We want to have values that
values, obviously.
So another thing that might be
interesting is we want to take type's
to values.
So think about the
identity function, the identity
functions. It just does nothing.
It just takes a value and returns the
value unmodified.
So when you have a lot of types, you have
to come up with a lot of different
implementation of the idea of the
identity function, which is pretty
boring.
So you want to write one identity
function that binds them all.
So you want to have a type as
an argument and then it returns a
function that can deal with
these things.
So in this case, we just
take a type A as an argument and
we return a function which is a value
from AA.
So here we
are using that.
So it takes that and that is the
type of natural numbers, which is just
zero, one, two, three, yada, yada,
and we turn it on modified.
So what's interesting about this is that
you can see we do type application
just the same way as we're doing it
with values.
So there's something weird going on.
If you've got a like C++,
you have these angled brackets or
Scollard, you've got square brackets to
type up a patient here.
This just feels like a value.
This is we're starting to get into the
realm of what it was really about.
So another example is just the same
thing with strings.
So another thing, another dependancy.
One half is want to have types
that depend on types.
So think about data structures.
So this is this is a linear list and
we want to build linear lists for every
type.
So
this is a type constructor.
It takes a type and it returns a new
type. So can say list, feed
and string and you get a list of string
and this this type
of stuff. Constructors, it has Knill,
which is just the empty list.
And this thing is pronounced KONE's.
We just we can take a value, take a list,
put the value in front of it and we get a
new list. So we're inductively generating
that list.
So here is an example.
We just have the list.
One, two, three, four, and we end with
the empty list.
That's a little bit clunky to write
because we're using the special kind of
syntax over there.
We can use this
very convenient list syntax to to
express that. So this is constructor
overloading. We can do that for
pretty much a lot of things.
So in
case you might notice, this little
single quote, this is just part of the
identifier. This is nothing special.
This is just so that I don't name
clash with the actual list in the
preview.
So, yeah, now we've got three different
kinds of dependencies.
So there's just one thing missing.
And that's the thing that you're missing
in most of the programing languages where
you've got where you can take values
to types.
That's that's the new thing.
This is what what we mean when we talk
about dependent types.
We can have types that depend on values.
So this is a string that
string vector and this vector is just
it's basically a list, but with the
length in the type.
So we we have additional information
in our type that says, OK, this
this vector is of length four
or whatever.
So obviously the vector is
length zero and the
case it takes a string,
a string vector of length then.
And what we get is a string vector
of length, one plus end.
And what's interesting about this, this
plus this is not a special type of a
plus. This is the same plus that we're
using on the value level.
So we've got a lot of for use here.
So whenever we've got a function that
we can use on a value level, we can use
that on the type level as long as it's
total. And yeah.
So this is
just an example. It's the string vector
of like four.
I have four elements.
If I were to delete one of these elements
and obviously it wouldn't compile, would
complain, hey, these lines don't match
up,
OK, this is too large
so we
can have a cake and eat it too.
We can build a vector
that is generic. So this is just the
same thing. String vector isn't very,
very useful because we can only put
strings in there.
So we don't want that. We want a vector
for everything and we also have that
in preload.
So this is a vector.
This is this has got the same
constructors as the list before.
It has the vector with with
length one we also got.
This is the same story.
So now let's implement something that
uses that. And in this case, we want to
implement the append function.
So append takes two vectors,
a vector of length N and the vector of
length M and the result
is a vector of like and plus M,
so the type tells us a lot of what's
going on here.
It's a little bit different, like the
Penford list where we just take a list, a
list, a list, a what does it do.
I don't know, I could just
throw away one of the lists.
So here we are implementing this function
in case the left hand side is the empty
list.
Empty vector. Excuse me, we just return
wise.
If it's the case,
we just take the front element.
We have we put it at the front and we
call upon recursively.
So we just
go through the list, put them together
and voila.
So there are two vectors one would
like for another one with for
we put them together, obviously
higher mathematics, length eight and
that that's great.
So, OK, that's that's
the view.
What. What.
Dependent types are what can do with them
and let's put them to use
and yeah, I want to talk about the
Kurihara correspondence, which,
well, it brings us into the land of
logic.
So there are a lot of logical connectors
out there and or not whatever.
And they actually they have
well, a corresponding type on the
in the Tipler in the title.
And so
when we look at something like this, this
looks very weird.
So this is a type
type with numbers and equals sign.
So we call this this type propositional
equality and
we can only constructed if the two
values on this equal
sign are are the
same thing.
Obviously they are by definition.
Twenty three equals twenty three.
So we can construct it.
This is a common.
This is just the pseudocode that I put up
there. So you can imagine how this looks
like. So it takes two arguments
sometimes something A, B
and we can construct this if
both sides are equal.
And what was interesting about this is
that twenty three equals twenty
three is all is a logical proposition.
So we
say this and we're going to prove that.
And whenever we write a program
that satisfies this type,
we've got a proof.
So proof the program is
a proof.
It's not just a simple program.
We can really use programs as proof.
And this gives us a lot of interesting
possibilities when we want to do
something like test driven development
type driven development where I come
from. So you can't really
write types that
do an exhaustive check.
So you can say for all this
holds, for all values of whatever,
this is a lot better than just a test,
which is pretty much an anecdote.
So I knew I know some values where this
works out and you can do this
in an exhaustive way.
So.
So since we've got logic, we want to have
something like true value.
This is a very trivial case.
So we call the subunit and
has one constructor.
So it's always true.
Whenever I say I want some value
of unit, here is proof.
It's just a simple empty tuple.
We're not using that. But just for the
sake of completeness,
obviously we want to have a notion of
what's false.
So I said that whenever we find a program
that implements type signature, that's
a proof.
So when we don't have a proof,
then this thing has got to be
false. It's an empty type we call an
uninhabited type.
So Voit has no constructors.
We shouldn't be able to construct that.
Sometimes there are bugs in the compiler.
I think recently the COK people
found something where they could
prove false happens all
the time.
It's it's software.
It's still failed, but it's pretty early.
So it's researching.
So, OK, this is the empty type
one. Have another thing which is called
conjunction. So when I want to prove A
and B a true, I want to give a
construction for that. And so once
again, I'm using propositional quality
there. These things are trivially true.
Twenty three equals twenty three yaara.
And this is the proof for
it. So when we want to prove that two
things are true, just give
me two proofs, give me the two proofs and
put them together in Sabal.
So whereas n there is
or we've got something
that's called the either type or some
type, in this case it takes
to type arguments and it has to
constructors either a constructor for
the left type which say or a constructor
for the right.
It says it's attacked union
if you like to say that.
So another example.
This is obviously true and this isn't.
But we've got a proof for this
proposition because we can construct this
value like an OR
if one of these things is
true, then we can construct the whole
value.
And this leads
to some very interesting conclusions
with logic. When you've got the last
exclude the excluded middle,
where you got every proposition, P, P
or not P is always true.
That's a problem because
there are unsolved problems.
People's enpi true or not
true.
Wycheproof, we don't know, we can't
provide a proof because we don't have a
proof for it and we have not we
don't even have a reputation,
so that's a problem and we are going to
deal with that.
So next thing, implication,
so when I've got a proof of something,
I can transform it into another proof.
So this is once again, this is very,
very trivial example.
So when A is true, it implies
that is true. Big deal.
And this is what this type signature
says. It's a very trivial
theorem, but it's it's
a theorem of less.
So this thing over
there is just a lambda.
If you know JavaScript, it's when you
write function, Perens, EXPAREL,
yada, yada, lots of stuff.
We just write backslash.
We thought it was better than just
writing function.
So here we're using that.
Pretty simple. Once again, you might
notice that we're not stating a
as a type argument.
That is it.
We can figure that out. I was a little
bit while noisy in the first
example. So here you go.
So now it's getting weird, now we're
getting into the penalty phase plan,
since we want to have something like a
predicate logic, we want to have
quantification, universal quantification
or quantification.
And this is the new universal case.
So it's just a generalization
of the function space.
So here, the
return type actually depends
on the value that we feed into the
function.
So this you can read this one is for
all natural numbers, we can say
one plus and equals and plus one.
That might sound trivial, but we need
proof that it's mathematics.
So natural numbers are defined
inductively.
It's either a zero or a successor.
So in the zero case we can say,
OK, we can fill in zero.
Are there we we see one equals
one. OK, reflexivity with one.
Next thing we Panorama's on the next
case along using here
is calling plus s recursively
and I'm using rewrite to rewrite the
goal.
It's not that important.
I can show it to you after the talk, but
we're not going to into depth.
So this is a proof by induction.
So the stuff you learn at school
and I never understand in school, but I
understand with different types what
word.
So it feels natural.
I don't know.
So just for the sake of completeness,
we've got existential quantification.
We are not going to talk about that.
But I just want to fill you in on the
stuff. Um, so
recall the vector.
The vector has length of
some natural number and
when we filter that, so we've got a
boolean function here that looks
at every value and figures out this is
true or false and we throw
out elements if there are false.
So we don't know what the lengths, but
we know there exists some natural number
that reflects that length.
We use this kind of weird Tupperware,
it's called, some people call this a
dependent couple.
Some people call it a dependent product.
Some people call that independence.
Some it's horribly confusing.
I like to call them signal type.
Yeah, very helpful.
So, yeah,
this is just we can say, OK, we can
filter this and we know that there exists
some length.
If we filter VMT, it's obviously
going to be the empty list.
But if we filter some cons
case, then we call filter recursively
and we go through it.
Either this is true, then
we increment the length by one, otherwise
we just throw it away and we don't keep
track of that.
So this type text as well.
So last thing, I hope
I'm not bothering you. So, um,
so this is negation.
We want to say when something is not
true, obviously two equals
three is not
true. Yeah.
So here
unconvincing it that this is not possible
when I'm saying OK, refl.
This doesn't work.
REFL is not a constructor of of two.
Exactly.
So we have to convince Esdras at some
point that this is not going to work.
So this impossible keyword helps.
So whenever we are trying to say that
something's not true or negate something,
we just say that this proposition
implies faults.
So it's a function.
So we have to map every value
in the starting set to a value
and in the in the image.
Yeah.
So
if, if the domain is empty
then we can't map it
then, then we can map every point.
But if the domain is not empty and the
domain is empty, we've got a problem
because we kind of map these types.
We cannot do this function.
So this is what this negation
stuff is about.
And now we're going to use that.
As I said before, the Law of the Excluded
Middle says that every
proposition is either true or not true,
which is a problem when we've got of
problems.
So.
We want to negate that, we would just say
not this is not true, which
would be a very big problem because then
we couldn't decide, decide if something
was true or not.
So we in this case, we're saying not
not. And that's not the classical not
not in classical logic.
Not not a is a.
So this is not
it's not that way in constructive logic.
So what this is saying is say we do not
refute the law of the excluded middle.
We cannot assume it in general,
which is a very important distinction.
So this
either A not a is
so popular that we got
it's on tape.
We call it deck for the Citable, and we
will use that in the same sample.
So life quoting once we fail.
So let's try a new model.
We call this demo.
And yeah.
So I want to introduce you to a
nice little
data structure, which is called Free.
And it takes a type
and it turns out.
So it's got to constructor's got a leaf
and branch.
So tree of a
branch and it takes
a value of eight, takes the left hand
tree and the right tree and
returns the tree.
So.
So this type takes so we can
type check this in them, if
you're using IMEX, there is a great emacs
mode,
so everyone served here,
so.
Oh, excuse me.
And as we just have to
just have to leave.
It's just a leaf leaf
ranch, leaf ranch, whatever, so
you can take an empty tree is just a
leaf.
Whatever, yeah,
value, yes,
it doesn't have a value level, we can
think of it as a liability, so
let's build something that we can live
with and we've
got a function from A to B to C,
and it takes a tree of A.P.
and returns a tree of C,
so we put them on top of each other and
just well, apply
the function to all the Paris.
So, yeah.
I can say, give me a definition, so this
is one of the this is the interactive
stuff that I was talking
about, need to do
something and it will help the compiler a
little bit here.
Excuse me.
So there's be so I'm
just telling you this.
Please choose these names because it is
terrible at choosing names.
It's horrible, really.
Trust me. So what I can do now is I can
do pattern matching.
I can, but in
this case I can do case splitting.
So give me all the cases that you
want, can have
it and can have two cases, can have
a leaf or branch.
So yeah. Cool.
Let's keep going.
So careful.
OK, this works
ok.
These things are called holds
on metal variables.
It's a part of the program that we didn't
write yet and we can ask address
are what type does it have.
So this is what we know.
We know these things.
This is where we want to get.
So can I can
ask Idriz, can you solve this problem,
can solve that for me?
And in this case it could.
But what happens
if we got this case so
we can throw away data?
That might be the tactic
that we want to use in some cases.
But in other cases, that might be bad
because we are losing information.
We don't want to have that.
So this is this is
kind of bad.
We don't want that.
We don't want these two cases to happen.
So because we're we're losing information
here.
So what I'm going to do is I'm going to
introduce a new type,
which is tree shape.
And it's just the type
and that's called this a leaf shape,
which is a tree shape and the branch
shape
which takes the tree shape
and reshape.
And so this is the shape
of the left and right branch.
Let's throw this one away
and take a tree shape here.
So this is obviously
we think this has some
shape as some shape
as prime, and it will take
a branch shape of
S in its prime.
So once again, that
was
see,
so
now I'm assuming that these trees are
going to have the same shape.
Oh, this is wrong.
This OK,
obviously this type Czechia.
That's nice.
So now we can explain
once again, kispert
here, split there.
And lo and behold.
The other cases, they don't show up
anymore because it was figured out
if this one belief,
then this has to be a life as well.
Same goes for the branch because
they all got the same shape we
statically and guaranteed
that these safes got to be
the same.
So now this this is getting pretty nice.
So in Haskell, you've got something
that's called type inference where you
can write program and
Housel can infer the type.
We can't do that independently type
language, but we can do something else.
You can say write this program.
It was it
was said, OK, that's we
can do this. This looks pretty tricky.
Yes, it can do that.
So this is pretty neat
once we've got enough information that
high level.
Yes, I can sympathize.
This blew me out of the water when I saw
it first. This is so
great work. Everyone does
even better at that.
But yeah, so
it can figure out
by the information that it's got there
so we can look at that.
So it's a lot of information, but I've
written this by hand, but we don't need
it.
That's pretty nice.
So let's let's prove something.
Let's, let's write a function and
we call this one is Ellem and we want to
check if an element is in
the tree.
And I'm going to gloss over this
detail for a second.
So bear with me, please.
So we've got some element of X
of Type A.
We've got a treaty which has some
say it asks and it has elements
of it. So what?
So what could be the
the result type that we
want here in in a
lot of languages, we say, OK, this is a
boolean, but that's a
little bit problematic because a boolean
doesn't really convey any information.
It's just it's just saying yes or no.
It's like the answer is forty two.
What's the question?
It's not very helpful.
So what I want to do now
is I want to write
a predicate that contains
a lot more information than just the
boolean.
In the case of the Boolean, I could just
write false for every case so I could
write a wrong function here.
So let's write a predicate.
We call this is Ellum
and
it looks like this.
So let me
look at my church here
x the branch
and the left and the right tree.
So this is a proof that we found the
element.
So we're not
saying this is we're not just saying, OK,
we found the element, but we are
constructing a path to find this element.
So this is the proof that we found it.
Obviously, we need are
the paths.
So if we know that
is X is in the left branch,
then we can say
it's in.
This tree.
Oh, what are you doing
there,
telling me
it again, unexpected and
food,
what is so er.
Yeah
so say hello
to the type again
so we can decide this problem
can say for all elements
of type A, for some tree we
can decide if the element is in there.
This is why, this is why I introduced the
deck type anyway.
So
obviously we need the right
content
so yes
please. Type.
Yeah.
We get to the later, OK?
Can can can an element be in a leaf?
So look at the constructor.
No, it can't.
So the branch
you can. A branch.
Yeah. The leaf doesn't have an element.
That's what I meant with empty tree.
It doesn't have any elements in this
case.
Now, it'll be a little bit smaller here.
Yeah. Because of the tree of a
leaf and the leaf.
But yeah, because it's a tree of a
but it doesn't have any elements.
Yeah.
It's an empty it's an empty
tree of type A,
whatever is.
So it's split here
and let's find out.
What is what we want here?
So obviously there cannot be an element
in this in this thing because Leif
doesn't have any values in there.
So what I'm going to right now is.
A function that says
not in life,
so yeah, and
I'm going to extract the Lamba,
so let me
get rid of this.
Sometimes it was very
just wants to add a lot a lot of
arguments.
OK, let's just to you,
not in life
excuse me here.
And this is just impossible.
This is this is once again,
so in this case,
this this this thing doesn't have any
elements, therefore it cannot have
X in it.
So this proof
says
be in there.
Ah, yeah, and tiebreaks,
so we can right here.
This is just the same thing, let's make
this a little prayer.
So now we've got to prove that
in a leaf there can be any elements.
So we've got a reputation for that.
So
to do something else.
Well, I'm going to do now is I'm going to
do something that's called a width
pattern, which is an intermediate
computation.
And now I'm going to use this
technique. So this is a type class
that says for type A, we can
decide if two things are equal.
So there are there are some things that
cannot we cannot prove to be equal.
It's a little bit bothersome, but,
yeah, they exist.
So we can explain once again,
once again.
And look at that.
So.
This is why and once I'm
doing pattern matching here.
It turns into acts, so it figured out
that these two elements got
to be the same because we've got a proof
of that. This is dependent pattern
matching or non-linear
matching.
So let's once again try to find proof
and here's a proof.
So writing these things is utterly
boring.
This is got this
written down somewhere.
So, yeah. This is oh,
so hot and loaded,
Volmer.
Hmm, that's just an address.
It's nothing interesting, really.
So sources address
31 simply
I said this is
this is
demised them your
family.
So this is the whole thing.
And I don't want to write that.
This is just utterly boring.
Most of it was right before it was right
for you.
So what we got here is we
got to prove that we didn't find the
value in the industry
if we didn't find a value, the left
left branch and we didn't find a value in
the right branch. And this is a proof
that it's now four minutes,
40, 50 minutes, OK?
So this is a proof that it's not under a
tree. So
that's what I told you.
It's a decided problem whether that
thing is under the tree or not.
So, yeah, that was life coding
and not wanting to talk a little bit
about effects.
So until now, we didn't do any side
effects. And if you know, Haskell, there
is this that m word
I'm not going to mention here.
People people tend to get scared
every time I say that.
So
we've got something that's called
algebraic effects. I don't know if that
sound less scary. I don't think so.
So this is a very dumb
program, but nevertheless, it has
some interesting things to tell us.
So up there, this
is a very horrible
looking type signature, but
that's in fact the type signature.
So when we write types that
are bigger than the problem programs,
sometimes that
feels kind of weird. But OK, so what
this notation says,
we've got two effects,
got IO and we've got standard
IO so we can use the file
effect to work with filesystem.
We can open files, read files, files,
whatever
standard. I always just write something
to the console.
Nothing special here.
And we can put them into this list
so we can have a very expressive
type type signature, this type section
which tells us what what can go on.
So in Haskell there is this I o type and
it can pretty much do everything so it
can communicate with the outside world
or calculate pide, your hard drive,
whatever.
So in this case we just know,
OK, it's finial,
they can do some stuff on the file system
and it can write to
write to the council or read from the
console.
So
this type signature has a very
interesting
if the Sultan has a very
interesting Tapson dysfunction open
recognize that if then
else on the type level.
And what it does is
actually figure this out is
could we open the file if yes.
Then we've got an open file handle,
otherwise we don't have one.
So this is what we want
to use, something like if it's on the
type level.
So if we look at this affects example
once again.
We are pattern matching on the result,
is this a successful operation
in this case? Yeah, I can read from it.
So let me try to compile that.
The effects that.
Takes a lot of time,
it does a lot of things,
and the complaints gets faster, so it
just reads in the first line of
of this program of of the source code.
So, yeah.
So what happens if we do something like
that?
We're not closing the file.
Try to combat that.
And I was complaining, it says it went
wrong.
Basically, we are working
on something that's called a reflection,
which makes this stuff readable,
but if you squint a little bit, you might
be able to read it or if you're
just using it for very long time.
But what this actually says, it's OK.
You promised me that.
This thing would be closed
once you want to leave the program.
I didn't do that.
So it's still an open file handle so we
can track the files are open
as one of these things that happened
quite a lot. Are you aware of the
database? And you just leave that open
and you run on file handles and your
application crashes and everyone's sad
and.
Yeah, so you can check that.
We can check that a compile time.
We could also do something like that.
We tried to
read from and from closed file.
So yeah, this is going to spit
something else out that you're probably
not able to read. I'm,
I can't do that as well.
So yeah.
So
this is pretty useful
and I want to show you something that is
even more useful, maybe not
too much, but so
this is a little demo that does
typed csv.
So we read in CSV
and look at the the schema,
just the header file and look at ok,
what, what columns do we have
and read that and
we do that at compile time.
So once we compile this program
it goes out, reads in the file, picks
out the the header and generates
a schema.
And what's interesting about that
is.
So.
Yeah, there's a spokesman, so.
So this says, OK,
reading the file, read and my CSFI
pick out the header, generate a schema,
call this one test schema, and
whenever we add a new
row to this and all,
we want to query that we've got compile
time guarantees that this value is
actually in the CSFI.
So we don't have to check.
This is in their.
This will always succeed.
I'm going a little bit over the top with
this because I'm also stating the
amount of rose that I'm reading in, which
is a little bit too much to be practical,
but it's just for fun.
So, yeah, let me show that to you.
So let's compare that.
That takes even longer.
Yeah, that took quite some time,
so, yeah, it's Siggie, it's German
Puckerman, I'm sorry.
So let me carry something else which
isn't there.
Don't me. It was.
Yeah, and say, OK, this is this
is not element of the scheme, we couldn't
solve that.
You might recognize this is something
which is
over here in
this album.
So this is this should look familiar
somehow.
And
that's pretty neat.
So this one this
line constructs such a proof
automatically. So we don't want to.
Right there.
There are there here.
That's that's a dumb task.
So that compiler can do that.
So this is what this process is doing.
So whenever we are looking up some field
F in some schema,
we just try to find the proof
that it's in there.
And then return the result.
So, yeah, ten minutes,
I think I'm done here.
So if you want to ask me questions,
please go ahead.
My mind is still blown, but if you have
questions lined up in front of the
microphone and ask
away,
let's grill the speaker,
microphone one, OK, so thank
you for your time.
It was interesting because I think I have
a question. Is it possible to make
errors a little better?
I mean, are to detect
some example type
mismatch and write
that the file was not closed,
that case? That's possible.
So someone's working on this
thing called our reflection, and it
gives you a type structure, a data
structure that represents this error.
And you can write an interest program
that interprets that error message
and gives you something that a human can
actually read this.
So this is one of the things why the
penalties are research.
We don't really know how to handle this
stuff. It's it's very hard
to write big applications in address
at the moment.
OK, over to Mike.
Yeah. Hey, how is it
implemented?
Is it running in a VM is itself hosted?
It's it's not self hosted at the
moment.
It's it's really in Haskell.
So if yes.
I love Haskell.
So it's a great language.
So we are planning to
rewrite it maybe at some point,
but there are not a lot of things in
place that we need.
So we've got this part of the library
called Licia, which is a pun on Parsec
from Haskell.
And this this is what I'm using
in this in this
in this case, we Pavo.
So we need stuff like that.
We need when when you look at the at
the it was interpretor or the compiler,
it has a lot of dependencies and we are
not nearly there.
So maybe at some point
we'll be self Holsted it's but it's not
a priority but so what is it.
So the compiler generates,
the compiler generates generates C
and puts an object.
OK, so it generates
JavaScript or whatever.
Yeah.
Like one, I
have two questions, actually.
OK, first one, do you
have any other any projects
that you know of that try to apply this
typing to imperative programing languages
as opposed to functional?
Excuse me, I didn't get there.
Are there any are
there any experiments trying to project
dependent typing to imperative programing
languages?
I know of a project that's called Flow
that is run by Facebook.
It's something that does statically
checking on on JavaScript.
And I've I've seen some of the ideas.
So this branches, if then else branches,
it knows in which
part of the branch it is.
And I don't know if it really qualifies
as being dependably typed.
I don't think so.
But there is a
there is a project that tries
to bring dependent types to JavaScript as
well.
Um,
Schola actually has dependent types.
It's it's pretty much the first
commercial programing language that
offers dependent types, even though not
full dependent types like we have an
address, but something
that is pretty powerful.
OK, next question.
The example of the trees where you
have this tree shaped type, how was that
actually implemented?
Do you do you have for every tree shape
one runtime object?
If you construct a new tree, you have to
do this. Every tree node construct
a new country.
You don't need a you don't need these
tree shapes at runtime.
They can get raised.
So you don't need to store your indices
so you don't have to carry around the
length of the vector as well.
So it just
isn't that isn't that isn't that needed
for the paper on that?
Bye bye, everyone. Brady that that's
called are how
is it called like of something like
adductor families don't need to carry
their indices or something like that.
I don't know if it's something like that.
You can't erase them. You don't need to.
Sometimes you carry them around when you
want to inspect them a runtime, but you
don't need them, General.
OK, over to Mike three,
quick question, is it as lazy as Haskell
now, so we've got
a strict construct, a lazy constructor.
You can have you can put laziness,
annotations and but
it's a strict language.
So this is this is geared toward system
programing. And Edwin wanted to have
something that that is actually strict
so you can reason about space
and stuff like that.
Easier, Mike, to
just the question about these types and
proofs that seem to have
I'm intrigued.
Does this do any propagation of
propagation to get the things
that you see there when it comes up with
a redefinitions, et cetera, or
do conflicts?
In other words, does it do an empty,
complete search and
aborts eventually when it's sort of like,
oh, well, I'll be searching for half an
hour and, you know, I'm not going to come
up with this definition anymore?
Or do you only do propagation
of facts like IBM or
the or the current compilers, let's
put it that way.
So I think that's a question that
probably Hadwin should answer.
I don't, I don't think I know the answer
to this. I'm sorry.
Yeah.
OK, like one.
Yes I have two questions.
Also the first one is
you showed some first order logic,
existential
and universal quantifiers.
Can you do also second order logic.
So quantum person sets or
or is that beyond the scope of the
language?
I didn't get that as well.
Sorry. So can you do second order logic
also or is it just first order?
Uh, also modal logic.
Is that in temporal modal logic or.
Oh, that's a good question.
I don't know if I really
need to try.
But also the second second question is,
um, so you
show this V example and
it seemed like do you actually like
to have the impetuses
be available for, like,
compiling? Yeah.
So, yeah, you can you
can use this in a like
another nice example will be like
table four for database
so you can call the database,
get the schema and types there.
So this is obviously it's just an
example. It's not really something that
is super useful, but I think it's
it's a neat example to to just demo a lot
of the stuff that what happens if it's
if if you feed it with a different
SISMI and then then you need
to. So you need to compile that once
again. Yeah. This is so it can't change
the program magically.
Just it's it's come out
and say you
need to actually check the input somehow
if you're running it, if the schema
changes you need to change a to
recompile. Yeah.
Signal and you'll do we have any
questions from IOC and stuff.
No.
OK,
Mike.
Sorry. Yeah.
So in that example if the file handles
that's the implication of that, that you
could not with a given types,
write a program but has to difficult
logic governing whether the handler was
in fact closed or
is it that compilation might in fact not
terminate?
Um.
Good question. Oh no, it's not it's not
really that. So you just you're
the type system that forces you to handle
these to tackle
these two cases. So you're not actually
compiling the file handle doesn't get
open during compilation.
So that's not what I mean.
OK, I mean, so
what is the I mean, basically,
presumably have a certain logic
which is captured by this type system,
which it might or might not
be desirable. And if it's the citable, it
probably means that you cannot prove
things that are particularly complicated.
But programs cannot prove
the termination of particularly
complicated programs they
can say of type system to citable.
That's what I'm ultimately asking,
is the types of undecidable are I?
That's I think that should be
the.
Dependent, dependent type checking
is I don't I think there was a paper that
says it's not desirable, but I'm
very thin ice here.
This is so so you're asking theoretical
questions. I'm just some compiler
wannabe hacker.
Just I'm not too sure.
You know, this is perfectly fine.
Yeah.
Mike, please.
If you
if you have a question, Gary's come to
Mike.
So he's he's
got the answer to your question, I think,
sir, that.
So we can take this country.
Can you go to a microphone, please?
So how many recordings?
I have a question regarding the example
for the file handling
the closing of the file
cannulas where there is an
error if the file is
not closed.
Yeah. And is it possible
to generate the closed, closed
statement automatically?
So to satisfy that the
file is closed at the end, that's
automatically closing.
That's yes.
That's a good question. I don't know
that.
But if it might be
possible, because the same
same thing can be applied to the memory
management or research resource
management in general.
I don't I don't know, I haven't tried
that could be possible.
Probably thinks so,
let's find out, maybe stack on it.
OK, last question, Mike, three.
Do if this language only a
proof of concept or do you plan
to support it a long time?
And what are your plans to
implement next?
This is once again a question that should
be asked to anyone, but we talked
about this quite a lot.
This is an experiment.
There are a lot of different approaches
to dependent types.
There are a lot of different kinds of
type, like intentional type,
extensional type theory, observational
type theory there.
People try to come up
with all sorts of different approaches
there, and it was pretty
conservative in its approach.
So we just it's just one
way maybe it will turn into
a programing language that can use in
production, I don't know, ten years.
I don't know, maybe never.
So this is so currently this is
just a fun project to to find out
where it's where we're going with that.
We can go with that.
Yeah, sure.
All the housekeeping now, if you're
leaving, take anything with you and
a round of applause for Rachel.
Thanks for your attention.