Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • 14:28
    SethTisue synchronize #1265
  • 14:25
    SethTisue milestoned #7515
  • 14:06
    tkawachi closed #2148
  • 14:06
    tkawachi commented #2148
  • 13:21
    som-snytt commented #7515
  • 13:21
    som-snytt edited #7515
  • 12:07
    myazinn commented #12440
  • 11:56
    som-snytt closed #12440
  • 11:56
    som-snytt commented #12440
  • 10:26
    myazinn edited #12440
  • 10:24
    myazinn opened #12440
  • 08:47

    nicolasstucki on main

    Clean up grammar and other nit … Clean up grammar and other nit … Clean up grammar and other nit … and 2 more (compare)

  • 08:47
    nicolasstucki closed #2121
  • 08:46
    nicolasstucki assigned #2148
  • 08:26
    sjrd commented #1265
  • 08:23
    lrytz edited #12439
  • 08:23
    lrytz milestoned #12439
  • 08:23
    lrytz opened #12439
  • 08:23
    lrytz labeled #12439
  • 08:23
    lrytz labeled #12439
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...
Vinayak Pathak
@vinayakpathak
i'm thinking about your statement: "I have a Monoid for some type, but I dont know which type"
Fabio Labella
@SystemFw
yeah, that doesn't hold
go back to Model
you have a Model for some State, but you don't know which State
hence when you try to coerce it to Int, type mismatch
Vinayak Pathak
@vinayakpathak
that is if I write val m: Model = new Model {...}?
Fabio Labella
@SystemFw
yes
Vinayak Pathak
@vinayakpathak
i see i see
so existential types allow us to define values that have this information hiding feature
if you wanted to define a function that took a Model without knowing its State, you could do that with universal types too no?
Fabio Labella
@SystemFw
nope
Vinayak Pathak
@vinayakpathak
def f[Model[_]] = ??? ?
Fabio Labella
@SystemFw
because you would have Model[State]
wait
the _ you are using there doesn't mean what you think it means
because scala is weird
like
I know what you mean
but your code there doesn't mean that
Vinayak Pathak
@vinayakpathak
i see!
Fabio Labella
@SystemFw
it means that you are taking a higher-kinded type Model[_]
or in other words
def f[Model[_]] = ???
is not the same
and in fact has nothing to do with