23

It is a common misconception that we can translate let-expresions to applications. The difference between let x : t := b in v and (fun x : t => v) b is that in the let-expression, during type-checking of v we know that x is equal to b, but in the application we do not (the subexpression fun x : t => v has to make sense on its own). Here is an example: ...


7

Yes, realizability theory allows you to model dependent type theory based on a variety of computational models, such as: Turing machines (with or without oracles), various $\lambda$-calculi, topological models of computation, sequential functionals, game-semantics computational models, and many others. References: Jaap van Oosten: Realizability: an ...


6

There are potentially multiple ways of presenting canonicity (and I think complications depending on the theory). However, I think the simplest way to think about it is from the perspective of a programmer wanting to use the type theory to compute something. For instance, we might want to compute some natural number satisfying some specification we've come ...


5

Recall that (a few paragraphs above) two objects are definitionally equal if after certain computation steps they evaluate to identical results. Assume throughout this post that $M$ and $N$ are definitionally equal. This means that there is a series of computation steps $M_0 \leftrightarrow M_1 \leftrightarrow \ldots \leftrightarrow M_n$ where I use $\...


5

Yes, there is such an untyped function, and it turns out that it is equivalent to the untyped erasure of iteration for church numerals. The Cedille project has been doing lots to give types to these functions, and the core concept there is the dependent intersection, which provides a limited form of self reference that is enough to derive induction ...


5

Supposing we have $a$ and $b$ of type $A$ and $p : \mathrm{Id}_A(a,b)$, there simply is not any rule of type theory that would allow you to replace $b$ with $a$ arbitrarily. So one answer is "because type theory does not let you do that", and if you think that it can be done, please show me how. But I suppose that is a non-answer, what you really are asking ...


4

The definition is not correct. It states that a machine is polynomial time (the field poly in poly-time-machine) when its running time is below the exponential function $n \mapsto 2^n$ (the definition is-poly). This would allow, for example, a running time $n \mapsto 1.5^n$, which isn not poly-time according to the accepted definition.


4

We don't always want extentionality In mathematics, a function is a relation between its inputs and its output. Two functions are equal if and only if they map the same outputs to the same inputs. But in computer science, we're often interested in descriptions of computations which we also call “functions”, where it matters how the outputs are calculated ...


3

In general cummulative universes are a bit nasty. To see what is really going on, at the very least it makes sense to have explicit lifting maps $\mathsf{lift}_{i,j} : \mathcal{U}_i \to \mathcal{U}_j$ for $i \leq j$. With these in place, your question is: how do the types $$\mathsf{lift}_{i,i+1}(A =_{\mathcal{U}_i} B)$$ and $$(\mathsf{lift}_{i,i+1} A) =_{\...


2

What Agda is showing you in the source code in both cases are the propositional proofs, i.e., elements of the identity type. In Agda the judgemental (definitional) equality is invisible to the user. Agda uses it in the background to verify that terms have required types. When it has to compare $a$ and $b$, it normalizes both of them (based on judgemental ...


2

what does it mean by becoming extensional in the first place? The axiom of extensionality relates to what it means for two functions to be equal. Specifically, extensionality says: $f = g \iff \forall x \ldotp f(x) = g(x)$ That is, functions are equal if they map equal inputs to equal outputs. By this definition, quicksort and mergesort are equal, even if ...


2

The induction principle for $=_{U_{i+1}}$ gives you a map $(A=_{U_{i+1}}B)\rightarrow (A=_{U_i}B)$. In HoTT without univalence, there is no map $(A=_{U_i}B)\rightarrow (A=_{U_{i+1}}B)$: indeed, you could assume the univalence axiom only for universe $U_i$. In that case, $A\simeq B$ gives you by univalence an inhabitant of $A=_{U_i}B$, but not of $A=_{U_{i+1}...


2

The only way to prove ∥ X ∥ is to prove X (unless you admit some other axiom). So, assuming P is a proposition, there is no way to prove ∥ ((A) ⊎ (¬ A)) ∥ if you cannot prove ((A) ⊎ (¬ A)). It is not a correct intuition that undecidable propositions are either true or false, just we do not know about it. A formal system S with an undecidable proposition P ...


1

In general, type inference for dependent types is undecidable. This means that when checking a function, we need some way to know what type its argument has. In the case of Idris, they simply annotate lambdas with parameter types. This is very common in type theory, since it makes your type system syntax directed in a very simple way. When you do this, you ...


1

I'll talk about this more software-engineering-ly. Are you talking about a coproduct type whose latter constructors can refer to prior ones (which, looks pretty similar to a product whose latter fields can refer to prior ones)? This is possible in Agda after HIT is introduced (in version 2.6.0): -- Auxiliary definition: Nat data Nat : Set where zero : ...


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