►
From YouTube: Polonius WG: The role of subset relations
Description
A discussion about the role of subset relations in Polonius's design and a proposal to propagate not the full subset relation but only equality.
Paper document:
https://paper.dropbox.com/doc/Polonius-and-subset-propagation--AemU19yUmQ461DupzxgaCj2NAg-2uMIPkQSbqpPjqrJ9L9DM
A
A
There
must
be
a
simplified
version
of
this,
we'll
start
with
this.
So,
first
of
all,
let's
look
at
back
projection.
So
what
what
one
of
the
times
I
were
to
start
when
we
do
the
like
one
of
the
key
things
in
the
polonius
some
design
so
to
speak,
was
that
the
first
starting
point
we
just
have
fresh
regions
everywhere.
We
just
kind
of
give
up
just
going
to
give
them
unique
names
for
all
the
places
and
they
have
no
protect
no
connection
to
one
another
necessarily
and.
A
The
problem
is
this:
doesn't
or
I'll
show
you
in
this
example.
If
you're,
not
if
you're,
not
careful,
like
sometimes
connections
between
regions
have
to
propagate
across
control
points,
or
else
it
becomes
unsound
and
here's.
This
is
an
example
where
that
would
be
the
case
and
by
the
way,
lqt
well
you'll
see.
This
is
relevant
to
what
you
wrote.
Just
sorry,
a
good
question:
are
you
sharing
your
screen
right
now.
A
A
Something
like
this
right,
so
you
have
a
vector,
you
have
a
local
variable.
You
push
a
reference
to
the
local
variable
into
the
vector
and
you
try
to
mutate.
The
local
variable
and
the
idea
is
this
should
be
an
error
because
we
still
have
a
shared
reference
to
it.
So
it's
not
allowed
to
change
at
that
time
right,
because
this
is
a
use
one.
This
drop
here
is
just
a
call
to
the
drop
function,
so
it's
a
use
of
the
vector
from
our
point
of
view.
A
Okay,
stop
me
if
that
doesn't
make
sense,
I'm
going
to
assume
that
does
so,
then,
if
you
sort
of
do
sugar
vector
push,
you'll
see
it.
What
actually
happens
is
that
we
make
a
mutable
reference
to
the
vector
and
we
call
Veck
push
on
this
mutable
reference,
and
so,
if
we
dig
in
a
little
bit
more
into
the
types
of
what's
going
on
here
from
Polonius's
point
of
view,
then
you
have.
This
initial
vector
has
a
type
ampersand.
U
32
or
back
of
ampersand
you
32,
and
this
variable
P
is
a
mutable
reference.
A
With
there's,
actually
two
regions
involved:
I'm,
not
gonna.
This
one
doesn't
matter
so
I'm
gonna
leave
it
as
underscore,
but
it's
a
mutable
reference
which
has
some
region
to
a
vector,
and
then
this
this
region
appears
here
right,
and
so
what
could
go
wrong
if
you're,
not
careful
is
actually
that's,
add
one
more
thing.
A
A
Right
so
what
happens
when
we
check
this?
This
is
a
loan,
we'll
call
this
the
loan
l0,
and
let's
give
this
a
name
and
so
there's.
We
know
that
kind
of
l0
is
how
do
I
normally
write
this
take
see.
We
know
that
this
this
loan,
just
because
we
saw
the
blue
region
itself,
is
part
of
tixi
right
I'm,
mildly.
Simplifying
though
this
actually
works,
there's
actually
another
region
involved,
but
that's
the
idea
and
then
here
when
we
call
Veck
push.
A
So
this
importantly
at
this
point,
like
the
reference
is
not
yet
in
the
vector,
so
there's
the
only
place
that
the
loan
appears
as
as
part
of
this
tixi
region,
and
when
we
call
back
push
there
are
some.
The
typing
relations
will
kind
of
have
some
effect
here.
So
the
signature
of
push
is
something
like
and
mute
back
of,
te
t
is
to
say
it
takes
a
reference
to
a
vector
of
type
T
and
I
T.
In
this
case
the
T.
A
It's
gonna
be
sort
of
an
%
ik
d.
U
32
for
some
new
D,
and
so
we're
gonna
get
some
relation
which
is
like
this
region.
C
flows
into
D
d
f--,
because
the
T
is
shared
here
and
because
the
way
mutable
invariance
works,
tick
D
is
gonna
flow
into
the
and
vice
versa,
so
essentially
tick
T
equals
to
B.
If
we
simplify
this
and
get
rid
this
whole
D
thing
here
essentially
left
this.
A
So
what
we're
saying
is
somewhat
simplified
when
you
call
that
push
the
lone
l0
will
flow
from
C
into
B.
So
at
this
point
we
know
that
I
forget
how
what
do
we
call
this
relation
and
felonious
contains
America
contains
rule
requires
requires
a
change
that
I'll
still
contact
for
now,
so
we'll
kind
of
know
both
of
these
things,
and
that
means
now.
A
Okay,
but
now
this
is
where
it
gets
interesting,
because
now
we
don't
have
Tim
zero
and
temp.1
kind
of
go
out
of
scope
and
are
dead,
and
that
means
that
the
regions
in
their
types
are
also
dead,
B
and
C.
So
if
we
did
nothing
else,
but
what
I'm
showing
you
that
would
kind
of,
we
have
a
problem
now,
because
we
want
to
make
an
error
here
and
we
need
l0
to
be
in
scope.
A
The
only
live
region
is
today
and
if
you
notice,
we
didn't
even
talk
about
today
here
at
any
point,
that's
because
we
were
all
concerned
with
the
regions
that
occurred
in
this
in
this
reference,
but
we
didn't
think
about
there's
a
connection
between
the
type
of
the
reference
and
the
type
of
the
thing.
The
reference
refers
to
the
referent
and.
A
Let's
just
say,
it's
on
well
I'm,
not
gonna,
go
into
this
super
depth
of
how
this
all
plays
out
in
type
system,
but
the
short
version
is
that
the
type
of
the
thing
you
borrowed
the
vector
winds
up
being
equated
with
this
type.
They
have
to
be
equal,
so
you
wind
up
with
tae,
equals
you
end
up
with
this
subset,
to
gate,
to
be
and
subset
to
be
to
K,
which
is
equality
in
our
terms.
A
So
you
know
to
get
all
this
or
those
entities
this
way,
and
so
that's
where
this
subset
propagation
stuff
comes
in,
because
in
the
normal
Polonius
we
flow
these
things
forward,
and
then
we
have
down
here.
We
not
only
know
that
to
see
our
lipstick
B,
but
we
know
that
today,
L
lives
or
that's
a
hard
hard
habit
to
break
I,
don't
like
to
say
how
it
lives:
ticket
flows
into
2b
and
2b
flows
into
K,
so
they're,
essentially
equal,
which
means
we
get
a
requires
zero
to
get
here.
A
A
So
that's
how
that's
why
this
subset
propagation
is
kind
of
there
in
the
first
place
and
I
think
like
when
I
saw
a
long
time
ago.
Just
said:
oh
I
forgot:
why
do
we
even
have
substitution
and
then
Matthew
Jasper,
if
I
recall
so
I,
didn't
example
much
like
this
one?
That
was
exactly
why
that
proposal
was
totally
wrong.
That
makes
sense
yep
so
in
your
write-up
or
that
the
vet
push
raff
example.
Itself
is
just
like
a
mild
variation
on
this,
and
in
your
write-up
Okita,
you
said
there
are
no
mutable
references.
A
Basically,
you
introduced
a
branch,
and
you
say
you
only
want
it
this
size
in
this
when
you
get
here,
you're
dropping
the
vector,
but
in
this
side
of
the
branch
the
vector
never
comes
into
contact
with
this
loan.
Actually,
the
loan
can
be
even
out
here,
so
the
loan
is
created
in
both
branches,
but
it
never
gets
added
to
the
vector
in
one
side
and
we
would
like
to
make
sure
we
know
that
and
if
you
work
out
the
way
this
relation
thing
works.
A
A
The
subset
propagation
says
that
sub
type
has
to
keep
last
has
to
continue
forever.
Essentially,
but
sometimes
you
only
need
an
instantaneous
sub
type.
So
if
you
think
of
the
regions
as
sets
of
loans
or
the
provenances
I
guess
for
changing
my
terminology,
which
I'm
not
going
to
do
mid
call,
then
you
only
need
the
subset
relationship
to
hold
at
that
moment
and
that's
more
in
this
example,
where
we
have
two
variable
yeah
variables,
x
and
y,
and
we
copy
one
into
the
other
sometimes.
A
But
in
that
case
like
at
the
moment
in
which
we
do
the
copy,
whatever
X
might
point
out
at
that
time.
Y
can
now
point
out,
but
if
we
make
X
point
at
something
in
the
future,
y
still
will
never
point
at
that
right.
But
if,
but
that's
not,
what
blowing
is
things
because
blueness
creates
the
subset
relation
saying
that
these
regions
have
a
relationship
to
one
another
and
it
carries
it
forward.
So
at
this
point
it
still
believes
that
they're
related
to
one
another.
So
when
we
add
something
into
X,
we
wind
up.
A
A
Here
I
kind
of
said
that
these
have
different
letters.
The
type
of
vector
is
too
gay
and
the
type
of
temp
0
was
to
be,
but
we
kind
of
added
it
to
get
equals
to
be
relation.
But
what?
If
we
kind
of
pushed
that
earlier
and
said
for
this
to
be
well
typed,
they
have
to
actually
be
the
same
letter
in
the
first
place,
the
same
region.
A
A
Shows
that
problem,
where
it's
kind
of
complicated,
but
you
essentially
what
happens,
is
you
you
create
an
equality
in
one
branch
and
you
different
equality
and
the
other
branch.
So
here
we
have,
the
P
has
to
equal
the
type
the
type
of
this
has
to
equal
a
and
here
we
have
that
has
to
equal
B
and
because
equality
is
if
we
say
that
that's
just
true
across
the
entire
graph,
because
equality
is
transitive.
A
That
means
that
a
and
B
also
have
to
be
equal,
which
means
we've
lost
track
of
the
fact
that
these
are
two
different
vectors.
Essentially
so
now,
if
I
push
into
one
of
them
like
a
and
then
I
dropped,
the
B
you
know
or
if
I
push
into
a
I'll,
also
assume
that
that
region
lives
in
B
and
so
I
get
an
error
on
one
of
these
two
lines
or
both
I
guess
actually,
so
it
would
be
kind
of
nicer
if
we
said
well,
it's
only
equal.
A
The
only
has
to
be
equal
starting
at
this
point
essentially
before
then
it's
not
true
and
I
guess,
there's
another
other
I
think
about
it,
there's
probably
a
simpler
example.
There
would
leverage
that
similar
to
vector
stress
like,
in
other
words,
we're
also
saying
I,
didn't
even
use.
C
I
just
put
it
in
here
to
have
some
initial
value,
but
but
actually
we're
equated
C
all
because
they're
all
sort
of
going
through
P.
So
we
can
probably
do
something
focus.
A
A
B
A
I
couldn't
tell
if
it
was
no
or
I
hesitate.
Okay,
let's
look
at
47
680,
though
cuz
I
think
I
found
a
problem
just
five
minutes
ago.
That
I
thought
was
kind
of
interesting
and
surprising
to
me.
So
actually,
if
you
actually
looked
at
47,
680
you'll
see
that
there's
a
whole
bunch
of
examples
here,
some
of
them
which
are
quite
complicated
but
the
one
that
I
like
is
this
one.
A
So
this
is
my
sort
of
preferred
form
it's
kind
of
a
nonsense
program,
but
that's
okay,
Kumiko
into
infinite
loop,
but
what's
happening
is
you've,
got
some
linked
list
or
something,
and
you
have
as
loop
and
you're
saying.
If
there's
a
next
pointer,
I
want
to
move
temp
forward.
Otherwise
I
do
nothing
and
that
seems
like
it
should
be
allowed.
But
what
ends
up
happening
with
nll
today
is
you're
getting
error
and
the
reason
is
that
the
reason
is
kind
of
complicated,
because
we
have
some
logic.
A
A
A
A
Here
I
have
a
mutable
reference
to
something
and
then
I
I
borrowed
it
into
are
essentially
I
borrowed.
What
it
points
out
is
hurry
borrowed
it,
and
the
point
is
that
in
this
period,
I
can't
use
q
because
it's
we
borrowed
through
our.
But
if
I
overwrite
q
is
something
else
now,
I
can
write
and
that
should
be
okay
and
the
way
that
we
figure.
That
is
that
we
create
a
loan,
let's
call
it
l0
here
and
that
that's
a
loan
of
star
Q
and
that
loan
is
in
scope
because
R
is
life.
A
A
If
you
had
done
as
I
say,
this
would
be
a
different
name
now
q1,
but
that's
what
the
killing
does
and
it's
important
here,
because
when
you
call
maybe
next
you're
borrowing,
temp
and
then
you're
taking
the
result
of
that
borrow
V
and
you
are
making
it
live
across
the
loop.
So
the
borrow
of
temp
is
is
still
life.
When
you
come
around
the
loop,
the
only
thing
is
tap
that
out
points
at
something
else,
so
we
don't
we
kind
of
lose
track
of
that
in
the
current
NLL.
A
A
We
have
two
separate
things:
one
is
tracking
the
control
flow
and
seeing
that
we're
going
to
go
back
around
the
loop
and
the
other
is
I'm
doing
the
kills,
and
we
don't
see
that
in
the
control
flow
or
II
see
what
there's
one
path
where
temp
does
not
get
modified
and
there's
one
path
where
it
does,
but
we
don't
see
that
in
the
path
where
it
does
is
also
the
one
where
the
subset
occurs.
That's
the
thing:
the
data
only
flows
into
it.
If
it's
also
going
to
get
modified,
we
can't
check
for
that
weed.
B
A
A
A
When
you
re,
borrow
cue
whe,
when
you
borrow
the
restaurant
of
cue,
we
introduce
a
relation
that
says
that
a
a
flows
into
B
and
the
reason
is,
if
you
think
about
it,
it
must
like
the
only
reason
that
this
this
reference
R,
is
only
usable
because,
like
the
data
it's
pointing
at
is
this
X,
which
is
the
same
X.
That
Q
is
pointing
at
so
whatever
loans
sort
of
secure,
X
also
secured
be
right.
A
A
B
B
A
Okay,
well,
maybe
there's
no
sound
as
well,
which
is
good,
but
if
there
is,
it
has
something
to
do
with
the
fact
that
this
should
be
persistent
and
if
I
can
think
of
it
either.
While
we're
talking
when
they
hear
all
decide,
I
was
gonna
just
sort
of
play
through
how
this
example
works
out.
I
guess
I
might,
unless.
A
This
is,
like
a
mildly,
simplified
control
photograph
for
what
happens
up
here,
a
particular
I
kind
of
delighted.
The
whole
matching
just
made
it
a
whole
option.
Logic
essentially
goes
away,
but
it's
not
really
relevant.
So
it's
more
like
is
this.
Maybe
next
return
the
same
thing
it
was
given
and
randomly
picked
to
assign
or
not
a
sign,
but
you
got
right,
so
you
start
out
with
this
variable
temp
and
then
in
the
head
of
the
loop,
be
one
you
borrow
from
temp
call,
maybe
next
with
that.
A
A
A
There's
something
missing:
oh
right,
there's
this!
This
is
correct
because
we
borrowed
star
temp.
So
we
have
that
relationship
between
the
mutable
reference
that
we
D
referenced.
It
says
he
is
dependent
on
all
the
things
today
is
dependent
on
to
a
thousand
B,
so
we
get
down
to
here.
We
kind
of
we
have
here.
We
know
that
transitively
took
a
LSD,
be
in
today
autistic
C,
so
we
kind
of
know
both
of
those
things
here,
but
we
kill
L
zero,
so
we
had
until
until
we
killed
it.
A
A
A
A
B
A
B
The
I
think
the
main
difference
that
I'm
thinking
about
right
now,
because
the
question
that
I
asked
is
that
I
recently,
maybe
a
couple
weeks
ago,
did
a
change
such
that
loans
can
only
be
for
sort
of
placed
values.
So
I
made
like
a
value
expression
distinction
where
police
expressions
can
contain
dereferencing
and
place
values
cannot,
and
you
can
only
have
loans
for
placed
values
which
now
that
I'm
seeing
some
of
this
stuff
I'm,
not
so
sure.
B
B
A
The
answer
Polonius
is
no
place
today,
because
there's
also
these
subset
relationships
and
they're
important,
if
you
just
replaced
it
with
the
set
of
loans,
you
would
lose
the
connection
between
temps
euro
and
vector
and
that's
exactly
why
we
were
saying
well,
maybe
if
you
just
required
them
to
be
the
same
name,
but
then
you
could,
which
would
be
this
stricter
rule,
but
now
I'm
not
sure
what
the
answer
is
around
this.
If
we
do
the
sort
of
location,
dependent
equality
and
they
aren't
I,
didn't
quite
understand
your
response
actually
about
how
that
would
work.
B
There's
no
question
of
is
sort
of
at
the
end
of
each
branch
we
try
to
unify
the
information.
We
have
to
get
like
a
conservative
bound
on
how
what's
allowed
and
the
remainder
of
the
program,
but
because
we
drop
both
and
B
before
the
end
of
each
branch.
There's
nothing
it.
It
knows
that
it
doesn't
need
to
unify
this.
Those
pieces
of
information,
yeah.
A
So
the
key
thing
here
is:
you
can
replace
them.
If
I
can
restate
what
you
said,
you
can
replace
the
regions
with,
or
the
provenances
or
whatever,
with
the
set
of
loans,
but
the
variables
don't
have
a
single
type
they're,
the
type
that's
changing
across
yes
flow
and
so
a
strong
update
which,
for
those
from
and
the
parents
protector
means
changing
the
type
of
a
variable,
basically
we're
gonna
kind
of
up
change,
the
type
of
a
and
P
here
and
change
the
type
of
B
and
P
here
to
be
equal.
A
B
A
B
A
B
A
You
could
pick
fresh
names,
you
know
where,
for
things
that
are
equal,
they
have
the
same
name
and
then
replace
those
names
with
the
sets
of
loans,
and
it
should
be
fine
if
you
haven't
really
lost
any
information.
I
think
that
seems
correct.
That's
just
true!
You
keep
the
Equality
information,
because
now
you
have
the
same
name
and
you
keep
the
roll
one
once
they
have
the
same
name.
They'll
have
the
same
value
forever.
I.
B
Think
something
interesting
to
note
about
that,
like
strong,
update,
part
like
type
updating,
is
that
actually
I
think
the
types
never
it's
kind
of
weird
that
the
types
themselves
don't
actually
change
anymore
in
oxide?
What
happens
is
that
the
types
which
all
contain
these
like
provenance
vary
in
the
same
way
that
you
know
Nikko
has
been
writing
them
everywhere.
B
It's
like
to
gaze
and
take
these
whatever
those,
what
the
meaning
of
those
ticka
isn't
take
these
changes,
because
the
the
set
of
loans
and
them
grows
or
shrinks
as
things
flow
through
the
control
flow
graph.
So
it's
sort
of
like
the
interpretation
of
the
type
changes,
but
the
type
syntactically
remains
the
same.
Yes,.
A
A
That,
if
that's
true
I,
don't
quite
know
how
the
strong
update
story
plays
out
like
if
a
and
B
start
out
with
distinct
types,
and
they
have
to
wind
up
with
the
same
equal
types.
When
the
control
flow
converges
again,
then
it
seems
like
you,
either
need
to
keep
the
relationship
between
a
and
B
somewhere
or
change.
The
letters.
B
If
a
and
B
are
the
provenance
variables
on
a
and
B,
then
they
shouldn't
need
to
because
they're
disjoint
right,
like
I,
mean
they're
disjoint
in
the
program
like
it's,
it's
P,
that's
gonna
need
like
the
one
in
P
yeah,
that's
going
to
need
to
contain
in
the
true
side
of
the
branch,
all
the
things
in
Takai
and
the
false
side
of
the
branch.
All
the
things
in
tick
be.
A
A
A
B
A
B
A
A
B
A
B
A
This
is
basically
the
same
example
is
great
beginning
I
guess
I'm
trying
to
say
is:
if
they're,
not
forests
are
literally
the
same
letter,
then
I
don't
know
how
this
information
propagates.
If
they
are
a
force
to
have
this
letter,
then
it
seems
fine,
but
then
they
have.
It
adhere
like
a
and
B
have
to
be
equal.
Somehow
right.
So
something
has
to
used.