## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### Activity
• 07:33
NthPortal synchronize #9388
• 07:30
NthPortal synchronize #9258
• 07:23
NthPortal synchronize #9388
• 07:18
dwijnand edited #12395
• 07:17
dwijnand assigned #12392
• 07:17

dwijnand on 2.13.x

Handle Singleton types in patma… Handle Singleton types in patma… Merge pull request #9622 from d… (compare)

• 07:17
dwijnand closed #9622
• 07:17
dwijnand closed #12392
• 07:12
dwijnand commented #1409
• 07:12
dwijnand edited #1409
• 07:11
dwijnand synchronize #1409
• 05:15
jaingaurav1990 commented #11903
• 02:14
retronym synchronize #9622
• 01:18
retronym commented #9622
• 01:15
retronym synchronize #9622
• 01:14
SethTisue edited #1413
• 01:13
SethTisue labeled #1413
• 01:13
SethTisue assigned #1413
• 01:12
SethTisue opened #1413
• 01:10

SethTisue on 2.13.x

Ichoran
@Ichoran
Arity just means "how many arguments". It doesn't tell you whether they are type arguments or value arguments.
Or what you pack them into.
Klas Segeljakt
@segeljakt
I should not have wrote it like that
1-kind: Foo[A]
2-kind: Foo[A,B]
3-kind: Foo[A,B,C]
…?
Fabio Labella
@SystemFw
ehm, kind of
no pun intended
Klas Segeljakt
@segeljakt
lol
Fabio Labella
@SystemFw
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
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