Maths - Product Types

Product Type

Has one constructor (formation) and multiple ways of deconstructing (elimination) (projections).


product type


In type theory the product of A and B is denoted A×B. In logic the product is 'and' often denoted /\ .

An element of A×B is denoted (a,b) where 'a' is an element of 'A' and 'b' is an element of 'B'.


Types are defined by their formation, term introduction, term eliminator and computation rules:

Introduction Elimination

This is discussed on the propositional logic page here.

In type theory types are defined in terms of:

  • Type formation
  • Term introduction
  • Term Elimination

This picture shows how programming language constructs (In this case: Idris) relate to this theory:

product type as pair

β-reduction and η-reduction


construction followed by deconstruction:


deconstruction followed by construction:

Implementations in Idris

Product terms can be defined using 'data' but there is also a specific mechanism for products using 'record'.

Here we start with a product type 'M'. We can deconstruct it by using 'fst' and 'snd' then construct it to get back to 'M'
Idris> :let M = MkPair 2 "2"
Idris> MkPair (fst M) (snd M)
(2, "2") : (Integer, String)
Here we start with two terms 'x' and 'y' if we first construct using MkPair then deconstruct we get back to 'x' and 'y'.
Idris> :let x = 3
Idris> :let y = "3"
Idris> fst (MkPair x y)
3 : Integer
Idris> snd (MkPair x y)
"3" : String

Other implementations of product


We can have a type which corresponds to conjunction:

data And : Type -> Type -> Type where
   AndIntro : a -> b -> A a b

from : Idris-dev/libs/prelude/Builtins.idr

  ||| The non-dependent pair type, also known as conjunction.
  ||| @A the type of the left elements in the pair
  ||| @B the type of the right elements in the pair
  data Pair : (A : Type) -> (B : Type) -> Type where
     ||| A pair of elements
     ||| @a the left element of the pair
     ||| @b the right element of the pair
MkPair : {A, B : Type} -> (1 a : A) -> (1 b : B) -> Pair A B
from : Idris-dev/libs/prelude/ Prelude/Basics.idr
||| Return the first element of a pair.
fst : (a, b) -> a
fst (x, y) = x

||| Return the second element of a pair.
snd : (a, b) -> b
snd (x, y) = y


from : coq/theories/Init/Datatypes.v

(** [prod A B], written [A * B], is the product of [A] and [B];
    the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)

Inductive prod (A B:Type) : Type :=
  pair : A -> B -> A * B

where "x * y" := (prod x y) : type_scope.

Add Printing Let prod.

Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.

Arguments pair {A B} _ _.

Register prod as
Register pair as
Register prod_rect as

Section projections.
  Context {A : Type} {B : Type}.

  Definition fst (p:A * B) := match p with (x, y) => x end.
  Definition snd (p:A * B) := match p with (x, y) => y end.

  Register fst as
  Register snd as
End projections.


In logic the product is 'and' denoted /\

Relationship to Category Theory

Category theory is deeply related to type theory.

On this page is product is approached from the category theory direction and on this page is generalsed to the concept of a limit.

Next Steps

Other types are discussed on the following pages:

metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.


Terminology and Notation

Specific to this page here:


This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2021 Martin John Baker - All rights reserved - privacy policy.