Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • 18:16
    SethTisue edited #1407
  • 17:58
    SethTisue synchronize #1407
  • 17:57
    SethTisue commented #1407
  • 17:43
    SethTisue synchronize #1408
  • 17:43
    som-snytt commented #9567
  • 17:43
    SethTisue synchronize #1407
  • 17:40
    SethTisue synchronize #1408
  • 17:25
    SethTisue synchronize #1408
  • 17:24
    SethTisue synchronize #1407
  • 17:08
    SethTisue synchronize #1400
  • 17:07
    SethTisue synchronize #1407
  • 17:01
    harpocrates commented #9556
  • 16:58
    harpocrates commented #9551
  • 16:53
    SethTisue edited #1408
  • 16:53
    SethTisue converted_to_draft #1408
  • 16:53
    SethTisue edited #1408
  • 16:52
    SethTisue labeled #1408
  • 16:52
    SethTisue assigned #1408
  • 16:52
    SethTisue opened #1408
  • 16:52
    SethTisue edited #1407
Fabio Labella
@SystemFw
no pun intended
Klas Segeljakt
@segeljakt
lol
Fabio Labella
@SystemFw
your notation is too imprecise
the 1-kind, 2-kind thing
Ichoran
@Ichoran
Mathematical vectors have arity, for instance. v = (a, b) is a 2-ary vector.
Klas Segeljakt
@segeljakt
(y)
How would you explain kinds?
Fabio Labella
@SystemFw
it cannot distinguish between Either[A, B] and Free[F, R] (the F there can be IO, not Int, whereas the A in Either can be IO[Int], or String, but not IO)
that's the explanation I use for kinds
first of all, talking about kinds in Scala is a bit weird, the notation is not great
so I'm going to use Haskell notation, which is std, and show you the translation to scala
basically it starts with types
a type is a compile time label that's attached to a term (a term is a value like 1 or "hello" or map), which can be used to statically prove the absence of certain behaviour
Ichoran
@Ichoran
Haskell notation is basically the optimal notation for talking about types, anyway. It's like someone took that notation and built a programming language around it.
Fabio Labella
@SystemFw
or in layman terms, a type is a way of classifying value (but try to understand the definition above, because that's the correct one)
similarly, there are labels to classify types themselves
these labels are called kinds
Klas Segeljakt
@segeljakt
types give values meaning?
Fabio Labella
@SystemFw
that's a cool sentence but it doesn't really mean anything :)
traditionally, a kind system is quite simple
Ichoran
@Ichoran
Types just express what you know about a value (which may or may not not be its actual value) without running the program.
Fabio Labella
@SystemFw
by traditionally I mean in SystemFw, or roughly in Haskell, and it's basically a simply typed lambda calculus at the type level. Which means this
imagine there is no subtyping
like in Haskell
Ichoran
@Ichoran
Kinds are a way to classify your types.
Fabio Labella
@SystemFw
then for some types, you can immediately create values
e.g. if I tell you type Int, you know that 1 is a value
if I tell you String, you know that "hello" is a value
if I tell you Option[Int], you know that None and Some(4) are values
and so on
Klas Segeljakt
@segeljakt
ok
Fabio Labella
@SystemFw
the types you can create values for immediately are said to have kind * (pronounced star or Type)
but what about the type Option
you can't create a value of type Option, option of what?
you need further information
if I tell you Option[Int] , then you know
so the type Option needs to know about another type
so Option is said to have kind * -> *
which you can read as a function at the type level
Option has kind * -> * because it takes a concrete type (i.e. a type of kind *, e.g. Int), and returns another concrete type (i.e. a type of kind *, i.e. Option[Int])
does that make any sense at all?
Klas Segeljakt
@segeljakt
yeah
a * -> * is like a function taking a type as an argument and returning a type?
Fabio Labella
@SystemFw
yep
Ichoran
@Ichoran
The notation is perhaps overly abstract.
Fabio Labella
@SystemFw
you can also read that as
Type -> Type
might make it a bit easier, I'm just used to * by now
Klas Segeljakt
@segeljakt
How do you write it if it is Either[Int,Float]
Ichoran
@Ichoran
It's the symbol soup problem, really. Using arrows to define functions is cool when there's only one, but it gets perplexing when you have a bunch of them.