Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • Oct 18 2022 19:35
    @SethTisue banned @lunaterra22
  • Sep 14 2022 18:08
    @SethTisue banned @discjock:matrix.org
  • Sep 12 2022 20:37
    @SethTisue banned @manuelzamoratetherbtcusa:matrix.org
  • Sep 06 2022 14:29
    @SethTisue banned @white_hat_hacker:minds.com
  • Sep 06 2022 14:29
    @SethTisue banned @alexchole:matrix.org
  • Aug 31 2022 17:03
    @SethTisue banned @andersonwatts7:matrix.org
  • Jul 19 2022 20:37
    @SethTisue banned @tonyobanon
  • Jan 02 2022 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
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
Rob Norris
@tpolecat
This series on the typelevel blog is pretty good, re: this specific issue in Scala https://typelevel.org/blog/2015/07/13/type-members-parameters.html
Fabio Labella
@SystemFw
this is one aspect where theoretical background does help
Vinayak Pathak
@vinayakpathak
i have spent a lot of time on the other side of computer science theory, i.e., algorithms and complexity... only recently discovered the type theory, category theory etc... and it's all super fascinating
Fabio Labella
@SystemFw
otherwise it's hard to make intuition precise
@vinayakpathak I'd also recommend some basic study of logic
nothing too advanced, but the basics do help when reading about type theory

on the other side of computer science theory,

there's more... it's a fractal rabbit hole

one random example: models of computation, applied to concurrent and distributed computation
Vinayak Pathak
@vinayakpathak
i agree :)
Fabio Labella
@SystemFw
I wish people appreciated it more
Vinayak Pathak
@vinayakpathak
i feel that broadly though cs theory can be divided into the Turing style areas and the Church style areas
Turing style being algorithms, running time, complexity, etc... Church style being more logic, type theory, that sort of stuff
not sure what kinds of models of concurrent and distributed computations you are talking about... i remember seeing some in my grad school days, but they were mostly Turing style
@tpolecat thanks will check it out
Fabio Labella
@SystemFw
I mean, I don't want to open a whole new rabbit hole to dive into, type theory is big enough. But things like pi calculus, join calculus, model and temporal logic, and so on