Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • 05:03
    scala-jenkins milestoned #9674
  • 05:03
    som-snytt opened #9674
  • 05:02
    retronym labeled #9673
  • 05:01
    retronym review_requested #9673
  • 05:01
    scala-jenkins milestoned #9673
  • 05:01
    retronym opened #9673
  • 01:41
    SethTisue edited #1433
  • 01:40
    SethTisue labeled #1433
  • 01:40
    SethTisue assigned #1433
  • 01:40
    SethTisue opened #1433
  • Jun 18 22:52

    xuwei-k on xuwei-k-patch-1

    (compare)

  • Jun 18 22:52

    xuwei-k on main

    Create CODEOWNERS https://docs… (compare)

  • Jun 18 22:52
    xuwei-k closed #2084
  • Jun 18 20:45
    jacobus commented #1248
  • Jun 18 20:01

    eed3si9n on main

    Update scala-for-java-programme… Merge pull request #2060 from h… (compare)

  • Jun 18 20:01
    eed3si9n closed #2060
  • Jun 18 19:54
    xuwei-k commented #2059
  • Jun 18 19:54
    xuwei-k review_requested #2084
  • Jun 18 19:54
    xuwei-k review_requested #2084
  • Jun 18 19:54
    xuwei-k opened #2084
Fabio Labella
@SystemFw
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
Vinayak Pathak
@vinayakpathak
makes sense... so existential vs universal types are a type theory concept
Fabio Labella
@SystemFw
yes
Vinayak Pathak
@vinayakpathak
fascinating
Fabio Labella
@SystemFw
indeed :)
Vinayak Pathak
@vinayakpathak
is forSome the trick that lets you encode existential types using universals?
Fabio Labella
@SystemFw
no, it's a native feature for existentials
Vinayak Pathak
@vinayakpathak
or is it the "typeclass trick" using implicits
Fabio Labella
@SystemFw
which is half-broken, and it's going away

or is it the "typeclass trick" using implicits

No, I don't see any relevance to typeclasses and implicits here

Vinayak Pathak
@vinayakpathak
well when you define a typeclass such as trait Monoid[T] you are saying that a Monoid[T] exists for every T however, the way you implement it using implicits, it is guaranteed that it only exists for the T's for which you have defined a typeclass instance
so in some way you are encoding existentials using universals?
Fabio Labella
@SystemFw
no, this is a different thing
Vinayak Pathak
@vinayakpathak
okay
Fabio Labella
@SystemFw
first of all, your example has not much to do with typeclasses or implicits
you can replace Monoid[T] with anything that has a type parameter and explicit instances, and your question remains the same
second, you can look at existentials to be linked to information hiding
as in "I have a Monoid for some type, but I dont know which type"
whereas when you get Monoid[Int], you know that the Monoid is for Int
Vinayak Pathak
@vinayakpathak
true
Fabio Labella
@SystemFw
matter of fact
encoding existentials through universals in a simple way requires higher rank polymorphism (which I've talked about in this channel a few days ago), which scala doesn't have
Vinayak Pathak
@vinayakpathak
i see
Fabio Labella
@SystemFw
you could simulate it in this case, but then again abstract types already give you a way of encoding existential quantification, so...