28

HoTT "suffers" from Gödel incompleteness, of course, since it has a computably enumerable language and rules of inference, and we can formalize arithmetic in it. The authors of the HoTT book were perfectly aware of its incompletness. (In fact, this is quite obvious, especially when half of the authors are logicians of some sort). But does incompleteness "...


28

First, to reiterate one of cody's points, the Calculus of Inductive Constructions (which Coq's kernel is based on) is very different from the Calculus of Constructions. It is best thought of as starting at Martin-Löf type theory with universes, and then adding a sort Prop at the bottom of the type hierarchy. This is a very different beast than the ...


21

If you look at Notes on Chapter 8 you will see what has already been formalized, and I think that's a lot. There are the Coq HoTT library and the Agda HoTT-Agda library which formalize large chunks of Homotopy Type Theory. To get things done in Coq we needed a special version of Coq that was patched just for the purposes of HoTT. However, Coq is moving in ...


21

I've often wanted to try and summarize each dimension of the $\lambda$-cube and what they represent, so I'll give this one a shot. But first, one should probably try to dis-entangle various issues. The Coq interactive theorem prover is based on an underlying type theory, sometimes lovingly called the calculus of inductive constructions with universes. You'...


20

What you want exists, and is an enormous area of research: it's the entire theory of programming languages. Loosely speaking, you can view computation in two ways. You can think of machines, or you can think of languages. A machine is basically some kind of finite control augmented with some (possibly unbounded) memory. This is why introductory TOC ...


18

How do type classes fit in this model? The short answer is: they don't. Whenever you introduce coercions, type classes, or other mechanisms for ad-hoc polymorphism into a language, the main design issue you face is coherence. Basically, you need to ensure that typeclass resolution is deterministic, so that a well-typed program has a single ...


14

The formulas are formulas of Abadi-Plotkin logic, which they describe in their paper A Logic for Parametric Polymorphism. The semantics of System F that Abadi and Plotkin used to interpret their logic can be found in Bainbridge, Freyd, Scedrov, Scott's paper Functorial Polymorphism.


13

This is an interesting question! As Anthony's answer suggests, one can use the usual approaches to compiling a non-dependent functional language, provided you already have an interpreter to evaluate terms for type-checking. This is the approach taken by Edwin Brady. Now this is conceptually simpler, but it does lose the speed advantages of compilation when ...


12

As far as I understand, in Agda it is possible to represent all of that (i.e. all of Chapter 2 -- there is a library on github which does; AFAIK, the same is true of Coq). It is only when you get to later chapters that things get dicey. There are two obvious items: The circle. This is represented (in Agda) using a postulate, and so is not as nice as ...


10

Edwin Brady's PhD thesis outlines how to construct a compiler for a dependently typed programming language. I'm not an expert, but I'd say it's not extremely harder than implementing a System F-like compiler. Many of the principles are quite similar and some are the same (e.g. supercombinator compilation.) The thesis covers many other concerns.


10

As they explain in the related work section of the 2008 paper, the constraint types they describe are most closely related to refinement types. I wont give references, as there are plenty in the bibliography of the aforementioned paper, but I can give a quick overview. Refinement types are a language that allow the expression of refinements of the values of ...


9

If you want to include a fixpoint combinator in the language, you don't need to change anything to the syntax of types or the rules to type existing expressions. All it takes is adding one constant, a rule to type it and a rule to reduce expressions containing it: $$ \dfrac{}{\mathsf{fix} : (\tau \rightarrow \tau) \rightarrow \tau} \qquad \mathsf{fix} \, ...


9

The way I understand the difference is that ownership types constrain the shape of the object graph, and substructural systems (like separation logic) manage permissions to access the heap. In the original work on ownership types, the idea is to maintain the invariant of owners as dominators. An object $o$ is dominated by an object $d$, if every path from ...


9

Set theory is doing you some harm here and the sooner you liberate yourself from it the better it will be for your understanding of computer science. Forget the intersections and unions. People get this idea that $\forall$ and $\exists$ are like $\bigcap$ and $\bigcup$, which is the sort of thing the Polish school was doing a long time ago with Boolean ...


9

You can't do this using the traditional Church encoding for Bool: #Bool = ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool ... because you can't write a (useful) function of type: #Bool → * The reason why, as you noted, is that you can't pass in * as the first argument to #Bool, which in turn means that the True and False arguments may not be types. ...


9

I think that the type system you want is elementary affine logic with fixpoints. A distinctive feature (actually, the distinctive feature) of light logics, including elementary linear/affine logic, is that types do not ensure termination: unlike usual logical system, cut-elimination follows from a structural property of proofs (namely, stratification), the ...


8

JHC uses a different approach. The compiler's intermediate language is a dependently typed lambda-calculus where there is no distinction between types and values. JHC therefore can perform a case analysis on the type parameter of a function and call the correct overloaded function directly. The JHC website goes into some depth on the implementation, as ...


8

I don't want to make a statement about "all linear lambda calculi" since it's hard to make that precise, but for pure linear lambda-calculus the answer is yes. One way to enforce linearity in pure lambda calculus is by trying to type application and abstraction using the linear implication $A \multimap B$, $$ \frac{\Gamma \vdash t:A\multimap B\quad \Delta\...


8

First, note that nothing turns on the presence or absence of the empty type: if you have a nonlinear calculus with function types and unrestricted recursive types, then it is inconsistent. Indeed, your derivation works regardless of the type of the answer -- the very same term you have works for $\mu a.\; a \to X$ for any $X$. This is known as Curry's ...


8

I posted this to TYPES, but its probably worth copying here as well: In "The system F of variable types, fifteen years later", Girard remarks that there was no particular reason for the name F: However, in [3] it was shown that the obvious rules of conversion for this system, called F by chance, were converging. There may be another explanation in ...


8

It sounds like you want an overview of normalization arguments for type systems with positive datatypes. I'd recommend Nax Mendler's PhD dissertation: http://www.nuprl.org/documents/Mendler/InductiveDefinition.html. As the date suggests, this is pretty classic work. The basic intuition is that an ordinal $\lambda$ can be associated to any element of a ...


7

The two inference rules are different, because the first requires that x:T_1 is the only assumption, while the second allows side assumptions. This can have subtle effects of the consequence relation for the type theory prevents the type theory from modelling weakening by having as the hypothesis rule: $$ \frac{}{\Gamma, x:A \vdash x:A} $$ In your English ...


7

Spoiler: the types are isomorphic. First let me clarify what might be meant by "isomorphic". Say that two datatypes $S$ and $T$ are isomorphic if there are maps $f : S \to T$ and $g : T \to S$ such that $f(g(v)) = v$ for every value $v : T$ and $g(f(u)) = u$ for every value $u : U$. Let us fix a type $A$. We can then write your equations without the ...


7

I'm quite fond of Wadler's paper The Girard-Reynolds Isomorphism which shows that there is a translation from system $\mathrm{F}$ to and from Second Order Predicate Logic (a version with higher-order types). One direction is "dependency erasure", an important idea in dependent types, and the other is the "parametricity theorem" or theorem-for-free of a type. ...


7

I recently finished writing a survey of Ownership Types and found very little that discusses the relationship between the two topics. The three closest papers I came across are the following, which curiously come from the same conference: Yang Zhao and John Boyland. A fundamental permission interpretation for ownership types. In Second IEEE/IFIP ...


7

There are plenty such typing systems. Most work is based on the linear/affine typing system introduced in (1) and generalised in (2). Here are the main works on this subject. In (3) the typing system ensures a precise match with PCF (int its call-by-name variant -- changing to call-by-value is easy). In (4) the typing system gives a precise interpretation ...


7

Coq without Prop is not strong enough, because it's basically Martin-Löf type theory with universes. Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S : \mathrm{Term} \to \mathrm{Prop}$, and impredicative universal quantification lets you express arbitrary intersections.


7

Since the CoC has dependent types and system $F$ does not, I'll assume you mean a function whose types is in system $F$, but whose definition can only be written in CoC. Luckily in this case we can restrict to system $F_\omega$, which can express the same non-dependent functions as CoC, by some erasure argument. In general, a rule of thumb to construct such ...


6

Core calculi for Java typically take the classes-as-types approach. Two well-known examples are Featherweight Java and Classic Java.


6

Cook-Reckhow propositional proof systems are nonunifrom. E.g. the computational complexity counterpart to the class of polynomial-size $\mathsf{Extended Frege}$ proofs is the nonuniform complexity class $\mathsf{P/poly}$. We have to look at their uniform counterparts: E.g. the proof complexity counterpart for $\mathsf{P}$ are bounded arithmetic theories ...


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