46

In their basic form, type classes are somewhat similar to object interfaces. However, in many respects, they are much more general. Dispatch is on types, not values. No value is required to perform it. For example, it is possible to do dispatch on the result type of function, as with Haskell's Read class: class Read a where readsPrec :: Int -> String -...


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


26

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


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


18

[I haven't thought deeply about the issues of object-oriented type systems, but I will say what I know to get the discussion going.] We say that $A$ is a subtype of $B$ if all $A$-typed values can be used in every context where $B$-typed values are expected. Or, to put another way, $A$-typed values can "masquerade" as $B$-typed values. If such ...


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.


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


12

Typically, you use binary parametricity to prove program equivalences. It's unnatural to do this with a unary model, since it only talks about one program at a time. Normally, you use a unary model if all you are interested in is a unary property. For example, see our recent draft, Superficially Substructural Types, in which we prove a type soundness ...


11

The main reason for avoiding sets in semantics of types is that a typical programming language allows us to define arbitrary recursive functions. Therefore, whatever the meaning of a type is, it has to have the fixed-point property. The only set with such a property is the singleton set. To be more precise, a recursively defined value $v$ of type $\tau$ (...


11

Almost all systems with type inference use call-site information to do this. Examples include Standard ML, OCaml, F#, and Haskell. Many other languages use call-site information to infer type parameter instantiation, such as Java, C#, Scala, and Typed Racket. This often goes by the name "Local Type Inference". I would just describe what you're looking ...


11

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


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.


9

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

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

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


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

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

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

Semantic subtyping is based on an underlying set theoretic interpretation of types, where subtyping is subset. The original work, I believe, is by Castagna in the context of XML processing language CDuce. Types correspond to sets of XML documents. The ideas have since been reapplied to the $\pi$-calculus and to a calculus objects and classes.


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