haskell - About Haskell GADTs

Question

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.

Answer 1

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 :: * -> * -> *

Answer 2

* -> * 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.

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].
• Kinds of the form 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 * -> * -> *.

Kinds of higher-order types

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 ((* -> *) -> * -> *) -> * -> *.

GHCi

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 :: *

Kind errors

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

Answer 3

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 :: *