New answers tagged type-theory
2
There are various ways to define contexts in type theories. In this style, we assume there is some infinite set of variable names $V$ and define the context $\Gamma : V \rightharpoonup S$ as a partial function from the set of variable names to the set of types. $\mathrm{dom}(\Gamma)$ is then the subset of $V$ on which $\Gamma$ is defined, i.e. the variables ...
3
The initial assumption about such types having at most countably many elements is false. We can use inductive types to define a non-countable type, namely the countably branching trees:
(* Countably branching trees. *)
Inductive Tree : Type :=
| Leaf : Tree
| Node : (nat -> Tree) -> Tree.
Lemma nocycle (t : Tree) : forall (f : nat -> Tree), t = ...
Top 50 recent answers are included
Related Tags
type-theory × 465programming-languages × 107
dependent-types × 72
lambda-calculus × 62
type-checking × 59
type-inference × 44
functional-programming × 41
logic × 33
terminology × 22
reference-request × 22
category-theory × 20
inductive-datatypes × 19
polymorphisms × 18
homotopy-type-theory × 17
proof-assistants × 16
curry-howard × 16
coq × 15
typing × 15
compilers × 13
abstract-data-types × 11
computability × 10
notation × 10
haskell × 10
recursion × 8
semantics × 8