Stream: wg-traits

Topic: intersection type


varkor (Apr 23 2019 at 16:31, on Zulip):

the idea is "some value is both T1 and T2 simultaneously"

what property does it have that isn't satisfied by a product? i.e. if typeof(x) = T1 && T2 and typeof( (t1, t2) ) = T1 x T2, what would we expect to be true of x that we don't get by doing something on t1 or t2 separately?

nikomatsakis (Apr 23 2019 at 16:32, on Zulip):

Maybe I am confused -- a product (T1, T2) is the combination of a T1 and T2 value (and you can project out those independent things). But importantly any T1 and T2 value can be combined.

varkor (Apr 23 2019 at 16:32, on Zulip):

or maybe another way to ask my question is: why should dyn (Foo + Bar) be modelled by dyn Foo && dyn Bar, where && has the obvious trait bound criteria, rather than dyn (Foo + Bar) directly having the obvious bound criteria?

nikomatsakis (Apr 23 2019 at 16:32, on Zulip):

An intersection is a single value that is both

varkor (Apr 23 2019 at 16:33, on Zulip):

i.e. dyn (trait bound) : trait bound.

varkor (Apr 23 2019 at 16:33, on Zulip):

that is, dyn is parameterised by a bound, rather than by a list of traits

varkor (Apr 23 2019 at 16:35, on Zulip):

An intersection is a single value that is both

ah, so an intersection type here is a product without projections

nikomatsakis (Apr 23 2019 at 16:35, on Zulip):

it's not clear that what I am thinking makes sense, but my reasoning was that I wanted to avoid quantifying over something that is not types. That said, I think that it may work out fine to support dyn Bound1 + Bound2 directly, and to lower that in chalk's "program clause" callback to

varkor (Apr 23 2019 at 16:36, on Zulip):

I think it's very possible it'll be necessary to parameterise over bounds at some point in the future regardless (e.g. any of the various "constraint kinds" proposals)

centril (Apr 23 2019 at 16:36, on Zulip):

that is, dyn is parameterised by a bound, rather than by a list of traits

To that point, the way I would model dyn Trait in Haskell is:

data Dyn (c :: Type -> Constraint) = forall (t :: Type). (c t) => D t
nikomatsakis (Apr 23 2019 at 16:37, on Zulip):

I think it's very possible it'll be necessary to parameterise over bounds at some point in the future regardless (e.g. any of the various "constraint kinds" proposals)

plausible, but I would rather not

nikomatsakis (Apr 23 2019 at 16:37, on Zulip):

well, that's strong

nikomatsakis (Apr 23 2019 at 16:37, on Zulip):

but I would rather not go there if we don't have to

nikomatsakis (Apr 23 2019 at 16:37, on Zulip):

that said, I don't think we have to quantify over predicates in any case

nikomatsakis (Apr 23 2019 at 16:38, on Zulip):

in either scheme

nikomatsakis (Apr 23 2019 at 16:38, on Zulip):

as this logic would be "internal" to the callback, and implemented in Rust

varkor (Apr 23 2019 at 16:38, on Zulip):

ah, so an intersection type here is a product without projections

sorry, this is a confusing way of putting it — I essentially mean that we have the following introduction rule (and the obvious formation rule):
a: A, b: B ==> a&b : A && B
but no elimination (or computation) rules

nikomatsakis (Apr 23 2019 at 16:38, on Zulip):

but I would rather not go there if we don't have to

(though it's worth nothing that Lambda Calculus generally permits one to quantify over predicates)

varkor (Apr 23 2019 at 16:39, on Zulip):

but no elimination (or computation) rules

which is equivalent to a product type without projections

centril (Apr 23 2019 at 16:40, on Zulip):

but I would rather not go there if we don't have to

Having dyn Self::MyBound work is definitely something that I'm interested in exploring as part of -XConstraintKinds in Rust (associated traits, trait generics, ...)

varkor (Apr 23 2019 at 16:40, on Zulip):

but I would rather not go there if we don't have to

it's fairly tangential anyway
I just think that parameterisation over bounds is going to lead to a simpler (conceptual) model

varkor (Apr 23 2019 at 16:41, on Zulip):

(of course, I'm saying this without having tried to implement anything, so there are a lot of handfuls of salt to be taken here :grinning_face_with_smiling_eyes:)

varkor (Apr 23 2019 at 16:48, on Zulip):

pasted image

varkor (Apr 23 2019 at 16:48, on Zulip):

(I think this is the definition of an intersection type)

varkor (Apr 23 2019 at 16:50, on Zulip):

(namely, if an a: A satisfies some property p and b: Bsatisfies some property q, then there exists some object f(a, b): A & B such that f(a, b) satisfies both p and q)

nikomatsakis (Apr 23 2019 at 16:53, on Zulip):

I just think that parameterisation over bounds is going to lead to a simpler (conceptual) model

having thought it over, I think I agree

centril (Apr 23 2019 at 16:57, on Zulip):

@varkor that looks similar to the diagram for a product; i.e. set p, p', q', q = id

varkor (Apr 23 2019 at 16:59, on Zulip):

@centril: if you replace the two Ωs by A and B, then you get a product — but here Ω is an "object of truth values" (in Rust's case, this would just be bool)

varkor (Apr 23 2019 at 16:59, on Zulip):

the difference being that with an intersection type, you want to preserve the values of propositions, but you don't want to be able to project

varkor (Apr 23 2019 at 17:00, on Zulip):

(Ω here is known as a subobject classifier)

varkor (Apr 23 2019 at 17:00, on Zulip):

(this is really just a modification of the definition of a pullback over the subobject classifier in a topos)

centril (Apr 23 2019 at 17:00, on Zulip):

@varkor so you are using truncation?

varkor (Apr 23 2019 at 17:02, on Zulip):

truncations aren't really relevant here, because there's no identity type / higher dimensionality

varkor (Apr 23 2019 at 17:03, on Zulip):

edit: I'll rephrase

centril (Apr 23 2019 at 17:03, on Zulip):

@varkor here's where my category theory-fuu falls short ;)

centril (Apr 23 2019 at 17:08, on Zulip):

you want to preserve the values of propositions, but you don't want to be able to project

@varkor but this reminded me of Type & Prop ; i.e. we want to erase the witness and have proof irrelevance

varkor (Apr 23 2019 at 17:09, on Zulip):

I'll explain a bit more intuitively

varkor (Apr 23 2019 at 17:09, on Zulip):

pasted image

varkor (Apr 23 2019 at 17:09, on Zulip):

this is a typical product type (in context Gamma)

centril (Apr 23 2019 at 17:10, on Zulip):

sure

varkor (Apr 23 2019 at 17:10, on Zulip):

it's trivially the same as this diagram:

varkor (Apr 23 2019 at 17:10, on Zulip):

pasted image

varkor (Apr 23 2019 at 17:10, on Zulip):

because you can take A = A' and B = B'

varkor (Apr 23 2019 at 17:11, on Zulip):

however, if we don't let A' and B' be arbitrary, this is no longer as general as a product type, because you have "projections" only to the specified types A' and B'

varkor (Apr 23 2019 at 17:11, on Zulip):

in particular, if we take A' = B' = Bool, then we get this

varkor (Apr 23 2019 at 17:11, on Zulip):

pasted image

varkor (Apr 23 2019 at 17:12, on Zulip):

(well, the A x B in the middle should be something else, e.g. A & B)

varkor (Apr 23 2019 at 17:12, on Zulip):

here, our "projections" are only permitted to bool

varkor (Apr 23 2019 at 17:12, on Zulip):

i.e. the projections are just functions to bool, or propositions

varkor (Apr 23 2019 at 17:13, on Zulip):

so this means that the type A & B satisfies the same propositions as A and B separately, but you can't project

varkor (Apr 23 2019 at 17:13, on Zulip):

(we can obviously convert any product type into an intersection type)

varkor (Apr 23 2019 at 17:14, on Zulip):

(the type bool is known as a subobject classifier in a topos)

varkor (Apr 23 2019 at 17:14, on Zulip):

(but that's not important :) )

varkor (Apr 23 2019 at 17:15, on Zulip):

(it looks a little like a pullback type, but it's not as general)

varkor (Apr 23 2019 at 17:15, on Zulip):

so now we can define an "intersection type" in any category

centril (Apr 23 2019 at 17:17, on Zulip):

@varkor so we can get an intersection type by taking the usual product type but leave out the projections?

varkor (Apr 23 2019 at 17:19, on Zulip):

you need these extra functions to bool, I think — otherwise the type isn't really an "intersection"

varkor (Apr 23 2019 at 17:19, on Zulip):

it's just some type that's guaranteed to exist

varkor (Apr 23 2019 at 17:28, on Zulip):

(the confusing thing about the nomenclature here is that this definition does not give the usual notion of intersection of sets)

Last update: Nov 18 2019 at 01:30UTC