Kind (type theory)

Last updated

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.

Contents

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 C++, [1] Haskell and Scala. [2]

Examples

Kinds in Haskell

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

The kind system of Haskell 98 [4] includes exactly two kinds:

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. [5] [6] 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 [[Int]] (list of lists of Ints) are valid applications of the [] type constructor. Therefore, [] is a type of kind . Because Int has kind , applying [] to it results in [Int], of kind . The 2-tuple constructor (,) has kind , the 3-tuple constructor (,,) has kind 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:

dataTreez=Leaf|Fork(Treez)(Treez)

the kind of z could be anything, including , but also 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:

typeFunnyTree=Tree[]-- invalid

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

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

dataAppuntz=Z(untz)

has kind , 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:

dataTree(z::k)=Leaf|Fork(Treez)(Treez)typeFunnyTree=Tree[]-- OK

Since GHC 8.0.1, types and kinds are merged. [7]

See also

Related Research Articles

A method in object-oriented programming (OOP) is a procedure associated with a message and an object. An object consists of data and behavior; these comprise an interface, which specifies how the object may be utilized by any of its various consumers.

In programming languages and type theory, polymorphism is the provision of a single interface to entities of different types or the use of a single symbol to represent multiple different types.

Type inference refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistics.

In computer programming, especially functional programming and type theory, an algebraic data type is a kind of composite type, i.e., a type formed by combining other types.

In programming languages, ad hoc polymorphism is a kind of polymorphism in which polymorphic functions can be applied to arguments of different types, because a polymorphic function can denote a number of distinct and potentially heterogeneous implementations depending on the type of argument(s) to which it is applied. When applied to object-oriented or procedural concepts, it is also known as function overloading or operator overloading. The term ad hoc in this context is not intended to be pejorative; it refers simply to the fact that this type of polymorphism is not a fundamental feature of the type system. This is in contrast to parametric polymorphism, in which polymorphic functions are written without mention of any specific type, and can thus apply a single abstract implementation to any number of types in a transparent way. This classification was introduced by Christopher Strachey in 1967.

In computer science, a tagged union, also called a variant, variant record, choice type, discriminated union, disjoint union, sum type or coproduct, is a data structure used to hold a value that could take on several different, but fixed, types. Only one of the types can be in use at any one time, and a tag field explicitly indicates which one is in use. It can be thought of as a type that has several "cases", each of which should be handled correctly when that type is manipulated. This is critical in defining recursive datatypes, in which some component of a value may have the same type as the value itself, for example in defining a type for representing trees, where it is necessary to distinguish multi-node subtrees and leaves. Like ordinary unions, tagged unions can save storage by overlapping storage areas for each type, since only one is in use at a time.

In functional programming, a monad is an abstraction that allows structuring programs generically. Supporting languages may use monads to abstract away boilerplate code needed by the program logic. Monads achieve this by providing their own data type, which represents a specific form of computation, along with two procedures:

System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. System F was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds (1974).

Lambda cube

In mathematical logic and type theory, the λ-cube is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ-calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ-cube correspond to:

In computer programming languages, a recursive data type is a data type for values that may contain other values of the same type. Data of recursive types are usually viewed as directed graphs.

In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without depending on their type. Such functions and data types are called generic functions and generic datatypes respectively and form the basis of generic programming.

In computer science, a type class is a type system construct that supports ad hoc polymorphism. This is achieved by adding constraints to type variables in parametrically polymorphic types. Such a constraint typically involves a type class T and a type variable a, and means that a can only be instantiated to a type whose members support the overloaded operations associated with T.

In many programming languages, map is the name of a higher-order function that applies a given function to each element of a functor, e.g. a list, returning a list of results in the same order. It is often called apply-to-all when considered in functional form.

In computer programming, a nullary constructor is a constructor that takes no arguments. Also known as a 0-argument constructor or no-argument constructors.

In programming language theory, parametricity is an abstract uniformity property enjoyed by parametrically polymorphic functions, which captures the intuition that all instances of a polymorphic function act the same way.

In the area of mathematical logic and computer science known as type theory, a type constructor is a feature of a typed formal language that builds new types from old ones. Basic types are considered to be built using nullary type constructors. Some type constructors take another type as an argument, e.g., the constructors for product types, function types, power types and list types. New types can be defined by recursively composing type constructors.

A Hindley–Milner (HM) type system is a classical type system for the lambda calculus with parametric polymorphism. It is also known as Damas–Milner or Damas–Hindley–Milner. It was first described by J. Roger Hindley and later rediscovered by Robin Milner. Luis Damas contributed a close formal analysis and proof of the method in his PhD thesis.

In computer science, a type family associates data types with other data types, using a type-level function defined by an open-ended collection of valid instances of input types and the corresponding output types.

In mathematical logic, System U and System U are pure type systems, i.e. special forms of a typed lambda calculus with an arbitrary number of sorts, axioms and rules. They were both proved inconsistent by Jean-Yves Girard in 1972. This result led to the realization that Martin-Löf's original 1971 type theory was inconsistent as it allowed the same "Type in Type" behaviour that Girard's paradox exploits.

Flix is a functional, imperative, and logic programming language developed at Aarhus University, with funding from the Independent Research Fund Denmark, and by a community of open source contributors. The Flix language supports algebraic data types, pattern matching, parametric polymorphism, currying, higher-order functions, extensible records, channel and process-based concurrency, and tail call elimination. Two notable features of Flix are its type and effect system and its support for first-class Datalog constraints.

References

  1. "CS 115: Parametric Polymorphism: Template Functions". www2.cs.uregina.ca. Retrieved 2020-08-06.
  2. Generics of a Higher Kind
  3. Pierce (2002), chapter 32
  4. Kinds - The Haskell 98 Report
  5. "Chapter 4 Declarations and Binding". Haskell 2010 Language Report. Retrieved 23 July 2012.
  6. Miran, Lipovača. "Learn You a Haskell for Great Good!". Making Our Own Types and Typeclasses. Retrieved 23 July 2012.
  7. "9.1. Language options — Glasgow Haskell Compiler Users Guide".