Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • 19:57
    SethTisue milestoned #9258
  • 19:57
    SethTisue demilestoned #9258
  • 19:57
    SethTisue commented #9258
  • 19:57
    SethTisue commented #9388
  • 19:56
    SethTisue milestoned #9388
  • 19:56
    SethTisue demilestoned #9388
  • 18:03
    ebruchez opened #2017
  • 17:42
    som-snytt edited #9567
  • 17:36
    som-snytt edited #9567
  • 17:36
    som-snytt edited #9567
  • 16:55
    lrytz commented #9631
  • 16:45
    SethTisue commented #9631
  • 16:44
    dwijnand labeled #9632
  • 16:44
    dwijnand edited #9632
  • 16:44
    scala-jenkins milestoned #9632
  • 16:44
    dwijnand opened #9632
  • 16:38
    dwijnand commented #9631
  • 16:35
    dwijnand commented #9567
  • 16:34

    dwijnand on 2.13.x

    Test status quo for leading inf… Postfix error doesn't suppress … Backport Allow infix operators … and 4 more (compare)

  • 16:34
    dwijnand closed #9567
Fabio Labella
@SystemFw
when you do : Model you remove the refinement
which is inferred otherwise
it should bem: Model {type State = Int }
Vinayak Pathak
@vinayakpathak
yeah that's interesting
Fabio Labella
@SystemFw
you can look into the Aux pattern as well to see a shorthand
which is very commonly used in the shapeless world
Vinayak Pathak
@vinayakpathak
yeah I've seen the Aux pattern
Fabio Labella
@SystemFw
same thing, m: Model.Aux[Int]
I'd recommend using existentials only when you need them though
Vinayak Pathak
@vinayakpathak
if I had chosen to implement Model as trait Model[State] though, I would've been notified about the error at the line val m: Model = new Model[Int] {...} coz there would be a missing type parameter
Fabio Labella
@SystemFw
well : Model is a valid type there, so there's no error
the error is when you try to unify it with Int later
Vinayak Pathak
@vinayakpathak
ummm why is Model valid
Fabio Labella
@SystemFw
do you need State to be existential there, since you are already making the whole Model existential in Algorithm?
Vinayak Pathak
@vinayakpathak
i'm not sure what existential means
Fabio Labella
@SystemFw

ummm why is Model valid

Because scala allows you to have abstract (existential) types

well, replace that word with "abstract"
scala allows you to have abstract types
Vinayak Pathak
@vinayakpathak
oh i see ok
ok then i'm not sure when one would need a type to be existential as opposed to just a type parameter
Fabio Labella
@SystemFw
the two things, type parameters and abstract types (universals and existentials) are two different ways to enforce information boudaries
jonathan edwards
@_jedw_twitter
@abdheshkumar Thanks man, I guess i wasn’t reading enough of the page.
Fabio Labella
@SystemFw
well, one use case is to hide the specific type used there
for example, imagine List[Algorithm]
Vinayak Pathak
@vinayakpathak
i see
Fabio Labella
@SystemFw
assume that each algorithm has an input, output and internal state
and the in-out is the only thing that matters from the outside
if you had Algorithm[State] you woudn't be able to put them in a List with a proper type
Vinayak Pathak
@vinayakpathak
hmm i see
Fabio Labella
@SystemFw
but since in my hypothetical example the State is purely internal, you hide it by making it existential
in this case through an abstract type
does that make any sense?
Vinayak Pathak
@vinayakpathak
ok got it
yeah
Fabio Labella
@SystemFw
cool
Vinayak Pathak
@vinayakpathak
but is it an aesthetic thing or do their exist things we couldn't do if existential types didn't exist
Fabio Labella
@SystemFw
that's a really good question
the answer is not that simple unfortunately
you need to distinguish between existential and universal types as a general concept (e.g. in type theory), and the programming language features that encode them
but in short, no, it's not an aesthetic thing
Vinayak Pathak
@vinayakpathak
ahh so universal type being another name for type parameters?
it sort of makes sense... coz when you define trait MyTrait[T] you're saying MyTrait[T] exists for every T but if you say trait MyTrait {type T} you're making no such guarantees
Fabio Labella
@SystemFw
it's a fundamental distinction conceptually. However it is possible to encode existentials through universals with a trick. That's why I'm not sure how to answer your question without being either imprecise or confusing :P

it sort of makes sense... coz when you define trait MyTrait[T] you're saying MyTrait[T] exists for every T but if you say trait MyTrait {type T} you're making no such guarantees

yes, you are making a different guarantee, that it exists a T for which MyTrait exist

those correspond to universal and existential quantification in logic
because at the heart of all this there's a very deep theoretical result which links type theory and logic
the Curry-Howard isomorphism
Vinayak Pathak
@vinayakpathak
yeah... i've heard about that link several times
Fabio Labella
@SystemFw
now, as I said the type theory concepts and the mapping of such concepts to specific programming language feature vary
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