About Haskell GADTs

Question

Can someone explain or give a link explaining the * → * part of the code below?

data BinaryTree t :: * -> * where Leaf :: BinaryTree Empty a Branch :: a -> BinaryTree isempty a -> BinaryTree isempty' a -> BinaryTree NonEmpty a 

Thank you very much.

Answer 1

Signature Signature . They can be used to explicitly determine the arity of a type constructor. * means "any type", and the rest work like normal function types. In this case, we even have a partial application:

 BinaryTree t :: * -> * 

means that “ BinaryTree t is a function from types to types”, which makes sense since you can apply it to another type:

 f :: (BinaryTree t) a -> (BinaryTree t) b * -> * * * -> * * 

The BinaryTree t applies to type a , giving you the type BinaryTree ta :: * . (BinaryTree t) one is not yet fully applied, therefore it has the form * -> * , and you still need to apply it to get a simple type. (This works the same as when f 1 still has type Int -> Int , when f :: Int -> Int -> Int )

Note that you can mix up ordinary “arity declarations” by specifying type parameters that are implicit and kind signatures, as is done here. We could also write BinaryTree as follows:

 data BinaryTree ta -- normal variant 

or like this:

 data BinaryTree :: * -> * -> * -- fully "kinded" 

In both cases, the compiler knows that BinaryTree will accept two type parameters.

And what is it for? Firstly, as described in the link, sometimes you need or want to explicitly declare how many types of parameters your type needs to use. Another, perhaps more interesting case arises when you use different types than * (aka DataKinds ). Look at this:

 data Empty = Empty | NonEmpty data BinaryTree (t :: Empty) (a :: *) :: * where -- ... 

Oh, and ghci lets you look at views if you are not sure. It works the same as :t :

 Prelude> :k Either Either :: * -> * -> * 

Answer 2

* -> * is an example of a view signature. Views can be considered as "types of types." That is, just as values ​​have types, types have types.

Kinds

If we ignore some language extensions, types are created from two constructors:

• * indicates the type of the correct types , i.e. those types that are populated by values ​​such as Int , Char , Maybe Int , [Char] .
• Kinds of the form k1 -> k2 (where k1 and k2 themselves species) are assigned by type constructors , i.e. express expressions that must be filled with one or more type arguments form the correct type. For example: a constructor of type Maybe needs an argument of the form * to create the correct type, and therefore it has the form * -> * ; the same hold for the list type constructor [] , which also has the form * -> * ; a constructor of type Either takes two arguments of the form * to form the correct types (for example, Either Int Char or Either (Maybe Int) [Char] ) and, therefore, has the form * -> * -> * .

Types of higher order types

Note that the constructor of the form -> bound to the right. That is, * -> * -> * matches * -> (* -> *) . For an example of a so-called type of a higher order (i.e., a Type that is used as a type constructor instead of a constructive type), we first consider the Rose type of pink trees:

 data Rose a = Branch a [Rose a] 

This is a first order type type * -> * . But if we generalize, abstracting on its use of the type constructor for lists, we get

 data GRose fa = Branch a (fa) 

which has the form (* -> *) -> * -> * and, therefore, is a type of second order.

Another example of a second-order type is a fixed-point operator of type Fix :

 newtype Fix f = In {out :: f (Fix f)} 

Types of the order above two practically do not occur. One of the few examples I've seen is the Fix version, raised to the form * -> * :

 data HFix ha = HIn {hOut :: h (HFix h) a} 

Indeed, HFix has the form ((* -> *) -> * -> *) -> * -> * .

Ghci

The GHC Interactive Environment (ghci) offers the command :kind (usually abbreviated :k ) to query the type of an expression of type. For instance:

 > :k Either Either :: * -> * -> * > :k Either Int Either Int :: * -> * > :k Either Int Char Either Int Char :: * 

Good mistakes

It’s just that a program may contain a type error, you can enter good errors. For instance:

 > :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 set Either as the second argument to an expression of the type * -> * , rather than * as needed.

This is also a flawed error if you apply an expression of a type of non-functional type (for example, of the form * ) to an expression of another type:

 > :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 , just as functions can have types like Int -> String or a -> a

Basically * denotes any specific type of type Int . The type constructor of the BinaryTree type then takes a specific type to make the concrete type a type of BinaryTree Int or BinaryTree Double . This is indicated by the type BinaryTree , which is * -> * .

You can check this in ghci:

 ghci> :k Int Int :: * ghci> :k Maybe Maybe :: * -> * ghci> :k Maybe Int Maybe Int :: *