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


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

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

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


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

You state: infinite unions can have no relationship between strings of a language. Can you explain what you mean by this? Meanwhile, every language is the infinite union of the singleton languages that each contain one element of the language. Clearly, not every language is regular.


4

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


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

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


3

Agda is definitely the better choice if you're doing Homotopy Type Theory. Idris has several features that are specifically incompatible with HoTT. Specifically, you can use dependent pattern matching to prove Uniqueness of Identity Proofs (UIP), which, when combined with Univalence, allows you to prove False. There's also a type-case feature which you can ...


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

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

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

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

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


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

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

The best way to explain it is $$\mathsf{Bool} \to C \cong C \times C,$$ which is a special case of $$(A + B) \to C \cong (A \to C) \times (B \to C).$$ Read the above as follows: as sum is equivalent to a pair of visitors. (By the way, this is not the de Morgan law. It does not have a name, as far as I know. It's a general consequence of the definition of the ...


2

The symbol $(\bot)$ usually represents the least element of a lattice. The least element often goes at the bottom part of a Hasse diagram. That is maybe the reason you're looking for. For example, in a Hasse diagram containing propositions with the logical consequence relation, one usually put falsehood, at the bottom of the diagram, mostly because from a ...


2

Interpreting your problem as finding a computable $f$ such that $f\big(\langle M\rangle\big)=\langle M'\rangle$ with the property that $M'$ enumerates all programs equivalent to $M$, i.e. all $M''$ with $L(M'')=L(M)$, the answer is no (such $f$ does not exist). One way to show this is to observe that such $f$ would place the language $\left\{\big(\langle M_1\...


1

Meta-variable explanation by example Consider the simply typed lambda calculus (STLC) with base types Int for integers and Bool for booleans. In this calculus, we can have an identity function for integers $(\lambda x:\mathrm{Int}.x)$ and another one for booleans $(\lambda x:\mathrm{Bool}.x)$. More generally, For every type $A$ of STLC, there is an identity ...


1

Normally, Agda does an analysis to determine that your indexed type is equivalent to a parameterized type. Essentially, since A occurs in the result type, knowing that l : List A tells you what type A is 'stored' in the value l. The value is known, which means that tricks that involve embedding a universe into a small type within said universe to cause a ...


1

You should think in Turing Machines. If I understand correctly, what you ask is more or less "Given the code of a Turing Machine, is it possible to enumerate the codes of all Turing Machines with the same language?". I think this is not possible, because it is undecidable to know whether two TM have the same languages (all the more so list all TM ...


1

There are two senses in which type formation operations are 'functorial,' but neither matches functoriality on the category of types. First, you can interpret the collection of types as a groupoid, and consider isomorphisms between types to be 'arrows.' These compose, but also always have inverses, so are in some sense undirected. However, this is also why ...


1

$\newcommand{\Type}{\text{Type}}\newcommand{\llb}{[\![}\newcommand{\rrb}{]\!]}\newcommand{\map}{\text{map}}$ Note: This answer is not a standalone answer, but an incomplete attempt to give some intuition for András Kovács's answer. One important thing to point out is that is that type constructors are not always functors. In particular, the type constructor $...


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