World Library  
Flag as Inappropriate
Email this Article

Kind (type theory)

Article Id: WHEBN0020627460
Reproduction Date:

Title: Kind (type theory)  
Author: World Heritage Encyclopedia
Language: English
Subject: Data types, Type constructor, Type theory, Type system, Process Environment Block
Collection: Data Types, Type Theory
Publisher: World Heritage Encyclopedia
Publication
Date:
 

Kind (type theory)

In the area of mathematical logic and computer science known as type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator. A kind system is essentially a simply typed lambda calculus "one level up", endowed with a primitive type, denoted * and called "type", which is the kind of any data type which does not need any type parameters.

A kind is sometimes confusingly described as the "type of a (data) type", but it is actually more of an arity specifier. Syntactically, it is natural to consider polymorphic types to be type constructors, thus non-polymorphic types to be nullary type constructors. But all nullary constructors, thus all monomorphic types, have the same, simplest kind; namely *.

Since higher-order type operators are uncommon in programming languages, in most programming practice, kinds are used to distinguish between data types and the types of constructors which are used to implement parametric polymorphism. Kinds appear, either explicitly or implicitly, in languages whose type systems account for parametric polymorphism in a programatically accessible way, such as Haskell and Scala.[1]

Contents

  • Examples 1
  • Kinds in Haskell 2
    • Kind inference 2.1
  • See also 3
  • References 4

Examples

  • *, pronounced "type", is the kind of all data types seen as nullary type constructors, and also called proper types in this context. This normally includes function types in functional programming languages.
  • * \rightarrow * is the kind of a unary type constructor, e.g. of a list type constructor.
  • * \rightarrow * \rightarrow * is the kind of a binary type constructor (via currying), e.g. of a pair type constructor, and also that of a function type constructor (not to be confused with the result of its application, which itself is a function type, thus of kind *)
  • (* \rightarrow *) \rightarrow * is the kind of a higher-order type operator from unary type constructors to proper types. See Pierce (2002), chapter 32 for an application.

Kinds in Haskell

(Note: Haskell documentation uses the same arrow for both function types and kinds.)

Haskell's kind system[2] has just two rules:

  • *, pronounced "type" is the kind of all data types.
  • k_1 \rightarrow k_2 is the kind of a unary type constructor, which takes a type of kind k_1 and produces a type of kind k_2.

An inhabited type (as proper types are called in Haskell) is a type which has values. For instance, ignoring type classes which complicate the picture, 4 is a value of type Int, while [1, 2, 3] is a value of type [Int] (list of Ints). Therefore, Int and [Int] have kind *, but so does any function type, for instance Int -> Bool or even Int -> Int -> Bool.

A type constructor takes one or more type arguments, and produces a data type when enough arguments are supplied, i.e. it supports partial application thanks to currying.[3][4] This is how Haskell achieves parametric types. For instance, the type [] (list) is a type constructor - it takes a single argument to specify the type of the elements of the list. Hence, [Int] (list of Ints), [Float] (list of Floats) and even (list of lists of Ints) are valid applications of the [] type constructor. Therefore, [] is a type of kind * \rightarrow *. Because Int has kind *, applying it to [] results in [Int], of kind *. The 2-tuple constructor (,) has kind * \rightarrow * \rightarrow *, the 3-tuple constructor (,,) has kind * \rightarrow * \rightarrow * \rightarrow * and so on.

Kind inference

Standard Haskell does not allow polymorphic kinds. This is in contrast to parametric polymorphism on types, which is supported in Haskell. For instance, in the following example:

data Tree z  = Leaf | Fork (Tree z) (Tree z)

the kind of z could be anything, including *, but also * \rightarrow * etc. Haskell by default will always infer kinds to be *, unless the type explicitly indicates otherwise (see below). Therefore the type checker will reject the following use of Tree:

type FunnyTree = Tree []     -- invalid

because the kind of [], * \rightarrow * does not match the expected kind for z, which is always *.

Higher-order type operators are allowed however. For instance:

data App unt z = Z (unt z)

has kind (* \rightarrow *) \rightarrow * \rightarrow *, i.e. unt is expected to be a unary data constructor, which gets applied to its argument, which must be a type, and returns another type.

GHC has the extension PolyKinds, which, together with KindSignatures, allows polymorphic kinds. For example:

data Tree (z :: k) = Leaf | Fork (Tree z) (Tree z)
type FunnyTree = Tree []     -- OK

See also

References

  • Pierce, Benjamin (2002).  , chapter 29, "Type Operators and Kinding"
  1. ^ Generics of a Higher Kind
  2. ^ Kinds - The Haskell 98 Report
  3. ^ "Chapter 4 Declarations and Binding". Haskell 2010 Language Report. Retrieved 23 July 2012. 
  4. ^ Miran, Lipovača. "Learn You a Haskell for Great Good!". Making Our Own Types and Typeclasses. Retrieved 23 July 2012. 
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
 
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
 
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.
 


Copyright © World Library Foundation. All rights reserved. eBooks from Project Gutenberg are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.