14

$\mathsf{id}$ and $\mathsf{const}$ are not variables of the calculus, but syntactic sugar for $\lambda x \rightarrow x$ and $\lambda x \rightarrow \lambda y \rightarrow x$ respectively. This is stated at the end of §2.2 and subtly conveyed by the use of a sans-serif font rather than italics (this is a typographic convention of this particular document, not a ...


7

You can always inhabit a type by a free variable: the type $\tau$ is inhabited by the free variable $x_\tau$. When people speak about "implementation" of a type they mean a closed term, i.e., one without free variables. The examples you gave contain free variables, namely $b_a$. In pure simply-typed $\lambda$-calculus all terms are "...


7

I think we just need to get some things straight here: In the expression $\lambda a : \mathsf{type} . \lambda x : a . x$ the variable $a$ is bound (by the outer $\lambda$). The expressions $\lambda a : \mathsf{type} . \lambda x : a . x$ and $\lambda b : \mathsf{type} . \lambda x : b . x$ are $\alpha$-equal. The expression $\lambda a : \mathsf{type} . \...


7

Javascript has no bottom type. It does not even really have types in the sense of type theory. Instead, values are tagged with information that is called "dynamic type". Programming languages typically do not have the bottom type (it is also called the empty type) because they allow defintion by general recursion, which implies that all types are ...


6

The missing part is the "identity extension lemma", which is mentioned in Reynolds' original paper but not in Wadler's. For $F : \text{Type} \to \text{Type}$, this says that if the relational interpretation of $F$ is instantiated with a type $A$ and the identity relation on $A$, we get the identity relation on $F\,A$. For System F, identity ...


6

Canonicity does not imply weak normalization. First, let me phrase the involved definitions more precisely: WN: every open term is reducible to a normal term Canonicity: every closed term is reducible to a canonical term (Note: in modern metatheory of type theory, it is more common to talk about conversion instead of reduction, and likewise to talk about ...


6

The seminal paper on this topic is Linear Types Can Change the World! by Phil Wadler. Of course, with a title like that, you know it has to be a Wadler paper. It's a pun, the implication being that linear/uniqueness type system allows you to represent operations which mutate the world state. You can use linear types today in languages such as Clean. See, for ...


5

$\newcommand{\fix}{\mathsf{fix}}$ $\newcommand{\fold}{\mathsf{fold}}$ $\newcommand{\map}{\mathsf{map}}$ Here is, I believe, how one would use parametricity to prove your last lemma. I'm going to rework some stuff slightly for my own understanding. We have: $$C = ∀ r. (F r → r) → r$$ with $F$ functorial. We have: $$\fix : F C → C$$ corresponding to your ...


4

The dependent types allow you to specify what properties your function should have, not just what its domain and codomain are. This way it becomes impossible to accidentally use the wrong function. For example, suppose we want a function that sorts lists (of integers). In ordinary programming we would ask for a value of type List → List, and then we would ...


4

So, the answer is arguably "yes," this is an example of dependent types. However, the problem with a lot of simple examples that people create for this is that they don't demonstrate non-trivial aspects of dependent typing. Arguably yours is better in this respect, because the type in question depends on an arbitrary value in MemorySlabCache. ...


4

OCaml and Scala are popular choices for types systems, but they are by no means the only languages you can write a compiler, interpreter, typechecker, or type system in. Type-checking involves traversing syntax trees representing terms and types. Languages with some form of algebraic data type make this easy, since these traversals can be defined using ...


4

If by "non-terminating real number" you mean to say that the digit expansion of the number is an infinite sequence, then that is not saying much, because every real number is "non-terminating" in this sense, even the real number 42, for its digit expansion is $$41.999999999999999999999999999999....$$ In any case, nobody suggests that the ...


3

I think the best way to understand why homotopy type theory related stuff is interesting from a computer science perspective is that is a more satisfying account of extensional equality than any prior version. Lots of attempts have been made previously to add extensionality features to type theory that have been missing relative to e.g. set theory, but they ...


3

I won't lie: I don't understand the homotopy part of homotopy type theory. But I have a decent grasp of Univalence, which is the axiom at the heart of Homotopy Type Theory (HoTT). The main idea of univalence is that we treat equivalences (essentially, isomorphisms) as equalities. When two types are isomorphic, you have a way to get from one to the other and ...


3

Yes. Before I give the answer, let me set the stage. Giving types to expressions and functions Historically, programming languages started to have types to qualify memory locations: does the memory cell where x is stored contain an integer or a floating-point value? Type enforcement is then to check (or coerce) that the value that gets stored into x has the ...


3

I'll admit I'm confused about the details of your question: you want the implementation of a program to appear in its type? Usually types talk about behavior. That's why they're useful! The idea of having the full specification of a procedure appear in types is very suggestive of dependent type theory. Traditionally these theories only apply to languages ...


3

Agda has an interpretation in classical set theory, as well as in realizability models. Any proof carried out in Agda is valid in any of these models. It can therefore be interpreted in classical set theory to give a proof of uncountability of $2^\mathbb{N}$, but it can also be interpreted in the effective topos to give a proof of computable uncountability ...


3

There is no assumption in your proof that the functions involved are computable, so it would be quite stingy to interpret the proof that way merely because Agda allows you to compute with its terms. Rather, yes how it should be interpreted depends on the model, and constructive (in the sense of just removing axioms) proofs like the one you've given enable an ...


3

The greatest fixed point cannot contain only the infinite lists, because it must contain all the elements of the least fixed point (and every other fixed point). Another way to see this is that just the infinite lists are not even a fixed point, since applying $F$ will add $\mathrm{Nil}$, which is not infinite. However, adding the infinite lists is the right ...


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 = ...


3

This paper is my go-to for implementing dependent types. It starts from the basics, uses bidirectional types, and has accompanying code in Haskell. If you're at all interested in type inference, this paper is great, and also has accompanying Haskell code. David Christiansen has a tutorial on dependent type checking with bidirectional types, with a Haskell ...


3

A metavariable is a variable that denotes some hypothetical chunk of a program. This distinction is important in the theory of programming languages, where we need to distinguish variables representing program fragments from the variables contained in those programs. The terminology, I think, comes from logic: if you're defining a logic, you need to define ...


3

Not sure whether I completely understand the question, but here is my attempt: a naïve reading would allow for Γ, t, or T to contain type variables not mentioned in χ. $\Gamma$, $t$ and $T$ may contain type variables not mentioned in $\mathcal{X}$. The set $\mathcal{X}$ contains only unification variables. That is, fresh variables generated by the typing ...


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 ...


2

In actual programming languages, a function is not forced to deal explicity with input is not meant to. For a function f(x) you can say something like: // x must satisfy x != 0, otherwise inv(x) results in undefined behaviour. double inv(double x) { return 1/x; } In computer since though, using $\bot$ is a very useful symbolic tool to express such ...


2

"Inhabited" is the properly constructive notion of "non-empty". The idea is that to demonstrate that a type is inhabited requires exhibiting a particular construction with that type, while 'non-empty' means merely demonstrating that it is impossible to demonstrate that there are no such constructions. "Uninhabited" is the ...


2

As mentioned by Andrej, this is an instance of transporting along an equivalence of families and display maps. In this specific case, we have an equivalence of graphs and relations. open import Function open import Data.Product open import Relation.Binary.PropositionalEquality open import Level renaming (zero to lzero; suc to lsuc) -- type of relations on a ...


2

I don't know about statement types, but there's been a lot of research over the decades about CPU instruction frequency and how it impacts ISA design, IR design, and VM design... but it's all for languages like C. See, for example, loads/stores/branch frequencies for the SPEC2017 benchmarks. If your language is C-like, there are basically only two reasons to ...


2

What happens if I try to get Bar before it has been set? If you expect a compilation error, then you are not talking about a single type, but instead a sequence of types, where the type changes after each call to the set method. Look into 'strong update' and 'linear types'. Why not just use a record type? type MyRecord = { Foo : Error, Bar : number }


2

As an example, here is the full derivation for the type judgement $$\alpha::\ast,y::\alpha \vdash (\lambda x \rightarrow x :: \alpha \rightarrow \alpha) \: y :: \alpha$$ where $\enspace \Gamma = \alpha::\ast,y::\alpha \enspace$ and $\enspace \Gamma' = \Gamma,x::\alpha \enspace$: $$ { \dfrac { \dfrac { \Gamma \vdash \alpha \rightarrow \alpha :: \ast ...


Only top voted, non community-wiki answers of a minimum length are eligible