The kind system is one of the hidden gems of GHC. I especially think the connection with runtime machine representation and operational semantics is the kind of incredible coming together of low-level and high-level concerns that typifies haskell to me.
Quality content! Great tone of voice, the emphasis on certain words and ideas, nice cadence between sentences! Very precise sentences and definitions! As Darth Vader would say:“Most impressive!”
Types serve to abstract over values, Kinds serve to abstract over Types. At some point we will want to abstract over Kinds and then up and up... What will the fix point be? A type system where values are on par with values ? (Dependent-types?)
Excellent video, as always :) Is there a defaulting mechanism for kinds? Notice that the kind of ReaderT that GHC tells us is only one of many different kinds you could assign to it. GHC tells us: type ReaderT :: Type -> (Type -> Type) -> Type -> Type But it will gladly accept: type ReaderT :: Type -> ((Type -> Type) -> Type) -> (Type -> Type) -> Type Or even: type ReaderT :: Type -> (Constraint -> Type) -> Constraint -> Type We can even turn on PolyKinds and see that indeed GHC can infer a more general kind of type ReaderT :: Type -> (k -> Type) -> k -> Type This all makes sense since there's nothing here that restricts _a_ to having kind Type. So my question is: What are the rules GHC uses to determine these ambiguous kinds (without PolyKinds)?
Hello. Please may I have a link to your Haskell PhD thesis. I had it but lost it. I have been doing Haskell for a month now, I would love to burn some hours torturing my brain with your work
I am not really a Haskell programmer but I read a lot about it. How does this compare to Rust's trait type system? Its basically an abstraction of "similar kinds of types" as you said.
Kind signatures have confused me a decent bit in Haskell. Heres some questions If a Constraint appears to the left of a fat arrow, what appears to the right? A Type? Does it then "output" a Type? So its kind signature would be (=>) :: Constraint -> Type -> Type. Is => defined somewhere. Is it right associative? Is Constraint a kind level Bool. I understand super basic set theory/intro logic and the fat arrow looks like an "implies", should it be read this way? Could fmap :: Functor f => (a -> b) -> f a -> f b be read as "if Functor f is true then (a -> b) -> f a -> f b is true". If so, what does the truth of a type mean? Where should I go for more info, theres got to be a book chapter or some papers right? Side note: I did import Data.Kind (Type, Constraint) :k Type -- Type :: * :k Constraint -- Constraint :: * WHAT? Does * there mean Type! If so that explains why we can use -> in kind signatures but I have no idea how to write a function that outputs a Type, do I need to use the type keyword for this? Is there a way to punch Functor List into ghci and get True if List's Functor instance is in scope and False if it isn't? Sorry for asking so many questions
@Richard Eisenberg Thanks for the reply! What about the proper way to read a fat arrow aloud? Is it intended to look like an "implies" from basic logic, or is that a complete coincidence...
The terminology is kind of interesting, we say `4 :: Int` is a value, and `id :: Int -> Int` is a value, but while `Int :: Type` is a type, `List :: Type -> Type` is not. Is there a word that includes both Int and List, i.e., things that can be given as arguments to a type family? "Type-level value"? ("n-ary type constructor" perhaps but that gets iffy once we want to include unsaturated type families as well.)
@Richard Eisenberg Monad is a good point. I thought a while back that maybe there's an alternate universe where the "class" keyword is "constraint" and classes are called "constraint constructors".
Amazing video, so informative! Looking forward to the next one
Incredible walkthrough!
Best Haskell instructor ever!
Yours is the best username ever
Thank you as always for the video, Mr. E
👨💻
The kind system is one of the hidden gems of GHC. I especially think the connection with runtime machine representation and operational semantics is the kind of incredible coming together of low-level and high-level concerns that typifies haskell to me.
The explanation is very concise. I finally learned something about haskell without headache! Thank you!
great videos !. Please never stop making them!
Quality content! Great tone of voice, the emphasis on certain words and ideas, nice cadence between sentences! Very precise sentences and definitions! As Darth Vader would say:“Most impressive!”
Informative and easy-to-follow :)
Types serve to abstract over values, Kinds serve to abstract over Types. At some point we will want to abstract over Kinds and then up and up... What will the fix point be? A type system where values are on par with values ? (Dependent-types?)
Great video!
Excellent video, as always :)
Is there a defaulting mechanism for kinds? Notice that the kind of ReaderT that GHC tells us is only one of many different kinds you could assign to it.
GHC tells us:
type ReaderT :: Type -> (Type -> Type) -> Type -> Type
But it will gladly accept:
type ReaderT :: Type -> ((Type -> Type) -> Type) -> (Type -> Type) -> Type
Or even:
type ReaderT :: Type -> (Constraint -> Type) -> Constraint -> Type
We can even turn on PolyKinds and see that indeed GHC can infer a more general kind of
type ReaderT :: Type -> (k -> Type) -> k -> Type
This all makes sense since there's nothing here that restricts _a_ to having kind Type.
So my question is: What are the rules GHC uses to determine these ambiguous kinds (without PolyKinds)?
Hello. Please may I have a link to your Haskell PhD thesis. I had it but lost it. I have been doing Haskell for a month now, I would love to burn some hours torturing my brain with your work
I am not really a Haskell programmer but I read a lot about it. How does this compare to Rust's trait type system? Its basically an abstraction of "similar kinds of types" as you said.
Kind signatures have confused me a decent bit in Haskell. Heres some questions
If a Constraint appears to the left of a fat arrow, what appears to the right? A Type? Does it then "output" a Type? So its kind signature would be (=>) :: Constraint -> Type -> Type. Is => defined somewhere. Is it right associative?
Is Constraint a kind level Bool. I understand super basic set theory/intro logic and the fat arrow looks like an "implies", should it be read this way? Could fmap :: Functor f => (a -> b) -> f a -> f b be read as "if Functor f is true then (a -> b) -> f a -> f b is true". If so, what does the truth of a type mean?
Where should I go for more info, theres got to be a book chapter or some papers right?
Side note: I did
import Data.Kind (Type, Constraint)
:k Type
-- Type :: *
:k Constraint
-- Constraint :: *
WHAT? Does * there mean Type! If so that explains why we can use -> in kind signatures but I have no idea how to write a function that outputs a Type, do I need to use the type keyword for this? Is there a way to punch
Functor List
into ghci and get True if List's Functor instance is in scope and False if it isn't?
Sorry for asking so many questions
@Richard Eisenberg Thanks for the reply! What about the proper way to read a fat arrow aloud? Is it intended to look like an "implies" from basic logic, or is that a complete coincidence...
very interesting. type of types, meta types.... powerful, i was wondering how functors could be implemented for any container ....
The terminology is kind of interesting, we say `4 :: Int` is a value, and `id :: Int -> Int` is a value, but while `Int :: Type` is a type, `List :: Type -> Type` is not.
Is there a word that includes both Int and List, i.e., things that can be given as arguments to a type family? "Type-level value"?
("n-ary type constructor" perhaps but that gets iffy once we want to include unsaturated type families as well.)
@Richard Eisenberg Monad is a good point. I thought a while back that maybe there's an alternate universe where the "class" keyword is "constraint" and classes are called "constraint constructors".
Java doesn't have higher kinded types, but Scala does, so if you want this on the JVM you can just use Scala.
It's easier to use: kind List :: Type -> Type instead of the type keyword