Stream: general

Topic: object safety phrasing


Jake Goulding (Apr 27 2019 at 14:38, on Zulip):

Is it accurate to say that the fundamental reason that a given trait cannot be made into an object is because it's not possible to construct / select the vtable at that point in time?

Jake Goulding (Apr 27 2019 at 14:40, on Zulip):

There's also the unsized aspect, which I know is being worked on via unsized rvalues, so I'm ignoring that when i state "fundamental"

centril (Apr 27 2019 at 15:31, on Zulip):

@eddyb ^--- would "type erasure safe" have been a better phrasing?

eddyb (Apr 27 2019 at 15:31, on Zulip):

hmpf

eddyb (Apr 27 2019 at 15:31, on Zulip):

not exactly

centril (Apr 27 2019 at 15:31, on Zulip):

(explaining why e.g. for<T> fn(T) and dyn for<T> Fn(T) ain't OK)

eddyb (Apr 27 2019 at 15:32, on Zulip):

@Jake Goulding so if we're only taking the "no generic methods" problem

eddyb (Apr 27 2019 at 15:32, on Zulip):

it's the possibility of reification of the vtable at all

eddyb (Apr 27 2019 at 15:33, on Zulip):

with non-generic functions, you have a finite number of fn pointers, and that's enough

eddyb (Apr 27 2019 at 15:33, on Zulip):

to do dynamic dispatch

eddyb (Apr 27 2019 at 15:33, on Zulip):

@centril eh, I think that assumes too much

centril (Apr 27 2019 at 15:33, on Zulip):

(deleted)

eddyb (Apr 27 2019 at 15:33, on Zulip):

sorry, Zulip is annoying, UI-wise

centril (Apr 27 2019 at 15:34, on Zulip):

(deleted)

nagisa (Apr 27 2019 at 15:35, on Zulip):

You can by clicking a v that is visible on the left I tihnk, but only within 10 minutes of writing the message. Or maybe not.

centril (Apr 27 2019 at 15:35, on Zulip):

doesn't seem so

eddyb (Apr 27 2019 at 15:36, on Zulip):

it's on the right

centril (Apr 27 2019 at 15:36, on Zulip):

with non-generic functions, you have a finite number of fn pointers, and that's enough

(Treating lifetime generic functions as non-generic due to parametricity)

Jake Goulding (Apr 27 2019 at 15:39, on Zulip):

@eddyb is it correct that there's only the two categories feeding into object safety today: generics and unsized? Make sure I'm not missing an avenue

Matthew Jasper (Apr 27 2019 at 15:40, on Zulip):

The second is being able to implement Trait for dyn Trait (which implies the stuff around Sized if you treat std::mem::swap as an honorary method of Sized).

Jake Goulding (Apr 27 2019 at 15:42, on Zulip):

@Matthew Jasper I'm not seeing the connection with swap here... could you expand a smidge?

Matthew Jasper (Apr 27 2019 at 15:45, on Zulip):

The signature of swap is (effectively) fn swap(&mut self, other: &mut Self), which isn't object safe because the second parameter references Self.

Matthew Jasper (Apr 27 2019 at 15:47, on Zulip):

And such signatures aren't object safe because there's no way to "glue together" all of the individual implementations into one for dyn Sized

Matthew Jasper (Apr 27 2019 at 15:48, on Zulip):

No matter how we implemented trait objects

eddyb (Apr 27 2019 at 16:34, on Zulip):

uhhhhhhhh

eddyb (Apr 27 2019 at 16:34, on Zulip):

a swap method is perfectly fine

eddyb (Apr 27 2019 at 16:34, on Zulip):

we're just not implementing dyn Trait fully today

eddyb (Apr 27 2019 at 16:34, on Zulip):

you could use it, in the future, for something like &mut [dyn Trait]

eddyb (Apr 27 2019 at 16:35, on Zulip):

since that's &mut [T] for an unknown T

eddyb (Apr 27 2019 at 16:35, on Zulip):

@centril okay fine I mean "only erasable generics". which is I guess what your point was

Matthew Jasper (Apr 27 2019 at 16:36, on Zulip):

What would swap even do with two different types?

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

@eddyb yep

eddyb (Apr 27 2019 at 16:36, on Zulip):

@Matthew Jasper it would require same-type

eddyb (Apr 27 2019 at 16:36, on Zulip):

which... is a thing you can statically typecheck and lots of formalisms have had for like... half a century even?

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

we should consider dyn for<T: ?Concrete> Fn(T) or something

eddyb (Apr 27 2019 at 16:36, on Zulip):

what

centril (Apr 27 2019 at 16:37, on Zulip):

@eddyb ?

eddyb (Apr 27 2019 at 16:38, on Zulip):

anyway, like I said, [dyn Trait], by the only rules that are known to work, must come from a [T; n] where T: Sized and n: usize

eddyb (Apr 27 2019 at 16:38, on Zulip):

the element type can't vary between elements

eddyb (Apr 27 2019 at 16:38, on Zulip):

that would mean that you'd end up with the same skolem variable when accessing elements

eddyb (Apr 27 2019 at 16:39, on Zulip):

so e.g. a [ref mut a, ref mut b, ..] pattern would know that a and b are not only dyn Trait, but the same concrete type

eddyb (Apr 27 2019 at 16:39, on Zulip):

and so you could swap them!

centril (Apr 27 2019 at 16:39, on Zulip):

@eddyb same story for Vec<dyn Trait> presumably?

eddyb (Apr 27 2019 at 16:39, on Zulip):

yupp

eddyb (Apr 27 2019 at 16:39, on Zulip):

that's just a growable Box<[dyn Trait]>

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

:ship:

eddyb (Apr 27 2019 at 16:40, on Zulip):

(not swap them with mem::swap, that'd be harder, but with a swap method)

eddyb (Apr 27 2019 at 16:40, on Zulip):

Zulip makes it tedious to correct typos, lol

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

/me checks what the equivalent of Vec<dyn Trait> is in Haskell

eddyb (Apr 27 2019 at 16:41, on Zulip):

it probably involves the keyword forall because gotta love Haskell

centril (Apr 27 2019 at 16:41, on Zulip):

yup

eddyb (Apr 27 2019 at 16:41, on Zulip):

but, basically, you just put the binder outside the []

eddyb (Apr 27 2019 at 16:42, on Zulip):

if you put it inside, that's like Vec<Box<dyn Trait>>

eddyb (Apr 27 2019 at 16:42, on Zulip):

Rust has implicit binder slots in *const, *mut, & and &mut and nothing else

eddyb (Apr 27 2019 at 16:43, on Zulip):

I keep meaning to write this up instead of ranting about it once it a while

eddyb (Apr 27 2019 at 16:43, on Zulip):

it fits together pretty well

centril (Apr 27 2019 at 16:43, on Zulip):

please do

centril (Apr 27 2019 at 16:46, on Zulip):
<interactive>:11:5: error:
    * My brain just exploded
      I can't handle pattern bindings for existential or GADT data constructors.
      Instead, use a case-expression, or do-notation, to unpack the constructor.
centril (Apr 27 2019 at 16:51, on Zulip):

@eddyb

{-# LANGUAGE ExistentialQuantification, RankNTypes, ConstraintKinds, KindSignatures #-}

import Data.Kind

data DynList (c :: * -> Constraint) = forall (t :: *). c t => DL [t]

main = print $ case DL [0, 1, 2 ] :: DynList Show of DL xs -> show <$> xs
centril (Apr 27 2019 at 16:54, on Zulip):

https://github.com/goldfirere/singletons/pull/228 :joy:

centril (Apr 27 2019 at 16:55, on Zulip):

@eddyb seems perfectly reasonable to me

Last update: Nov 20 2019 at 11:55UTC