Consider the following function:
f :: a -> Int
f x = (1 :: Int)
We might say that the type of f
is a -> Int
, and that f
therefore is of a "polymorphic" type.
Which of the following is the most accurate way to think about f
?
There is in fact a single f
of type a -> Int
. It can be used, however, as an f :: Int -> Int
, as an f :: Double -> Int
, and so forth.
Literally speaking, the type of f
is NOT a -> Int
. Indeed, that is just a shorthand way of saying that there is a family of functions f
whose type is concrete (i.e., there is an f :: Int -> Int
, an f :: Double -> Double
, and so forth; moreover, each of these functions is distinct from each other).
Similarly, we can consider the following type declaration:
data Maybe a = Just a | Nothing
And ask which of the two views is more correct:
There is no single type Maybe
; indeed, there is merely a family of concrete types (Maybe Int
, Maybe String
, etc) and nothing more.
There is in fact a single type Maybe
. This type is a higher-kinded type. When we say that it is a "type" we mean it literally (not as a shorthand for (1)). It just so happens that we can also write Maybe Int
, Maybe Double
, and so forth to generate distinct types (which happen to be concrete). But, at the end of the day (i.e.): Maybe
, Maybe Int
, and Maybe String
denote three distinct types, two of which are concrete and one of which is higher-kinded.
In Haskell, are "higher-kinded types" really types? Or are only concrete types "the real types", and when we speak of "higher-kinded types" we are merely denoting a family of concrete types. Moreover, do paramametrically polymorphic functions denote functions of a single type, or do they merely denote a collection functions 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
.