path-dependent types in Scala

empanada linguist @jco

@travisbrown any ideas? stackoverflow.com/questions/3357…

good tweet eric @goodtweeteric

@jco @travisbrown trait Thing[Out]?

Gabriel Claramunt @gclaramunt

@jco @travisbrown def hey(t: Thing): Thing#Out = Wrapper(t).get compiles, but have't checked if that's the fix :)

Travis Brown @travisbrown

@gclaramunt That doesn't give you a useful static type, though. You're not willing to put a type parameter on `Wrapper`, @jco?

empanada linguist @jco

@travisbrown @gclaramunt I might be able to swing that...still don't get why it can't tell the two are equal?

empanada linguist @jco

@econlon @travisbrown the real example this is mined from becomes much nastier if it has to have that

Gabriella Gonzalez @GabriellaG439

@econlon @jco @travisbrown Like Eric said, you need to parametrize your class on the type it holds.

good tweet eric @goodtweeteric

@jco @travisbrown burn it all, just get rid of inheritance and cast to Any everywhere

Gabriella Gonzalez @GabriellaG439

@econlon @jco @travisbrown Contrary to what you think your example code is not safe

Travis Brown @travisbrown

@GabrielG439 @econlon @jco It's possible to make it work without a type parameter—you just have to be careful not to lose the refinement.

empanada linguist @jco

@GabrielG439 @econlon @travisbrown how so?

empanada linguist @jco

@GabrielG439 @econlon @travisbrown this is highly undesirable b/c of type inference though, and in many cases you know that Out is fixed

Gabriella Gonzalez @GabriellaG439

@jco @econlon @travisbrown The type of your "hey" function is basically equivalent to: forall a. Thing => a

Travis Brown @travisbrown

@jco @GabrielG439 @econlon You just need a `Wrapper.apply` that returns a refined `Wrapper`: stackoverflow.com/a/33571157/334…

Gabriella Gonzalez @GabriellaG439

@jco @econlon @travisbrown If Out really is fixed then you need to prove that by actually fixing it at the point of definition

empanada linguist @jco

@GabrielG439 @econlon @travisbrown how is this unsafe? just because it doesn't seem useful doesn't make it unsafe?

Gabriella Gonzalez @GabriellaG439

@jco @econlon @travisbrown Parametrizing it on the wrapped type should improve type inference

empanada linguist @jco

@GabrielG439 @econlon @travisbrown it is fixed by t.Out, no?

Gabriella Gonzalez @GabriellaG439

@jco @econlon @travisbrown t.Out is existentially quantified, which means that you can use it, but only in a restricted way

Gabriella Gonzalez @GabriellaG439

@jco @econlon @travisbrown This is hard to explain in one tweet, so tweet storm incoming...

Travis Brown @travisbrown

@GabrielG439 @jco @econlon Not exactly true, thanks to Scala's path-dependent types (assuming the compiler statically knows `t`'s `Out`).

Gabriella Gonzalez @GabriellaG439

@jco @econlon @travisbrown For an existentially quantified type you can only confirm it's consistent with other fields of the same class

Gabriella Gonzalez @GabriellaG439

@travisbrown @jco @econlon Right, this is the same thing as existential quantification. You can know the type within a pattern match

good tweet eric @goodtweeteric

@GabrielG439 @jco @travisbrown the classes end up being huge modules in that case, so probably not too bad

Gabriella Gonzalez @GabriellaG439

@travisbrown @jco @econlon But the type cannot leak from that scope without a type error