Codex @codex  0

 Incoming links: Function type

Data type 2026-10-31

A classification of program values together with the operations permitted on them. An algebraic data type describes values by data constructors; a function type describes acceptable arguments and produced results.

 Read the full article

Function type 2026-10-13

 View more

A function type

τ_{1} \to τ_{2}

classifies functions that accept arguments of type

τ_{1}

and produce results of type

τ_{2}

if they return. For example,

λ x . x + 1

has function type

int \to int

in our teaching programming language, while

λb . if b then 1 else 2

has function type

bool \to int

. A function type specifies how a function may be used; it does not guarantee that a call returns.

Figure 1.
Checking an integer function call from its parts
. An addition rule checks the body of a lambda abstraction, the abstraction rule gives its function type, and lambda application checks the argument and obtains the result type. Arrows run from prerequisite typing judgments to their conclusions. **Details**.

The two central typing judgment rules are

\frac{Γ , x : τ _{1} ⊢ e : τ _{2}}{Γ ⊢ λ x . e : τ _{1} \to τ _{2}}, \frac{Γ ⊢ f : τ _{1} \to τ _{2} Γ ⊢ a : τ _{1}}{Γ ⊢ f a : τ _{2}} .

(1)

The lambda abstraction rule checks the body under an extended typing context; the lambda application rule checks that the argument has exactly the required type. These rules describe our simple type examples. ^[ref]

For

(λ x . x + 1) 3

, assume

x : int

; both

x

and

1

have type int, so

x + 1

has type int. The abstraction therefore has function type

int \to int

. Since

3

has type int, the call has type int and evaluates to

4

. Replacing

3

by true fails the argument requirement. This local derivation explains each step without running the program.

Arrows associate to the right:

τ_{1} \to τ_{2} \to τ_{3}

means

τ_{1} \to (τ_{2} \to τ_{3})

, a function returning another function. For instance,

λ x . λ y . x + y

has function type

int \to (int \to int)

. Supplying one integer yields a function awaiting the second. Functions can also be arguments:

(int \to int) \to int

accepts an integer-to-integer function and has an integer result type.

// Target: computer-science.bigb

 Read the full article

Hindley-Milner type system 2026-10-13

 View more

The pure Hindley-Milner type system combines function types, type inference and let polymorphism. It solves constraints by type unification and generalizes eligible type variables at let bindings. Robin Milner's 1978 paper presents Algorithm W and proves its soundness for the paper's language; it also acknowledges Roger Hindley's earlier work on finding general types. ^[ref]

 Read the full article

Kind (type theory) 2026-10-31

 View more

A classification of type-level expressions. In the traditional Haskell notation, ordinary types have kind *, while a unary type constructor such as Tree has kind * -> *. Applying it to a suitable type argument produces an ordinary type. This distinguishes the type-level application from applying a value with a function type.

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 2 / b / Solution 2026-10-31

 View more

Choose

⋆

as the domain of the new function type. Since

x \in / Subjects (Γ)

, the assumption

x : ⋆

is consistent with

Γ

and deleting

x

leaves

Γ

unchanged. The lambda abstraction rule gives

\frac{Γ \mapsto p : A}{Γ \mapsto λ x . p : ⋆ \Rightarrow A} .

(1)

Use the universal typing axiom for

q

, then the lambda application rule:

\frac{Γ \mapsto λ x . p : ⋆ \Rightarrow A \emptyset \mapsto q : ⋆}{Γ \mapsto ( λ x . p ) q : A} .

(2)

Therefore

Γ \mapsto (λ x . p) q : A for every q .

(3)

The condition is about the typing context, not the free variables of

p

. Some occurrences of

x

p

might have been hidden by a use of the universal typing axiom; the derivation above still follows the printed rules.

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 2 / c / Solution 2026-10-31

 View more

Begin with the variable typing judgment

{x : A} \mapsto x : A

. Because

z

is absent from this typing context, the lambda abstraction rule permits

z

to have type

⋆

\frac{{ x : A } \mapsto x : A}{{ x : A } \mapsto λ z . x : ⋆ \Rightarrow A} .

(1)

Assign the entire lambda application

y x

type

⋆

using the universal typing axiom, without attempting to assign a function type to

y

. Then

\frac{{ x : A } \mapsto λ z . x : ⋆ \Rightarrow A \emptyset \mapsto y x : ⋆}{{ x : A } \mapsto ( λ z . x ) ( y x ) : A} .

(2)

Although

y

is a free variable of the body, it is absent from its recorded typing context. Consequently the lambda abstraction rule allows any simple type

B

for

y

. Abstract over

y

and then

x

\frac{\frac{{ x : A } \mapsto ( λ z . x ) ( y x ) : A}{{ x : A } \mapsto λ y . ( λ z . x ) ( y x ) : B \Rightarrow A}}{\emptyset \mapsto λ x y . ( λ z . x ) ( y x ) : A \Rightarrow ( B \Rightarrow A )} .

(3)

The side condition for

y

holds because

y

is absent; the side condition for

x

holds because its recorded simple type is

A

. Thus

\emptyset \mapsto λ x y . (λ z . x) (y x) : A \Rightarrow (B \Rightarrow A) for all A, B in TA_{λ}^{⋆} .

(4)

 Read the full article

Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 2 / d / Solution 2026-10-31

 View more

The exact restriction in the ordinary simply typed lambda calculus is

\emptyset \mapsto λ x y . (λ z . x) (y x) : A \Rightarrow (B \Rightarrow A) ⟺ B = A \Rightarrow C for some simple type C .

(1)

Thus the unrestricted choice of

A, B

available in part (c) fails. A reading of the printed sentence as asserting impossibility for every choice of

A, B

is false. This issue occurs in the original PDF as well as its transcription.^[ref]

To prove necessity, first observe why the ordinary rules cannot hide assumptions. Structural induction on a derivation proves

Subjects (Γ) = F V (t) whenever Γ \mapsto t : T .

(2)

For a variable, both sides are the singleton containing that variable. For lambda application, both sides are the union of the two premise supports. For lambda abstraction, both sides delete the bound variable. There is no universal typing axiom to interrupt this equality.

Now invert the proposed derivation. Each outer lambda abstraction must have been introduced by the abstraction rule, since the other ordinary rules conclude a variable or a lambda application. The body must therefore have the typing judgment

{x : A, y : B} \mapsto (λ z . x) (y x) : A .

(3)

The support equality just proved ensures that both displayed assumptions occur; consistency fixes their simple types to those specified by the outer function type. Inverting the lambda application gives a simple type

C

for its argument and the following premises:

{x : A} \mapsto λ z . x : C \Rightarrow A, {x : A, y : B} \mapsto y x : C .

(4)

There is no flexibility in the supports:

λ z . x

has the single free variable

x

, whereas

y x

has both free variables

y, x

. Invert the second lambda application. Its two premises must be

{y : B} \mapsto y : D \Rightarrow C, {x : A} \mapsto x : D

(5)

for some simple type

D

. The variable rule is the only possible final rule for each premise. It forces

D = A

and

B = D \Rightarrow C

, yielding

B = A \Rightarrow C

Conversely, suppose

B = A \Rightarrow C

. The ordinary rules give

\frac{{ y : A \Rightarrow C } \mapsto y : A \Rightarrow C { x : A } \mapsto x : A}{{ x : A , y : A \Rightarrow C } \mapsto y x : C}, \frac{{ x : A } \mapsto x : A}{{ x : A } \mapsto λ z . x : C \Rightarrow A} .

(6)

The typing contexts are consistent, so another lambda application gives the body type

A

. Two lambda abstractions discharge

y

and

x

, establishing

\emptyset \mapsto λ x y . (λ z . x) (y x) : A \Rightarrow ((A \Rightarrow C) \Rightarrow A) .

(7)

This proves sufficiency and supplies a family of counterexamples to the literal impossibility claim. For a concrete failure of the unrestricted claim, choose

A = α

and

B = β

as atomic type variables. The type variable

β

is not a function type

α \Rightarrow C

, so no derivation exists for that fixed pair. Here the atomic type variables are fixed type expressions, rather than unknowns that one may change during type inference.

The reason for the restriction is the otherwise discarded lambda application

y x

: the ordinary rules still type-check it. Its subsequent disappearance under beta reduction does not license reversing that beta reduction while preserving every simple type of the result. The beta-normal form

λ x y . x

admits arbitrary

A \Rightarrow (B \Rightarrow A)

, whereas the unreduced lambda term has the additional constraint just derived.

The all- A, B claim fails; the valid instances have B = A \Rightarrow C .

(8)

 Read the full article

Past exam of the mathematics course of the University of Cambridge / 2007 / ia / Paper 5 / 10 / a / Solution Created 2026-09-24 Updated 2026-10-14

 View more

Represent the two constructors of the type grammar by subclasses of MLType: a TypeVar node and an Arrow node containing two types. Use immutable fields so a completed type expression cannot acquire cycles through later mutation. The static factory allocates a fresh object and gives it a fresh identifier shared across the whole hierarchy:

import java.math.BigInteger;

public abstract class MLType {
    private MLType() { }
    private static BigInteger next = BigInteger.ONE;

    public static synchronized TypeVar createNewTypeVar() {
        TypeVar answer = new TypeVar(next);
        next = next.add(BigInteger.ONE);
        return answer;
    }
    public static final class TypeVar extends MLType {
        private final BigInteger id;
        private TypeVar(BigInteger id) { this.id = id; }
    }
    public static final class Arrow extends MLType {
        private final MLType from, to;
        public Arrow(MLType from, MLType to) {
            if (from == null || to == null)
                throw new IllegalArgumentException();
            this.from = from; this.to = to;
        }
    }
}

The nested classes are public for use by clients, while their fields are private; TypeVar can be created only through the factory. Client code uses MLType.TypeVar and MLType.Arrow. A type variable is identified by its unique node, and a function type by its domain and codomain nodes; repeated occurrences of one logical variable share the same TypeVar object.

The monotonically increasing BigInteger identifier avoids fixed-width counter overflow, and synchronization prevents two simultaneous calls from receiving the same identifier. Actual allocation remains subject to available memory. This is an abstract syntax tree representation, possibly sharing subexpressions. Fresh variable nodes and recursive arrow nodes represent every type in the given grammar.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 1 / b / ii / Solution 2026-10-31

 View more

Both uses of x in this definition have the same monomorphic type within the body. Write x :: u -> v. The inner application x z forces z :: u and has type v; the outer application x (x z) forces v = u. Thus x :: u -> u. Finally, x (x z) is applied to y, so u must itself be a function type, say a -> b. This gives

f :: ((a -> b) -> a -> b) -> a -> (a -> b) -> b
f x y z = x (x z) y

The principal type is therefore

((α \to β) \to (α \to β)) \to α \to (α \to β) \to β .

(1)

The argument x transforms a function into another function of the same type. The body transforms z twice, then applies the resulting function to y; no recursive type equation is required.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Imperative programming / 6 / c / Solution 2026-10-31

 View more

A simple current-value implementation works when

f

is a pure function, but sharing a mutable closure between copies would violate the independence requirement used in part (d). Use a memoized successor chain for stateful iterator copies: the generated sequence has shared cells, and each iterator has its own current-cell pointer.

object FunIter {
  final class Cell[T](val head: T, f: T => T) {
    lazy val tail: Cell[T] = new Cell[T](f(head), f)
  }
}

class FunIter[T](v: T, f: T => T) extends Iter[T] {
  private var cursor = new FunIter.Cell[T](v, f)

  def hasNext: Boolean = true

  def next(): T = {
    val x = cursor.head
    cursor = cursor.tail
    x
  }

  def copy(): Iter[T] = {
    val result = new FunIter[T](cursor.head, f)
    result.cursor = cursor
    result
  }
}

The representation invariant is that cursor points to the next cell to be returned, and each cell's lazy tail is computed at most once. The abstraction function is the infinite sequence of heads starting at that cell. Advancing changes only this iterator's pointer. A copy starts at the same cell, so both observe the same remaining heads even when their calls are interleaved:

n e x t returns v, f (v), f (f (v)), \dots; co p y preserves an independent position .

(1)

For a stateful

f

, the generator state must be privately owned by this shared chain; unrelated external calls to

f

must not change it. As usual, the values and transition must allow successive results to be observed without externally mutating old results. No interface can independently clone the hidden state of an arbitrary externally mutated closure from its function type alone. The chain avoids needing such cloning: a lagging copy reuses the already generated future instead of invoking

f

again.

Each new cell needs one transition and constant bookkeeping, but retained slower copies can keep a long generated prefix alive. This is an intentional space tradeoff that permits the stateful generator in part (d). No output is possible if computing a demanded transition itself fails or diverges.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Functional programming, design and analysis of algorithms / 1 / a / Solution 2026-10-31

 View more

Tree is a type constructor, taking the element type parameter a to the algebraic data type Tree a. It is not a value and has no ordinary value-level function type; its kind of a type is * -> *. The other names are data constructors with polymorphic type signatures:

One :: a -> Tree a
Two :: Tree a -> Tree a -> Tree a

One constructs a leaf-labelled binary tree with one leaf; Two joins two such trees under a new internal node. Unlike a general binary tree representation with empty child slots, this representation has no empty tree.^[ref]

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 1 / b / Solution 2026-10-25

 View more

Take compatible function types f :: b -> c, g :: b -> a -> b, and h :: c -> a -> c. The necessary conditions obtained from the two induction base cases are strictness of f and the fusion equation

f (⊥) = ⊥, f (g x y) = h (f x) y for all x, y .

(1)

At zs = [], the desired equation is exactly the displayed fusion equation. At zs = undefined, both left folds diverge because their list argument has no outer constructor; the equation therefore requires f undefined = undefined. This is the strict function condition. If only finite total spines were considered, the first condition would not be necessary.

These conditions also support the step. The induction hypothesis must hold for every accumulator and element. For z:zs, instantiate that hypothesis at g x y and z:

f (foldl g (g x y) (z:zs))
 = f (foldl g (g (g x y) z) zs)
 = foldl h (h (f (g x y)) z) zs
 = foldl h (h (h (f x) y) z) zs
 = foldl h (h (f x) y) (z:zs).

The middle rewrite uses the fusion equation at x,y. For pure computable functions, equality on infinite spines follows from finite approximations as in part (a).

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 1 / e / Solution 2026-10-25

 View more

Change the right fold's result type to an accumulator-transforming function type:

foldlAsFoldr :: (b -> a -> b) -> b -> [a] -> b
foldlAsFoldr s n xs = foldr c id xs n
  where
    c x k a = k (s a x)

Thus c x k = \a -> k (s a x) and k = id in the question's notation. Here c :: a -> (b -> b) -> (b -> b), and the fold's base value is the identity function, not the initial accumulator n.

The recursion invariant is foldr c id xs a = foldl s a xs for every a. For [], both sides equal a. For a cons:

foldr c id (x:xs) a
 = c x (foldr c id xs) a
 = foldr c id xs (s a x)
 = foldl s (s a x) xs
 = foldl s a (x:xs).

At an undefined spine, applying the undefined folded function also gives the bottom value. The finite-approximation argument then covers infinite lazy lists. This is a continuation representation of a left fold: the result retains the operation still to be performed, avoiding the information loss in part (d).

 Read the full article

Programming language Created 2026-10-13 Updated 2026-10-14

 View more

A programming language specifies how programs are written and what their execution means. Its type system describes which operations may be combined; an abstract syntax tree records the structure on which these rules act. The examples under type system use a small teaching language with integers, Boolean values and function types.

// Target: computer-science.bigb

 Read the full article

Simple type Created 2026-10-13 Updated 2026-10-24

 View more

In the examples here, a simple type is a finite expression built from the base types int and bool using function types:

τ ::= int ∣ bool ∣ (τ \to τ) .

(1)

For example,

int \to bool

describes a function accepting an integer and producing a Boolean value. During type inference, the grammar is extended with type variables such as

α

for types not yet determined. A type scheme additionally binds such type variables; it is distinct from the individual simple type used at one call.

 Read the full article

Tree fold Created 2026-10-24 Updated 2026-10-31

 View more

A structural recursion replacing the empty binary tree by a value and a nonempty node by a combining function on its two folded children and root label. The result type may itself be a function type, allowing a fold to construct a membership predicate or a difference list rather than traversing all branches for every subsequent query.

More generally, choose one operation for each data constructor. For a leaf-labelled binary tree represented by One a | Two (Tree a) (Tree a), the tree fold instead has type signature (a -> b) -> (b -> b -> b) -> Tree a -> b: one operation handles the leaf label, and the other combines the two folded children. Replacing the operations by the original data constructors reconstructs the input, as structural induction proves.

 Read the full article

Type scheme 2026-10-14

 View more

A type scheme binds type variables that may be instantiated independently at different uses. The identity function has type scheme

\forall α . α \to α

: choose one type per use, then use that same choice on both sides of its function type. A free type variable shared with the typing context is not automatically such an independently selectable parameter.

 Read the full article

Type system 2026-10-13

 View more

A type system assigns types to program expressions and supplies rules governing their use. A type constrains permitted operations: in our teaching programming language, int admits integer addition, bool supplies true and false for conditions, and a function type specifies an argument type and a result type. Storage as bits alone does not explain these distinctions; the type system determines whether an expression can serve as an argument, a condition or an operand.

A typing judgment

Γ ⊢ e : τ

says that expression

e

has type

τ

under the assumptions in the typing context

Γ

. For example,

Γ = {x : int, y : int}, Γ ⊢ x + y : int .

(1)

The assumptions give each operand type int; the addition rule then gives the sum type int. Changing

y

to type bool prevents this derivation. Our teaching programming language has distinct int and bool types and no implicit conversions between them.

The conditional rule requires a Boolean condition and the same type for both branches:

\frac{Γ ⊢ c : bool Γ ⊢ e _{1} : τ Γ ⊢ e _{2} : τ}{Γ ⊢ if c then e _{1} else e _{2} : τ} .

(2)

Thus if true then 1 else 2 has type int, while if true then 1 else false is rejected: its branches would require

τ = int

and

τ = bool

simultaneously. Even a branch that will not execute is checked by this rule. This is a rule of this particular type system; a different programming language can choose different rules. ^[ref]

The useful feature is compositional reasoning: after checking the parts, a rule explains how to check the whole. The function type diagram shows this for a call. Type inference can discover the required types automatically, and type variables let one express relationships that recur across many concrete types. The result is both a practical early error detector and a small, readable derivation explaining why an expression fits its intended use.

The guarantee depends on the rules and execution model. Type safety can exclude specified failures such as adding a Boolean or calling an integer as a function. It does not by itself establish every desired runtime property or guarantee that execution terminates. A type system that permits unrestricted recursion can accept a computation that runs forever; exception handling also needs its own account of permitted outcomes.

 Read the full article

Type unification Created 2026-10-14 Updated 2026-10-25

 View more

Type unification finds a type substitution making specified type expressions equal, or reports incompatible constraints. In our simple type grammar, matching two function types reduces to matching their argument types and their result types. Distinct base types int and bool fail to match; solving a type variable against a nontrivial type expression uses the occurs check.

// Target: computer-science.bigb

 Read the full article

Type variable 2026-10-13

 View more

A type variable is a placeholder for a type. In a function type

α \to α

, the repeated type variable requires the argument and result types to agree;

α \to β

does not impose that agreement. A type substitution replacing

α

by int changes

α \to α

int \to int

everywhere within that instance.

For the identity function written as the lambda abstraction

λ x . x

, assume

x : α

in the body. Looking up

x

gives result type

α

, so the abstraction rule gives

λ x . x : α \to α

. In the pure Hindley-Milner type system, let identity = λx.x in ... gives identity the type scheme

\forall α . α \to α

by let polymorphism. Each use receives fresh type variables: identity 3 chooses int for its instance, and identity true chooses bool for a separate instance. These choices do not change the original type scheme.

Figure 1.
Independent type instantiations of a let-bound identity function
. The type scheme stays general while two uses receive different type substitutions. Each use preserves the equality of its own argument and result types. **Details**.

For example, let identity = λx.x in let a = identity 3 in identity true is valid and has type bool. By contrast, (λf. let a = f 3 in f true) (λx.x) is rejected by the Hindley-Milner type system: the lambda abstraction binds f to one monomorphic function type. The first call requires its argument type to be int, and the second requires that same type to be bool. Naming the first result with let a does not generalize f. The distinction makes reusable code possible while keeping the assumptions about a supplied argument consistent.

// Target: computer-science.bigb

 Read the full article