Dependent type theory and 'arbitrary' type functions
My first answer to this question was high on concepts and low on details and reflected on the subquestion, 'what is going on?'; this answer will be the same but focused on the subquestion, 'can we get arbitrary type functions?'.
One extension to the algebraic operations of sum and product are the so called 'large operators', which represent the sum and product of a sequence (or more generally, the sum and product of a function over a domain) usually written Σ and Π respectively. See Sigma Notation.
So the sum
a₀ + a₁X + a₂X² + ...
might be written
Σ[i ∈ ℕ]aᵢXⁱ
where a is some sequence of real numbers, for example. The product would be represented similarly with Π instead of Σ.
When you look from a distance, this kind of expression looks a lot like an 'arbitrary' function in X; we are limited of course to expressible series, and their associated analytic functions. Is this a candidate for a representation in a type theory? Definitely!
The class of type theories which have immediate representations of these expressions is the class of 'dependent' type theories: theories with dependent types. Naturally we have terms dependent on terms, and in languages like Haskell with type functions and type quantification, terms and types depending on types. In a dependent setting, we additionally have types depending on terms. Haskell is not a dependently typed language, although many features of dependent types can be simulated by torturing the language a bit.
Curry-Howard and dependent types
The 'Curry-Howard isomorphism' started life as an observation that the terms and type-judging rules of simply-typed lambda calculus correspond exactly to natural deduction (as formulated by Gentzen) applied to intuitionistic propositional logic, with types taking the place of propositions, and terms taking the place of proofs, despite the two being independently invented/discovered. Since then, it has been a huge source of inspiration for type theorists. One of the most obvious things to consider is whether, and how, this correspondence for propositional logic can be extended to predicate or higher order logics. Dependent type theories initially arose from this avenue of exploration.
For an introduction to the Curry-Howard isomorphism for simply-typed lambda calculus, see here. As an example, if we want to prove A ∧ B we must prove A and prove B; a combined proof is simply a pair of proofs: one for each conjunct.
In natural deduction:
Γ ⊢ A Γ ⊢ B
Γ ⊢ A ∧ B
and in simply-typed lambda calculus:
Γ ⊢ a : A Γ ⊢ b : B
Γ ⊢ (a, b) : A × B
Similar correspondences exist for ∨ and sum types, → and function types, and the various elimination rules.
An unprovable (intuitionistically false) proposition corresponds to an uninhabited type.
With the analogy of types as logical propositions in mind, we can start to consider how to model predicates in the type-world. There are many ways in which this has been formalised (see this introduction to Martin-Löf's Intuitionistic Type Theory for a widely-used standard) but the abstract approach usually observes that a predicate is like a proposition with free term variables, or, alternatively, a function taking terms to propositions. If we allow type expressions to contain terms, then a treatment in lambda calculus style immediately presents itself as a possibility!
Considering only constructive proofs, what constitutes a proof of ∀x ∈ X.P(x)? We can think of it as a proof function, taking terms (x) to proofs of their corresponding propositions (P(x)). So members (proofs) of the type (proposition) ∀x : X.P(x) are 'dependent functions', which for each x in X give a term of type P(x).
What about ∃x ∈ X.P(x)? We need any member of X, x, together with a proof of P(x). So members (proofs) of the type (proposition) ∃x : X.P(x) are 'dependent pairs': a distinguished term x in X, together with a term of type P(x).
Notation:
I will use
∀x ∈ X...
for actual statements about members of the class X, and
∀x : X...
for type expressions corresponding to universal quantification over type X. Likewise for ∃.
Combinatorial considerations: products and sums
As well as the Curry-Howard correspondence of types with propositions, we have the combinatorial correspondence of algebraic types with numbers and functions, which is the main point of this question. Happily, this can be extended to the dependent types outlined above!
I will use the modulus notation
|A|
to represent the 'size' of a type A, to make explicit the correspondence outlined in the question, between types and numbers. Note that this is a concept outside of the theory; I do not claim that there need be any such operator within the language.
Let us count the possible (fully reduced, canonical) members of type
∀x : X.P(x)
which is the type of dependent functions taking terms x of type X to terms of type P(x). Each such function must have an output for every term of X, and this output must be of a particular type. For each x in X, then, this gives |P(x)| 'choices' of output.
The punchline is
|∀x : X.P(x)| = Π[x : X]|P(x)|
which of course doesn't make huge deal of sense if X is IO (), but is applicable to algebraic types.
Similarly, a term of type
∃x : X.P(x)
is the type of pairs (x, p) with p : P(x), so given any x in X we can construct an appropriate pair with any member of P(x), giving |P(x)| 'choices'.
Hence,
|∃x : X.P(x)| = Σ[x : X]|P(x)|
with the same caveats.
This justifies the common notation for dependent types in theories using the symbols Π and Σ, and indeed many theories blur the distinction between 'for all' and 'product' and between 'there is' and 'sum', due to the above-mentioned correspondences.
We are getting close!
Vectors: representing dependent tuples
Can we now encode numerical expressions like
Σ[n ∈ ℕ]Xⁿ
as type expressions?
Not quite. While we can informally consider the meaning of expressions like Xⁿ in Haskell, where X is a type and n a natural number, it's an abuse of notation; this is a type expression containing a number: distinctly not a valid expression.
On the other hand, with dependent types in the picture, types containing numbers is precisely the point; in fact, dependent tuples or 'vectors' are a very commonly-cited example of how dependent types can provide pragmatic type-level safety for operations like list access. A vector is just a list along with type-level information regarding its length: precisely what we are after for type expressions like Xⁿ.
For the duration of this answer, let
Vec X n
be the type of length-n vectors of X-type values.
Technically n here is, rather than an actual natural number, a representation in the system of a natural number. We can represent natural numbers (Nat) in Peano style as either zero (0) or the successor (S) of another natural number, and for n ∈ ℕ I write ˻n˼ to mean the term in Nat which represents n. For example, ˻3˼ is S (S (S 0)).
Then we have
|Vec X ˻n˼| = |X|ⁿ
for any n ∈ ℕ.
Nat types: promoting ℕ terms to types
Now we can encode expressions like
Σ[n ∈ ℕ]Xⁿ
as types. This particular expression would give rise to a type which is of course isomorphic to the type of lists of X, as identified in the question. (Not only that, but from a category-theoretic point of view, the type function - which is a functor - taking X to the above type is naturally isomorphic to the List functor.)
One final piece of the puzzle for 'arbitrary' functions is how to encode, for
f : ℕ → ℕ
expressions like
Σ[n ∈ ℕ]f(n)Xⁿ
so that we can apply arbitrary coefficients to a power series.
We already understand the correspondence of algebraic types with numbers, allowing us to map from types to numbers and type functions to numerical functions. We can also go the other way! - taking a natural number, there is obviously a definable algebraic type with that many term members, whether or not we have dependent types. We can easily prove this outside of the type theory by induction. What we need is a way to map from natural numbers to types, inside the system.
A pleasing realisation is that, once we have dependent types, proof by induction and construction by recursion become intimately similar - indeed they are the very same thing in many theories. Since we can prove by induction that types exist which fulfil our needs, should we not be able to construct them?
There are several ways to represent types at the term level. I will use here an imaginary Haskellish notation with * for the universe of types, itself usually considered a type in a dependent setting.1
Likewise, there are also at least as many ways to notate 'ℕ-elimination' as there are dependent type theories. I will use a Haskellish pattern-matching notation.
We need a mapping, α from Nat to *, with the property
∀n ∈ ℕ.|α ˻n˼| = n.
The following pseudodefinition suffices.
data Zero -- empty type
data Successor a = Z | Suc a -- Successor ≅ Maybe
α : Nat -> *
α 0 = Zero
α (S n) = Successor (α n)
So we see that the action of α mirrors the behaviour of the successor S, making it a kind of homomorphism. Successor is a type function which 'adds one' to the number of members of a type; that is, |Successor a| = 1 + |a| for any a with a defined size.
For example α ˻4˼ (which is α (S (S (S (S 0))))), is
Successor (Successor (Successor (Successor Zero)))
and the terms of this type are
Z
Suc Z
Suc (Suc Z)
Suc (Suc (Suc Z))
giving us exactly four elements: |α ˻4˼| = 4.
Likewise, for any n ∈ ℕ, we have
|α ˻n˼| = n
as required.
- Many theories require that the members of
* are mere representatives of types, and an operation is provided as an explicit mapping from terms of type * to their associated types. Other theories permit the literal types themselves to be term-level entities.
'Arbitrary' functions?
Now we have the apparatus to express a fully general power series as a type!
The series
Σ[n ∈ ℕ]f(n)Xⁿ
becomes the type
∃n : Nat.α (˻f˼ n) × (Vec X n)
where ˻f˼ : Nat → Nat is some suitable representation within the language of the function f. We can see this as follows.
|∃n : Nat.α (˻f˼ n) × (Vec X n)|
= Σ[n : Nat]|α (˻f˼ n) × (Vec X n)| (property of ∃ types)
= Σ[n ∈ ℕ]|α (˻f˼ ˻n˼) × (Vec X ˻n˼)| (switching Nat for ℕ)
= Σ[n ∈ ℕ]|α ˻f(n)˼ × (Vec X ˻n˼)| (applying ˻f˼ to ˻n˼)
= Σ[n ∈ ℕ]|α ˻f(n)˼||Vec X ˻n˼| (splitting product)
= Σ[n ∈ ℕ]f(n)|X|ⁿ (properties of α and Vec)
Just how 'arbitrary' is this? We are limited not only to integer coefficients by this method, but to natural numbers. Apart from that, f can be anything at all, given a Turing Complete language with dependent types, we can represent any analytic function with natural number coefficients.
I haven't investigated the interaction of this with, for example, the case provided in the question of List X ≅ 1/(1 - X) or what possible sense such negative and non-integer 'types' might have in this context.
Hopefully this answer goes some way to exploring how far we can go with arbitrary type functions.
Branch x (Branch y Nil Nil) Nilor it looks likeBranch x Nil (Branch y Nil Nil). – Chris Taylorundefined,throw, etc. We should use it. – Philip JF