In Haskell, are "higher-kinded types" *really* types? Or do they merely denote collections of *concrete* types and nothing more?
It's not entirely clear what you want to ask, and what is the practical difference between 1 and 2 in both cases, but from an underlying math perspective:
Parametrically Polymorphic Functions
f
actually has type f :: forall a.a->int
It is a perfectly legal type for a function in typed lambda calculus, which Haskell is based on. It can be something like:
f = λa:Type.λx:a.(body for f)
How do you get Double->Int
from it? You apply it to Double
type:
f Double = (λa:Type.λx:a.(body for f)) Double => λx:Double.(body for f|a=Double)
Haskell does both operations (type abstraction and type application) behind the scene, although it is possible to explicitly state forall
part in the type signature with XExplicitForAll
GHC extension, and explicitly make a Double->Int
instance of f
with type signature:
f_double :: Double -> Int
f_double = f
Higher Kinded Types
Consider a simple type:
data Example = IntVal Int | NoVal
(Yes, it is Maybe Int
).
Maybe
is a type constructor, just like IntVal
is a data constructor. It is exactly the same thing, only 'one level higher', in the sense that Maybe
is applied to Type
, much like IntVal
is applied to Int
.
In lambda calculus, Maybe
has type:
Maybe : Type->Type
Haskell doesn't allow you to get a type from type constructor, but allows you to get a kind (which is just a fancy name for type of type):
:k Maybe
Maybe :: * -> *
So no, Maybe
is not a type: you can't have an object with the type Maybe
. Maybe
is (almost) a function from types to types, like IntVal
is a function from values to values.
We call the result of applying Maybe
to String
as Maybe String
, like we call the result of applying IntVal
to 4
as IntVal 4
.
First a question: Is the statement "all lists have length" a single statement or a series of statements "list1 has length", "list2 has length",...?
If you give the type of f
with explicit forall
, you get f :: forall a. a -> Int
. First of all, this is not "higher-kinded". We can do the following in GHCI:
λ> :set -XRankNTypes
λ> :k (forall a. a -> Int)
(forall a. a -> Int) :: *
So f
has a kind of *
.
Now, in Haskell, we can use ~
for type equality. We can set the following to check stuff in GHCI:
λ> :set -XImpredicativeTypes
λ> :set -XTypeFamilies
λ> :t undefined :: ((~) Int Int) => a
undefined :: ((~) Int Int) => a :: a
This shows that GHC figured out type equality for this example. Type inequality will give the following error:
λ> undefined :: ((~) (Int -> Int) (Int)) => a
<interactive>:22:1:
Couldn't match expected type ‘Int’ with actual type ‘Int -> Int’
In the expression: undefined :: ((~) (Int -> Int) (Int)) => a
In an equation for ‘it’:
it = undefined :: ((~) (Int -> Int) (Int)) => a
Now using this method directly will prevent us from comparing the type of f
, but I found a slight variant that should work for our purposes:
λ> :t undefined :: forall a. ((a -> Int) ~ (Int -> Int)) => a
undefined :: forall a. ((a -> Int) ~ (Int -> Int)) => a :: Int
In other words, if f
is type-equivalent to g :: Int -> Int
, then a
must be Int. This is similar to x = y
, y = 0
so x = 0
. We don't have x = 0
until we specify y = 0
, until then we just have x = y
.
Maybe
is different because it has the following kind:
λ> :k Maybe
Maybe :: * -> *
Because we're using DataKinds
, we have :k (~) :: k -> k -> GHC.Prim.Constraint
, so we can do things like:
λ> :t undefined :: (~) Maybe Maybe => Int
undefined :: (~) Maybe Maybe => Int :: Int
λ> :k Either ()
Either () :: * -> *
λ> :t undefined :: (~) Maybe (Either ()) => Int
Couldn't match expected type ‘Either ()’ with actual type ‘Maybe’
To sum up, f :: forall a. a -> Int
makes as much sense as the statement "if you give me anything, I'll give you an Int". Could you translate the statement into a bunch of statements "if you give me a dog..", "if you give me a penny.."? Yeah, but it weakens the statement. At the end, decide precisely what you mean by the "same" and you get your answer.