Can anyone explain or give a link explaining * -> * part of the code below?
data BinaryTree t :: * -> * where
Leaf :: BinaryTree Empty a
Branch :: a -> BinaryTree isempty a -> BinaryTree isempty' a -> BinaryTree NonEmpty a
Thanks a lot.
Can anyone explain or give a link explaining * -> * part of the code below?
data BinaryTree t :: * -> * where
Leaf :: BinaryTree Empty a
Branch :: a -> BinaryTree isempty a -> BinaryTree isempty' a -> BinaryTree NonEmpty a
Thanks a lot.
Kind signatures. They are can be used to explicitly define the arity of a type constructor. The *
means "any type", and the rest works kind of like normal function types.In this case, we even have a partial application:
BinaryTree t :: * -> *
means "BinaryTree t
is a function from types to types", which makes sense, since you can apply it to one other type:
f :: (BinaryTree t) a -> (BinaryTree t) b
* -> * * * -> * *
The BinaryTree t
part is applied to the type a
, giving you a type BinaryTree t a :: *
. (BinaryTree t)
alone is not fully applied yet, thus having a kind * -> *
, and you still need to apply it to get a simple type. (This works the same way as when f 1
still has type Int -> Int
when f :: Int -> Int -> Int
)
Note that you can mix normal "arity declarations", mentioning a type's parameters, which are implicit, and kind signatures, as it is done here. We could also have written BinaryTree
as follows:
data BinaryTree t a -- normal variant
or like this:
data BinaryTree :: * -> * -> * -- fully "kinded"
In both cases, the compiler knows that BinaryTree
is going to take two type parameters.
And what is it for? First, like is is described in the link, sometimes you need or want to explicitly declare how many type parameters your type should take. Another maybe more interesting case occurs when you use diffent kinds than *
(aka DataKinds). Look at this:
data Empty = Empty | NonEmpty
data BinaryTree (t :: Empty) (a :: *) :: * where
-- ...
Oh, and ghci lets you look at kinds, in case you are unsure. It works the same way as :t
:
Prelude> :k Either
Either :: * -> * -> *
* -> *
is an example of a kind signature. Kinds can be thought of as the "types of types". That is, just as values have types, types have kinds.
If we ignore some language extensions, kinds are built from just two constructors:
*
denotes the kind of proper types, i.e., those types that are inhabited by values, such as Int
, Char
, Maybe Int
, [Char]
.k1 -> k2
(where k1
and k2
are themselves kinds) designate type constructors, i.e., type expressions that require to be completed with one or more type arguments to form a proper type. For example: type constructor Maybe
needs an argument of kind *
in order to produce a proper type and so it has kind * -> *
; the same hold for the type constructor []
of lists, which thus also has kind * -> *
; the type constructor Either
takes two arguments of kind *
to form proper types (such as Either Int Char
or Either (Maybe Int) [Char]
) and, hence, it has kind * -> * -> *
.Note that the kind constructor ->
associates to the right. That is, * -> * -> *
is the same as * -> (* -> *)
. For an example of a so called higher-order type (i.e., a type that takes as a type constructor rather than a proper type as its argument), first consider the type Rose
of rose trees:
data Rose a = Branch a [Rose a]
This is a first-order type of kind * -> *
. But if we generalise by abstracting over its use of the type constructor for lists, we obtain
data GRose f a = Branch a (f a)
which has kind (* -> *) -> * -> *
and, hence, is a second-order type.
Another example of a second-order type is the type-level fixed-point operator Fix
:
newtype Fix f = In {out :: f (Fix f)}
Types of order higher than two in practice hardly occur. One of the few examples that I have seen is a version of Fix
"lifted to kind * -> *
:
data HFix h a = HIn {hOut :: h (HFix h) a}
Indeed, HFix
is of kind ((* -> *) -> * -> *) -> * -> *
.
The GHC's interactive environment (ghci) offers the command :kind
(typically abbreviated to :k
) for querying the kind of a type expression. For example:
> :k Either
Either :: * -> * -> *
> :k Either Int
Either Int :: * -> *
> :k Either Int Char
Either Int Char :: *
Just a program can contain a type error, it is possible to introduce kind errors. For example:
> :k Either Int Maybe
<interactive>:1:12:
Expecting one more argument to `Maybe'
In a type in a GHCi command: Either Int Maybe
Here we have supplied as the second argument to Either
a type expression of kind * -> *
rather than *
as required.
It is also a kind error if you apply a type expression of nonfunction kind (i.e, of kind *
) to another type expression:
> :k Int Char
<interactive>:1:1:
`Int' is applied to too many type arguments
In a type in a GHCi command: Int Char
This notation is used to denote kinds, similar to how functions can have types such as Int -> String
or a -> a
Basically *
denotes any concrete type like Int
. A type constructor like BinaryTree
then takes a concrete type to make a concrete type like BinaryTree Int
or BinaryTree Double
. This is denoted by the kind of BinaryTree
, which is * -> *
.
You can check it out in ghci:
ghci> :k Int
Int :: *
ghci> :k Maybe
Maybe :: * -> *
ghci> :k Maybe Int
Maybe Int :: *