In
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includin ...
, a type family associates
data type
In computer science and computer programming, a data type (or simply type) is a set of possible values and a set of allowed operations on it. A data type tells the compiler or interpreter how the programmer intends to use the data. Most progra ...
s with other
data type
In computer science and computer programming, a data type (or simply type) is a set of possible values and a set of allowed operations on it. A data type tells the compiler or interpreter how the programmer intends to use the data. Most progra ...
s, using a type-level
function defined by an open-ended collection of valid instances of input types and the corresponding output types.
Type families are a feature of some
type system
In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer progra ...
s that allow partial functions between types to be defined by
pattern matching
In computer science, pattern matching is the act of checking a given sequence of tokens for the presence of the constituents of some pattern. In contrast to pattern recognition, the match usually has to be exact: "either it will or will not be ...
. This is in contrast to data
type constructor
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. So ...
s, which define
injective
In mathematics, an injective function (also known as injection, or one-to-one function) is a function that maps distinct elements of its domain to distinct elements; that is, implies . (Equivalently, implies in the equivalent contraposi ...
functions from all types of a particular
kind to a new set of types, and type synonyms (a.k.a.
typedef
typedef is a reserved keyword in the programming languages C, C++, and Objective-C. It is used to create an additional name (''alias'') for another data type, but does not create a new type, except in the obscure case of a qualified typedef of ...
), which define functions from all types of a particular kind to another existing set of types using a single case.
Type families and
type class
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 a ...
es are closely related: normal type classes define partial functions from types to a collection of named ''values'' by pattern matching on the input types, while type families define partial functions from types to ''types'' by pattern matching on the input types. In fact, in many uses of type families there is a single type class which logically contains both values and types associated with each instance. A type family declared inside a type class is called an associated type.
Programming language
A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language.
The description of a programming l ...
s with support for type families or similar features include
Haskell
Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lan ...
(with a common language extension),
Standard ML
Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of ...
(through its module system),
Scala (under the name "abstract types"), and
C++ (through use of typedefs in templates).
Variations
The
TypeFamilies
extension in the
Glasgow Haskell Compiler
The Glasgow Haskell Compiler (GHC) is an open-source native code compiler for the functional programming language Haskell.
It provides a cross-platform environment for the writing and testing of Haskell code and it supports numerous extension ...
supports both ''type synonym families'' and ''data families''. Type synonym families are the more flexible (but harder to type-check) form, permitting the types in the
codomain
In mathematics, the codomain or set of destination of a function is the set into which all of the output of the function is constrained to fall. It is the set in the notation . The term range is sometimes ambiguously used to refer to either ...
of the type function to be any type whatsoever with the appropriate
kind.
Data families, on the other hand, restrict the codomain by requiring each instance to define a new
type constructor
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. So ...
for the function's result. This ensures that the function is
injective
In mathematics, an injective function (also known as injection, or one-to-one function) is a function that maps distinct elements of its domain to distinct elements; that is, implies . (Equivalently, implies in the equivalent contraposi ...
, allowing clients' contexts to deconstruct the type family and obtain the original argument type.
Motivation and examples
Type families are useful in abstracting patterns where a common "organization" or "structure" of types is repeated, but with different specific types in each case. Typical use cases include describing
abstract data type
In computer science, an abstract data type (ADT) is a mathematical model for data types. An abstract data type is defined by its behavior (semantics) from the point of view of a '' user'', of the data, specifically in terms of possible values, po ...
s like generic collections, or
design pattern
A design pattern is the re-usable form of a solution to a design problem. The idea was introduced by the architect Christopher Alexander and has been adapted for various other disciplines, particularly software engineering. The " Gang of Four" b ...
s like
model–view–controller
Model–view–controller (MVC) is a software architectural pattern commonly used for developing user interfaces that divide the related program logic into three interconnected elements. This is done to separate internal representations of infor ...
.
Self-optimizing abstract data types
One of the original motivations for the introduction of associated types was to allow
abstract data type
In computer science, an abstract data type (ADT) is a mathematical model for data types. An abstract data type is defined by its behavior (semantics) from the point of view of a '' user'', of the data, specifically in terms of possible values, po ...
s to be
parameterized by their content type such that the
data structure
In computer science, a data structure is a data organization, management, and storage format that is usually chosen for Efficiency, efficient Data access, access to data. More precisely, a data structure is a collection of data values, the rel ...
implementing the abstract type varies in a "self-optimizing" way.
Normal
algebraic data type
In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.
Two common classes of algebraic types are product types (i.e., ...
parameters can only describe data structures that behave uniformly with respect to all argument types. Associated types, however, can describe a family of data structures that have a uniform interface but vary in implementation according to one or more type parameters. For example,
using Haskell's associated types notation, we can declare a type class of valid
array
An array is a systematic arrangement of similar objects, usually in rows and columns.
Things called an array include:
{{TOC right
Music
* In twelve-tone and serial composition, the presentation of simultaneous twelve-tone sets such that the ...
element types, with an associated data family representing an array of that element type:
class ArrayElem e where
data Array e
index :: Array e -> Int -> e
Instances can then be defined for this class, which define both the data structure used and the operations on the data structure in a single location. For efficiency, we might use a packed
bit vector
A bit array (also known as bitmask, bit map, bit set, bit string, or bit vector) is an array data structure that compactly stores bits. It can be used to implement a simple set data structure. A bit array is effective at exploiting bit-level p ...
representation for arrays of
Boolean values, while using a normal
array data structure
In computer science, an array is a data structure consisting of a collection of ''elements'' ( values or variables), each identified by at least one ''array index'' or ''key''. An array is stored such that the position of each element can be c ...
for integer values. The data structure for arrays of
ordered pair
In mathematics, an ordered pair (''a'', ''b'') is a pair of objects. The order in which the objects appear in the pair is significant: the ordered pair (''a'', ''b'') is different from the ordered pair (''b'', ''a'') unless ''a'' = ''b''. (In co ...
s is defined recursively as a pair of arrays of each of the element types.
instance ArrayElem Bool where
data Array Bool = BoolArray BitVector
index (BoolArray ar) i = indexBitVector ar i
instance ArrayElem Int where
data Array Int = IntArray UIntArr
index (IntArray ar) i = indexUIntArr ar i
instance (ArrayElem a, ArrayElem b) => ArrayElem (a, b) where
data Array (a, b) = PairArray (Array a) (Array b)
index (PairArray ar br) = (index ar i, index br i)
With these definitions, when a client refers to an
Array (Int, Bool)
, an implementation is automatically selected using the defined instances.
A class for collections
Inverting the previous example, we can also use type families to define a class for collection types, where the type function maps each collection type to its corresponding element type:
class Collects c where
type Elem c
empty :: c
insert :: Elem c -> c -> c
toList :: c -> lem cinstance Collects where
type Elem = e
empty = []
insert = (:)
toList = id
instance Ord e => Collects (Set.Set e) where
type Elem (Set.Set e) = e
empty = Set.empty
insert = Set.insert
toList = Set.toList
In this example, the use of a type synonym family instead of a data family is essential, since multiple collection types may have the same element type.
Comparison with functional dependencies
Functional dependencies are another type system feature that have similar uses to associated types. While an associated type adds a named type function mapping the enclosing type class's parameters to another type, a functional dependency lists the result type as another parameter of the type class and adds a constraint between the type parameters (e.g. "parameter ''a'' uniquely determines parameter ''b''", written
a -> b
). The most common uses of functional dependencies can be directly converted to associated types and vice versa.
Type families are regarded as being generally easier to type-check than functional dependencies. Another advantage of associated types over functional dependencies is that the latter requires clients using the type class to state all of the dependent types in their contexts, including ones they do not use; since associated types do not require this, adding another associated type to the class requires updating only the class's instances, while clients can remain unchanged. The main advantages of functional dependencies over type families are in their added flexibility in handling a few unusual cases.
References
{{Reflist
External links
Haskell Wiki documentation on using type families in GHC
Functional programming
Type theory
Data types
Articles with example Haskell code