Player is loading...
TwoFace values: a bridge between terms and types
Friday, June 14, 2019 · 3:43 p.m. · 32m 55s
Scala 2.13 introduces literal types, and with great types comes great thirst for power to control them. In this talk we get acquainted with the singleton-ops library, a typelevel programming library that enables constraining and performing operations on literal types. We learn about the library’s TwoFace value feature, and how it can be used to bridge the gap between types and terms by converting a type expression to term expression and vice-versa.
Embed
Transcriptions
Note: this content has been automatically generated.
00:00:01
yeah i'll
00:00:03
fun to be here after a that's got that my first conference a conference uh um
00:00:10
i hope you don't mind i use that i like those colour uh they slide so a map that
00:00:14
to be a type levels colour there was no mutations
00:00:18
just object composition um so what it's all about me
00:00:26
uh this is the the um p. h. d. students and nine
00:00:29
c. uh uses got uh in many of the d. s. l.
00:00:33
uh it's a great idea so the engine to create a that the flow problem description language
00:00:40
uh if somebody's in those the the next month of the other really so you can come to me and ask questions
00:00:46
uh yeah i'm uh and with a a mad contributor
00:00:49
to this because it's them mostly to segment the ops
00:00:53
and they like you like to watch sit meetings but uh
00:00:59
so all of you know we we've ever start with
00:01:02
mine with the patient to help they're promoting the don't laughs
00:01:07
and the i introduce a then we introduced the new
00:01:11
blue though types that were active he's got two thirteen
00:01:15
uh we we continue on to introduce to think of
00:01:18
the knobs library and uh it's features to face eject buttons
00:01:24
and that would be the few a few seconds talk about
00:01:28
discovery situation with sixteen that don't ops and then we can come
00:01:33
okay this is the motivation example those who don't know what
00:01:38
it is it's a you describe what's how to construct couple of how the has a bit accurate types
00:01:45
so let's take an example for a fixed size
00:01:49
back to like uh uh with big vector using mass
00:01:53
and it has we don't care about that stuff back and enhance it has a a size
00:01:59
and fixed size and we want to be able to come got to an active but those together
00:02:05
and we want to select possible bother that go to create a new stuff that go for it
00:02:11
so far so good that's what we once
00:02:14
but we want everything to be constraints properly so
00:02:18
we want the a selection uh of
00:02:23
the bounced to beach acts and we won
00:02:27
the when we create the fix i suspect so uh we can recreate
00:02:31
something with zero uh elements or this so this is the first real attempts
00:02:39
uh we add requires theta though well required
00:02:44
yeah and by the way for an example why can't we can't drop new completely daddy
00:02:51
is because we need to separate us where we call an unchecked
00:02:56
and much and checked unchecked a creation of this the the yeah
00:03:01
he's a first class so oh this is a very simple
00:03:06
but no one time only very unsafe we don't like that
00:03:11
so let's uh we're all here that are discussed sing about where we are on
00:03:16
the way out way too that uh and we first get to use their little types
00:03:21
electro types or other they like it's a basic
00:03:25
twenty three it was also a earlier at the the
00:03:29
as a demonstration in the type of it's gotta by miles seven
00:03:34
uh and i know that would leave those change most probably uh i believe it was a type
00:03:41
one week was actually give it one instead of going to shapeless and with this
00:03:47
um so every type is a supporter of the very primitive type
00:03:52
is supported for that and it has a this sip also adds
00:03:58
to our though you like that construct the stars sorry that's not an upper bound
00:04:03
so it would prevent the the four whitening or a mechanism it's gotta
00:04:09
and um uh it also has a
00:04:13
way to fetch the value from it died
00:04:16
the way within this eh was used so with this you'd only reviewed shapeless with us
00:04:24
so let's examines some the some things
00:04:28
first what is at the five for the for statement by one week was the one letter
00:04:34
yeah yeah we get a warm with the in that type
00:04:40
and the white type in because we get out no adam attic whitening
00:04:45
to prevent that we can either force it with a little tight so
00:04:49
we've was the no type one oh we can uh say it's fine
00:04:56
uh the level says it's in its brackets one but
00:05:00
it's the same as the what the first the statement about
00:05:05
yeah and we can also forced a a
00:05:09
widening a cat in case of uh the final
00:05:14
with the next statement come by ah
00:05:18
i mean i think it won't come by
00:05:22
i really think it will come
00:05:25
okay the next segment one compact because we have type mismatch of a constant types
00:05:32
now uh the next segment does compile because this
00:05:37
is the one i thought type is still type
00:05:41
one uh constantine one so it also we combine
00:05:46
yeah yeah however the next one does not comply ah
00:05:52
why because want a a is is actually essentially it can't
00:05:57
so it does not a compound when we try to force a
00:06:03
yeah and and why didn't into a narrow uh in this case one little
00:06:10
well the next one next technical bile
00:06:14
i mean i think it will combine
00:06:17
okay so it it does compile because basic on starts operations on in line
00:06:24
eh you'll tones that types with the next statement comply with things it will come by
00:06:32
what would be the l. message for the next statements
00:06:38
it doesn't know what type minus this okay so something that
00:06:43
would someone doesn't know starlight all adults uh that that says
00:06:48
that makes sense but no it does not make sense if you know what you're doing
00:06:53
yeah but we wanted to make sense within the office somehow some magical way
00:07:00
okay with the next segment comp ah i mean i think it will compile
00:07:08
okay does compile actually yes surprise uh the uh it there is no actual
00:07:15
conversion will because if we look at the next one uh the next statement
00:07:19
uh the which was it in the to be you won a
00:07:25
lot uh a long but uh that this behaviour is the same means
00:07:31
kyle of all the versions and dotty i have no idea why it exists but it
00:07:35
does it's worth knowing when you instead of experiments that there is a bit for here
00:07:40
of course the next uh statement uh it it does not in line so we get
00:07:46
uh uh that too long is a combo too long as well if we want to make
00:07:52
our marks of two variables as this statement uh also does not in line
00:07:58
and that's important because we want to do some more basic operations
00:08:03
a way to be able to constrain some things and we want to be able to in line then as well
00:08:10
so uh how does the uh a segment on an upper bound works so we
00:08:16
forces the narrowing when applied to an argument and
00:08:22
when we use now on one really actually get to one uh when we use the
00:08:28
why don't we get any okay so that we must use this thing in the upper bound
00:08:33
to make sure that the us colour doesn't whine our arguments
00:08:39
sadly the next segment like the first one also compile
00:08:43
again this is some we behave i do not know why
00:08:47
okay uh this is the example how with uh the value always use like shape it's uh with this
00:08:55
so we have no nato co a little types and we want to compile them
00:09:00
anyway and we want to use them for compile die yeah safety and yeah yeah so
00:09:07
we have eh now instead of inane we once the
00:09:11
okay size is in its uh with a with a single
00:09:17
and the company they concatenation is also with an argument with singleton
00:09:23
but something we don't know what to do many somehow to set the type of
00:09:29
the outputs which should be additional baseline
00:09:32
us and as a as a nice too
00:09:36
how do we do that we i won't even get started on how
00:09:42
we're supposed to get to do the selection it'll because trains and checks
00:09:46
to the limit compile time which supposed to be possible because that information is available
00:09:52
and that and uh here we is still are forced to create some uh
00:09:59
yeah run time a check because we still have a normal
00:10:02
way of me has describing a mechanism to come stated eighteen
00:10:07
uh compile time other then we of the refined like right
00:10:14
so if we cannot so again we cannot work
00:10:19
without some special though so we need some special help
00:10:25
um so i will say uh the void to do something that allows some of the features you
00:10:32
say oh this can be done which it does all this can be down we find in the
00:10:36
uh uh but we will show or something that is eh eh a wider concept
00:10:43
so it's also the features of singapore's ops is to expand the default compiler in lining
00:10:49
in the non trivial cases like marks of two elements it to balance
00:10:55
a work around those of us easy in ego whitening
00:11:00
yeah we want to support various type operations
00:11:04
not believe this level button but type operations
00:11:07
we want to support any composition of type operation is to create type expressions again moving
00:11:13
there's not really type explosions and see um we ought to support
00:11:17
all the basic types eh yeah also interact with net and symbols that
00:11:22
the following is impossible deprecated and that the the valves as well and the yeah yeah
00:11:29
we want to assume like type expression compile time equivalency like
00:11:34
the statement that wasn't supposed to comply yeah and we want to be
00:11:40
able to come by and to a safely check uh at compile time constraints
00:11:46
and you should yeah yeah we don't have that information event fallback to run time checks
00:11:52
so how do you think that stops for this is the slide view for the next generations purposes
00:11:59
uh yeah we have two large impulse
00:12:05
off library and the addition of the two face inject the main spaces
00:12:11
well the basic type operation which right that has an out that
00:12:16
type and the value with uh that uh with that type out
00:12:21
and the way it using a the magical
00:12:25
white box mark was we're supposed to feel those
00:12:28
yeah it to to create the headed for the specific operation
00:12:34
they're like oh this is a bit more complicated because we
00:12:38
neither actually for every type of out we have we need a
00:12:44
a type of uh out different type of overlap abound so we can assign them to future up about that
00:12:50
i rely on that uh upper bound is the
00:12:54
uh the uh the constraints in that type argument
00:13:00
and we yeah actually uh and a
00:13:03
large michael that handles most of everything
00:13:07
so it has the upper and eh the op name and it uh is it up to three parameters
00:13:14
and these parameters can be again a composition of the or what marco
00:13:18
again again and the uh my quarter versus the tree and uh and
00:13:25
and calculates that the out revolt of all the operations
00:13:30
so an example that i yes loss is the all michael possibly the two arguments
00:13:36
and the the type alias of a
00:13:40
requirements is in uh does something similar
00:13:45
so let's take an example yeah we have we want
00:13:48
to do an average oh three arguments a. b. c.
00:13:53
yeah we want to go buy a a crew to create a compile time calculation of it it's
00:13:59
uh so we provide only because it got
00:14:03
a plus b. plus yep was we had this thing and the most important and
00:14:09
that's that's okay that's so when we uh run the
00:14:13
idea man to be gets this case uh comes that six
00:14:17
but what happens if we do every feed a along
00:14:23
so in case so uh and i think it's a values
00:14:27
uh we can do in fact one long lost five
00:14:32
last whatever the result would be a along with so
00:14:36
uh it it it was a big favour in
00:14:39
second half the fuel britain's ago but to build more
00:14:42
straight into in case of types i remove it so it does not support so in the i always given
00:14:49
yeah um and what happens if we have a non literal type present
00:14:55
so so you know i was gonna do the calculations but at first it with or
00:14:59
you know no no no give me accept non literal result so when we do that
00:15:07
the and the actual results is a a six but the return
00:15:12
uh the value will be six but the the the term will be wide it's
00:15:20
so think about knobs supports various type operations the a plus
00:15:25
minus and salon comparisons eh
00:15:29
logic operations if then else logic
00:15:32
the various methane constance a conversion
00:15:36
operations died checks then the strain
00:15:40
that sums up so that would be operations all of those again
00:15:45
at compile time eh or would be reduced to just uh constants
00:15:52
it also supports some special type operation that that we've
00:15:57
seen only about the x. that none of the tool
00:16:00
and the question of is is it known that or or various uses
00:16:05
also supports a row we choir a statement for one to create constraints
00:16:11
so we can just a week while in the condition and a generally message will uh pop out
00:16:17
all we can use uh yeah actually give a message uh maybe we'll see an example uh uh later
00:16:24
and in cases that at this constraint is some kind of an implicit document uh the
00:16:30
as for when we want when uh someone some implicit or
00:16:34
where it it right there as so we can relate that
00:16:40
uh this message into the s. that the implicit non phone imitation of that right
00:16:46
so this helps to keep the l. messages and non gripped
00:16:54
so now we have a single laughs as a a to help us
00:16:59
and this is why it looks like the few changes just to reduce down and some things
00:17:04
so instead over ain't within and don't think about also has an alias so
00:17:09
we call it next in this one still an extra hour it's it is playing
00:17:14
and she here we have the operation and we also add something called a
00:17:20
safety because we want the the out of it to be a a yeah
00:17:26
we want to make sure it uh it is and and so this make sure that
00:17:31
we use out it's the out which is an end and it's constant and so on
00:17:37
um a few we have their
00:17:40
requirements okay and uh the constraints so
00:17:45
we the condition needs a does the side will be logged into the or
00:17:50
well that and we compose our messages so the l. message that we
00:17:55
had in at one time now we can have that ain't a compile time
00:18:01
so we have you we don't have a type yeah yeah
00:18:06
string interpolation so all we're forced to use the process
00:18:09
thing like the old days about like at least something
00:18:14
yeah and that's about that's will compile time
00:18:19
so if you run a few examples yeah we curator back uh one of echo
00:18:25
to and that created with that one and two and as the one two types
00:18:31
and if we try just there's a greater better with zero we
00:18:34
get a nickel by time tables size must be positive on zero
00:18:38
yeah we can come by the vectors and we actually get this not out but
00:18:44
as uh the apple sells but if we checked actually what the uh
00:18:49
uh l. what the type of uh is it on is actually three so it's correct and
00:18:55
it's also we can put that that the impact of the one again the the result is free
00:19:01
uh so everything works out well yeah yeah but if
00:19:06
we try to yap just have a run time value one
00:19:12
then it's uh the signals that yeah that's that value from from
00:19:16
large messages we don't really care about because if it's not known compiler
00:19:22
so at the one hand we had gone by the time a run time yeah
00:19:28
h. x. everything worked uh but it was not very unsafe now we have a loving save but
00:19:33
we cannot use the use run time as a fall back
00:19:39
so we want to do something else
00:19:44
to face all the hope so a a
00:19:48
two phase values are named like that because one
00:19:51
side is types and the other side is terms
00:19:55
so of course type is the pretty try and
00:20:01
yeah it to face value was not something that complicated they're actually value
00:20:06
classes with dedicated to get the best effort in lining we can have
00:20:12
so and we made them so they're a a drop in replacements for the counter uh
00:20:18
a primitive so to face if you place it a little that
00:20:21
i think is placed in a it should work in most cases
00:20:26
and but it should provide the in lining capability if it's present
00:20:32
if not there is the fall back over run time like
00:20:35
the the the primitive with that worked as a as well
00:20:40
so uh to place a it to replace classes
00:20:43
have a single type document for that one but that
00:20:47
and that's so a a a to it can become tight like a a one will be at that
00:20:53
one but if we had a one time one dad that she
00:20:57
would be that in its and we will see no an example
00:21:02
so a lot of ways rectal overcomes little one
00:21:05
gives us yeah and and in that the position
00:21:10
however i run time one would be bus uh at
00:21:14
and there were the wide uh infinitive in the position
00:21:19
then uh a boat i but we have the long time value so
00:21:24
both can be used in run time but only one can be used
00:21:29
with other compile time a knowledge said that eh it
00:21:33
eh tags to calculate the uh compile time eh values
00:21:39
and what's important is that if we have the competent calculation then the land that conclusion doesn't occur though
00:21:45
so then in lining is is there is truly in
00:21:51
and we have examples if we have a two phase of one plus
00:21:55
two piece of while we get a two phase of two again on stuff
00:21:59
but if one of the arguments in the plus operation when inspiration
00:22:04
ease non literal then of course we get an on little with
00:22:08
the result that the tag but we still have that on time value
00:22:13
we can also have a at the to face value
00:22:16
with the literal and it will produce an lead to results
00:22:23
so i know the rules over to face those was call that we use the in the place it will face dot shell
00:22:31
uh i shall it it says okay i have an operation
00:22:36
i have a i know what the calculation is like if the
00:22:40
if then else is it now it's a shell of free arguments
00:22:43
so i i get the type argument and what the white type robots all where i have there
00:22:50
it they if he's we on and the tools statement is enter and a l.
00:22:54
statement i think so i had an if then else statement over in it and and
00:23:02
and with this uh with and they said we had to
00:23:06
do fall or the equivalent uh about a capabilities of two fixed
00:23:13
so we doubts uh and so this shell is how we're
00:23:18
going to do our operation in the it's the size of vector
00:23:24
we can that excites vector so we here we have a shallow to that last operation
00:23:30
an argument as to why because they had an argument is too and the white incense
00:23:35
and we free that that to values that it uses the outside
00:23:40
and that's i got the shot only says okay what the what the
00:23:44
they're what operation should exist it's always creates a
00:23:50
the of a placement to have uh we can so
00:23:52
we can add arguments uh an ad at these positions
00:23:57
so that type this uh type arguments uh does that
00:24:02
this type expression is move on to be a term expansion
00:24:08
i don't states yet show what's going on with the selection
00:24:12
however to facial is not really necessary okay in this case usually were no that we we
00:24:19
if you have implicit in you don't uh really them all the way to the call side
00:24:24
not something one work but here in this case of everything would work but what happens that
00:24:31
we leak into the course i that uh time yeah we'll be one plus two
00:24:37
plus meaning the uh the plus my corporation that is quite
00:24:42
of course it would be very very ugly because the a
00:24:46
and the rubber because that's got a c. is a uh
00:24:51
is the analysing their yeah so it it can become a really large uh uh yes
00:24:59
eh every largely but uh uh again usually you
00:25:03
can use the the shared and it's it's really fun
00:25:08
so the two faced term expression here becomes a type expression
00:25:13
at the at the out if we don't use the show
00:25:18
so now we can have checked values shared values are to face value was with constraints
00:25:25
the constraints so check the compile time you've possible if not possible then there's a run time
00:25:30
check that we can call and but one time check is the it will lead to an exception
00:25:37
so how it looks let's implement this their size check that a we have weeks then
00:25:45
yeah it here without any parameters so is the checked your parameter we just had a
00:25:51
this size which must say it's bigger than zero again and the message that we had
00:25:57
was different than we had previously then we showed when i show this
00:26:02
is now we eh this site everything here
00:26:06
check support run time and come a bottom part time and run time as a folder
00:26:12
so uh this is that we use side project the this is the argument that we get
00:26:19
and if we wish to call the unsaved jack is the fall back we just for
00:26:24
so with the news i that'll just go to it it's clay sighed as a check and
00:26:29
this returns that size which is chip which is checked what would compile time and one time
00:26:37
um okay so this is the largest uh uh
00:26:46
the code that we have and if to create this election check so the children to
00:26:52
selection jacqueline mind the we need to have the checks or even more would be better
00:26:58
we each a each index should be checked against the
00:27:02
browns although a of the size that weren't a size
00:27:07
so this look this is the uh uh eh this is
00:27:10
the index down check so we had index and the side
00:27:15
uh which is in style and that's what we eh and that's what we check
00:27:21
this is the end this can be done again that these
00:27:25
type is useful both the start index and the and the next
00:27:29
so you have the compile times during jack and
00:27:33
a full bowl uh yeah it for both indexes
00:27:39
yeah yeah what we have also is that a check between the vowels
00:27:45
and the check between the boundaries to be to happen at day
00:27:48
implicit because uh there is no intro me not information yet within these
00:27:54
we hear that we know both and and they're both values what their type
00:28:00
that's actually how are so we need a it to wait for the next
00:28:05
block all the statement to check both eh eh both arguments against one another
00:28:12
but again this one is is done like simply to to to the face and this
00:28:18
one done is is the checks yeah so now we have we use the check yeah it
00:28:24
providing the end document and uh start document
00:28:28
and both of them should be a checked against this size
00:28:33
which is that it's the the uh which is known for it
00:28:37
handed me a a here we create the fixed size spectral
00:28:42
after all the jets and we have the relative size eh calculation here
00:28:47
so we have a calculation we should be the end index minus the start with x. plus one and
00:28:53
this is a we add a two phase yeah the l. c. it to be smaller and this is how
00:29:00
everything is done at both compile time and right time
00:29:04
as a fallback both the constraints checking and the calculation
00:29:10
uh yes
00:29:16
the what
00:29:25
oh
00:29:27
why they why they should be used to a lot of no this that the bounce
00:29:32
when you can have the intake starts from zero to to the as minus one yes
00:29:39
so we are close to and then the questions later and
00:29:44
so again you pitfalls and in six diapers
00:29:49
that this is misleading it's got to it doesn't
00:29:51
work like the way you think it should so there's the part that it works well not it
00:29:56
i'm missing and they types if you think about using that data don't exist
00:30:01
if you like it say something but maybe this that won't happen the second one
00:30:07
and if you use to face value is on the right hand side of a comparison side like you probably now
00:30:13
a comparison one word away thing because it's embedded in the any trait
00:30:19
but there is a proposal to implement the university in in equality
00:30:23
yeah with extension as a so that will be a problem in the future if it it's a except that
00:30:29
i was go or who's got three um was in at
00:30:34
the obsolete can remain we need to remove the simple support
00:30:38
we can use object types plus extension that's that's really implement the to place a values instead
00:30:44
of the the product let's that we can general iowa is is that over the no the
00:30:50
well we can generate these other um yeah zero everyone's one argument salons
00:30:54
are we can use any kind yeah yeah we did some market magic
00:30:59
uh we can use in i was tasty reflection replaced michael about that a paradise implementation
00:31:06
but still we don't always do every feature can be supported and we can use union types
00:31:11
for a problem so we can finally have either all or i mean as the upper bound
00:31:18
implosion ah but the question this first roles it's got the bill really you think in
00:31:26
the last maybe no those features that should
00:31:29
be some how easily available in the language itself
00:31:34
conclusions thing about knobs let's get three types more like terms and
00:31:39
in fact uh the rise there one from another and vice versa
00:31:45
a two faces over the bible neighbourhood in line or
00:31:48
hopefully will be some times within the dot the compiler itself
00:31:53
and the future without the looks bites a a
00:31:56
wish to thank k. miles and frank and pow
00:32:00
perhaps because of them without them this one exists then that other continue to those in the knobs
00:32:06
and my work and the and sponsored by the rider twenty twenty legato project thank you all for listening
00:32:20
any any questions listed which is to get to the coffee
00:32:26
oh
00:32:38
okay i i suppose then uh you can ask questions oval coffee and
Conference Program
Keynote: Some Mistakes We Made When Designing Implicits (And Some Things We Got Right)
Martin Odersky, Professor EPFL, Chairman Typesafe
June 14, 2019 · 9:13 a.m.
303 views
Brave New World - tales of PureScript and Haskell in production
Felix Mulder, Snoop Dogg
June 14, 2019 · 10:22 a.m.
151 views
Actors Design Patterns and Arrowised FRP
June 14, 2019 · 10:53 a.m.
Taking Resources to the Type Level
June 14, 2019 · 11:48 a.m.
Lord of the rings: the Spire numerical towers
Denis Rosset, researcher in quantum physics
June 14, 2019 · 1:47 p.m.
Formal verification of Scala programs with Stainless
June 14, 2019 · 2:20 p.m.
118 views
Exploring Scala Tooling ecosystem
Jeferson David Ossa, Colombia
June 14, 2019 · 3:12 p.m.
TwoFace values: a bridge between terms and types
June 14, 2019 · 3:43 p.m.
GADTs in Dotty
June 14, 2019 · 4:41 p.m.
302 views
Closing Remarks
June 14, 2019 · 5:49 p.m.
Recommended talks
Integrating Developer Experiences - Build Server Protocol
Justin Kaeser, IntelliJ Scala
June 12, 2019 · 3:32 p.m.
551 views