Stream: general

Topic: impl Trait = existential?


RalfJ (May 28 2019 at 11:07, on Zulip):

claim: IIRC impl Trait is always an existential type, but in argument position it is isomorphic to a similar universally quantified type

problem: when you start nesting things, like fn foo(fn(impl Trait) -> impl Trait), the "proper" thing you'd expect is that the existentials are like fn foo(fn(exists T: Trait, T) -> (exists T: Trait, T)).

@Centril said this would be isomorphic to exists A: Trait. forall B: Trait. fn foo(fn(A) -> B) but I don't see how, this is totally different? In my function above, the closure can be called with any T!

centril (May 28 2019 at 11:11, on Zulip):

@RalfJ if you have fn foo(fn(exists T: Trait, T) -> (exists T: Trait, T)) then the return type seems to me like dyn Trait

centril (May 28 2019 at 11:12, on Zulip):

i.e. it can vary dynamically

centril (May 28 2019 at 11:12, on Zulip):

when you write something like fn foo() -> impl Alpha, the scoping is exists<A: Alpha> fn foo() -> A

RalfJ (May 28 2019 at 11:13, on Zulip):

that's isomorphic to fn foo() -> exists A: Alpha, A.

RalfJ (May 28 2019 at 11:13, on Zulip):

well okay here this relies on foo having no arguments, in general it'd rely on a restriction for types not to depend on values

RalfJ (May 28 2019 at 11:14, on Zulip):

but either way I don't see how the thing you suggested has anything to do with the type I wrote^^

centril (May 28 2019 at 11:14, on Zulip):

what does your comma notation mean here? is it a sigma type?

RalfJ (May 28 2019 at 11:14, on Zulip):

yeah this is basically Coq syntax

RalfJ (May 28 2019 at 11:15, on Zulip):

except I am ignoring propositional existential vs sigma^^

centril (May 28 2019 at 11:15, on Zulip):

(Coq syntax is so weird ^^)

RalfJ (May 28 2019 at 11:15, on Zulip):

(your syntax is even weirder :P )

RalfJ (May 28 2019 at 11:15, on Zulip):

, just terminates the list of binders. nothing weird. ;)

centril (May 28 2019 at 11:15, on Zulip):

(Idris does a: B *** P(a) -- very nice!)

RalfJ (May 28 2019 at 11:15, on Zulip):

wtf

RalfJ (May 28 2019 at 11:16, on Zulip):

looks like separating conjunction on steroids or so^^

RalfJ (May 28 2019 at 11:16, on Zulip):

or maybe it's the good ol' "** is pow", so this is actually an exponential, as in a product type? :P

centril (May 28 2019 at 11:16, on Zulip):

it's 3 *s

RalfJ (May 28 2019 at 11:17, on Zulip):

even more powerful than pow then^^

centril (May 28 2019 at 11:17, on Zulip):

but I have no idea; you'd have to ask Brady

RalfJ (May 28 2019 at 11:17, on Zulip):

not sure how that's nice, has nothing to do with any syntax I've ever seen. But also shrug whatever.

RalfJ (May 28 2019 at 11:17, on Zulip):

anyway, in exists A: Trait. forall B: Trait. fn foo(fn(A) -> B), foo can call the closure with only one type, namely the witness it took for A. In the one I wrote, interpreted in type theory, you can call the closure with a different argument type each time.

centril (May 28 2019 at 11:17, on Zulip):

well fn foo() -> exists A: Alpha, A seems the same as fn foo() -> dyn Alpha

RalfJ (May 28 2019 at 11:18, on Zulip):

that's like saying fn foo() -> impl Alpha is isomorphic to fn foo() -> dyn Alpha

RalfJ (May 28 2019 at 11:18, on Zulip):

the difference exists only because we have this dynamic-static dichotomy

RalfJ (May 28 2019 at 11:18, on Zulip):

(on the level of abstraction that I am thinking at right now)

centril (May 28 2019 at 11:18, on Zulip):

I think overall it's best to think of impl Trait in terms of type inference + opacity

RalfJ (May 28 2019 at 11:19, on Zulip):

you started mentioning type theory in the other thread, you dont get to change goalposts now^^

RalfJ (May 28 2019 at 11:20, on Zulip):

I was just making a remark where impl Trait is not an existential

centril (May 28 2019 at 11:20, on Zulip):

I didn't say which type theory :P

RalfJ (May 28 2019 at 11:21, on Zulip):

but we don't actually accept impl Trait in nested fn types or traits so I guess this discussion is moot :)

RalfJ (May 28 2019 at 11:21, on Zulip):

it seems like everywhere that we accept impl Trait, it is (isomorphic to) an existential. So beauty is restored. :)

centril (May 28 2019 at 11:21, on Zulip):

when I think of fn foo() -> impl Bar in terms of existentials, the existential binder is at the module level

RalfJ (May 28 2019 at 11:22, on Zulip):

hm. interesting. not how I think about them.^^

centril (May 28 2019 at 11:23, on Zulip):

if we do have something akin to fn foo(_: impl Fn() -> impl Bar) it does get tricky tho... if we put the existential for Bar at the module level it is very surprising

centril (May 28 2019 at 11:24, on Zulip):

instead: fn foo(_: exists<F: Fn() -> impl Bar> F) -- but we haven't made much progress

centril (May 28 2019 at 11:25, on Zulip):

presumably, what the user is trying to say is: fn foo(_: exists<F: Fn<(), Output: Bar>> F)

centril (May 28 2019 at 11:26, on Zulip):

which is representable. but I'm also not sure if that's what it should mean

Last update: Nov 20 2019 at 13:50UTC