Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • Oct 18 19:35
    @SethTisue banned @lunaterra22
  • Sep 14 18:08
    @SethTisue banned @discjock:matrix.org
  • Sep 12 20:37
    @SethTisue banned @manuelzamoratetherbtcusa:matrix.org
  • Sep 06 14:29
    @SethTisue banned @white_hat_hacker:minds.com
  • Sep 06 14:29
    @SethTisue banned @alexchole:matrix.org
  • Aug 31 17:03
    @SethTisue banned @andersonwatts7:matrix.org
  • Jul 19 20:37
    @SethTisue banned @tonyobanon
  • Jan 02 23:58
    @SethTisue banned @fakubishes:nerdsin.space
  • Dec 15 2021 05:01
    som-snytt commented #12516
  • Dec 15 2021 04:38
    SethTisue edited #1312
  • Dec 15 2021 04:38
    SethTisue opened #2273
  • Dec 15 2021 04:31
    jackkoenig opened #12516
  • Dec 15 2021 04:29
    SethTisue edited #1312
  • Dec 15 2021 04:28
    SethTisue edited #1312
  • Dec 15 2021 04:27
    SethTisue labeled #9831
  • Dec 15 2021 04:27
    scala-jenkins milestoned #9831
  • Dec 15 2021 04:27
    SethTisue labeled #9831
  • Dec 15 2021 04:27
    SethTisue opened #9831
  • Dec 15 2021 03:35
    som-snytt commented #11339
  • Dec 15 2021 03:27
    som-snytt labeled #12494
Fabio Labella
@SystemFw
and in fact has nothing to do with
def f(model: Model[_]) = ???
this is what you mean
a wildcard type
which again, it's a feature that encodes existentials
Vinayak Pathak
@vinayakpathak
actually yes, that's what i meant indeed
isn't this saying that f takes a value of type Model but doesn't care what State is
Fabio Labella
@SystemFw
yes
it's introducing an existential again
which is clearer if you use the forSome thing (which however is going away)
def f(model: Model[A] forSome { type A })
Vinayak Pathak
@vinayakpathak
i see i see
Fabio Labella
@SystemFw
whereas def f[A](model: Model[A]) means forall type A
Vinayak Pathak
@vinayakpathak
right
ok so doesn't it then encode existential types?
Fabio Labella
@SystemFw
what's "it" now?
Vinayak Pathak
@vinayakpathak
umm def f(model: Model[_])
or the one using forSome
Fabio Labella
@SystemFw
yes it does
both do
but thats' because you are using specific features that introduce existentials
you are not using universals anymore
Vinayak Pathak
@vinayakpathak
oh ok
oh i see
Fabio Labella
@SystemFw

for example in scala wildcard types are existentials, forSome are existentials, plus there's the fact that abstract types are existential types, which you are seeing here

as I said above

Vinayak Pathak
@vinayakpathak
actually, we can't really access the State type inside f's definition in this case can we
Fabio Labella
@SystemFw
nope, because it's existential
for example
try taking two Model[_] and assigning the values of type State inside them to each other
and you'll see a weird error about _1and _2
this is how a lot of people come across existentials for the first time
it makes their code magically compile at first (since it accepts anything)
Vinayak Pathak
@vinayakpathak
i see... coz it will think the first model's State is different from the second one's State?
Fabio Labella
@SystemFw
and then it fails later
Vinayak Pathak
@vinayakpathak
yes that's sort of what happened with me :)
Fabio Labella
@SystemFw

coz it will think the first model's State is different from the second one's State

more precisely, it will think that it has no way to know, which is what existential quantification is all about

Vinayak Pathak
@vinayakpathak
yes ok got it
Fabio Labella
@SystemFw
even if you pass two Model which do have the same State, you have hidden that information
when you add refinements and Aux to an abstract type, you are propagating that info again
Vinayak Pathak
@vinayakpathak
right
ok this makes a lot more sense... thanks for spending all this time explaining this!
Rob Norris
@tpolecat
:clap:
Fabio Labella
@SystemFw
@vinayakpathak no problem :)
There's a whole field or two of computer science about this stuff, so don't worry if you find it tricky
Vinayak Pathak
@vinayakpathak
type theory being one of them i guess?
is there a type theory book you'd recommend btw?
Rob Norris
@tpolecat
Path-dependent [existential] types are one of the defining features of Scala but they're poorly understood. Even by scalac in some cases. Poorly explained also.
Fabio Labella
@SystemFw
well, Types and Programming Languages is kinda the standard
also note that scala is somewhat unique in this regard
some things are novel, others require some skill to be linked to the theory
Vinayak Pathak
@vinayakpathak
i see i see... i will checkout that book