8 votes
Accepted

What are the rules for positive recursive types in dependent type theory?

Why are recursive types seldomly seen in dependent type theory? The point of inductive types is precisely that you get normalization. Unrestricted recursive types simply lead to non-normalizing terms....
Andrej Bauer's user avatar
  • 30.3k
8 votes
Accepted

What is meant by a full abstract model of a lambda-calculus like language?

In denotational semantics, you want to be able to map each of your language terms to some object in your semantic domain or model. Now, it cannot be any arbitrary domain/model as you like, but, ...
Apoorv's user avatar
  • 659
7 votes
Accepted

Can all regular tree types be expressed as $\mu$ types?

You can reduce mutual recursion to a single recursion, see Bekic's Theorem, see e.g. Section 10.1 of Winskel's (1), where Bekic is worked out for programs rather than types. Note however that the ...
Martin Berger's user avatar
7 votes
Accepted

call by value: what is a value?

The set of values is defined for a particular reduction relation. Each reduction relation defines its own set of values. Reduction for the lambda calculus isn't just beta reduction, there are also ...
Gilles 'SO- stop being evil''s user avatar
6 votes
Accepted

Some points about type checking of simply typed $\lambda$-calculus?

Your example is poorly chosen. In $(\lambda x : \mathsf{bool} . x) \, \mathsf{true}$ you can obviously read off the type from the $\lambda$-abstraction because it tells you that $x$ should have type $\...
Andrej Bauer's user avatar
  • 30.3k
6 votes

Why injection into sum type apparently leads to ambiguity?

I think the key point here is $\sigma$, $\tau$ and $\phi$ are type variables, and not specific types. So, what the typing rule for $\operatorname{inl}$ says is that $\operatorname{inl} M$ is of type $\...
svick's user avatar
  • 1,866
6 votes
Accepted

Proving preservation under substitution System F Omega

Throughout $y$ should have type $T_1$ instead of $T_2$. Let us be more careful about step 3. We are going to apply the following induction hypothesis: If $\Gamma, y : T_1, x : S \vdash t_1 : T_2$ ...
Andrej Bauer's user avatar
  • 30.3k
5 votes

How can an existential type be defined in terms of universal type?

As a general recipe, to figure out how to encode a type A, write down ∀Z . (A → Z) → Z and massage it to something that does ...
Andrej Bauer's user avatar
  • 30.3k
5 votes
Accepted

T&PL: Language grammar with terms

$S_0$ is the empty set. Let $i=0$. $$\begin{align} S_1= S_{0+1} & = \;\;\;\{true, false, 0\} \\ & \;\;\;\cup \; \{succ \: t_1, pred \: t_1, iszero \: t_1\ |\: t_1 \in S_0\} \\ & \;\;\;\...
John L.'s user avatar
  • 38.8k
5 votes
Accepted

Confusion about the definition of de Bruijn terms in the TAPL book

The $n$ isn't indexing how many references to variables there are, it's indexing how many free variables are able to be referred to. You can think of $0,1,\dots,n-1$ as being variables $v_0,v_1,\dots,...
Derek Elkins left SE's user avatar
5 votes
Accepted

Confluence to show equivalent terms have one common reduct

$S \leftrightarrow^* T$ does not mean that $S \rightarrow^* T$ and $T \rightarrow^* S$! It means that there is a chain of reductions $S = S_0 \rightleftharpoons_1 S_1 \rightleftharpoons_2 S_2 \...
Gilles 'SO- stop being evil''s user avatar
5 votes
Accepted

Free variables as defined in TAPL seems wrong

Since x is both free and not free it seems the definition of free variables is wrong. Why? There is no rule that says that the sets of free and bound variables have to be disjoint. Nothing breaks if ...
Natalie Clarius's user avatar
4 votes
Accepted

How to understand these exposure algorithm rules for System F sub?

In a typing rule (and more generally any deduction rule), all metavariables¹ are universally quantified. That is, the rule can be applied for any instantiation that is syntactically correct. For ...
Gilles 'SO- stop being evil''s user avatar
4 votes

Confusion about the definition of de Bruijn terms in the TAPL book

This is crucial: It further clarifies that the elements of $\mathcal{T}_n$ are terms with at most $n$ free variables, numbered between $0$ and $n-1$. Then, in the rest of your argument, you forgot ...
chi's user avatar
  • 14.5k
4 votes
Accepted

Why is the type ∀t.t un-inhabited in System F?

The simplest proof is giving a model where types are interpreted as propositions, and terms as proofs, then observing that $\forall \alpha.\alpha$ is interpreted as the false proposition, so any $\...
András Kovács's user avatar
4 votes
Accepted

What does "lambda terms modulo convertibility" mean?

Saying that you consider ⟨objects⟩ modulo ⟨equivalence⟩ means that you treat equivalent objects as equal. This implies that the only properties of the objects that you're interested in are the ones ...
Gilles 'SO- stop being evil''s user avatar
3 votes

Which is a type of objects in mainstream OO languages: a class, an interface, an abstract class, a metaclass?

Unfortunately I don't have a copy of TAPL with me, so I can't figure out exactly what the author intends. But there is a point we should make, that types are something which classifies terms or values,...
Jason Carr's user avatar
3 votes

Do the following concepts belong to syntax or semantics?

It's not really a good idea to try to divide everything in PL into "syntax" and "semantics". Often we mix things. Nevertheless, as for your question, we normally divide things up like this: terms, ...
Andrej Bauer's user avatar
  • 30.3k
3 votes

Proving property of a term using Induction

A term is defined recursively. You can do induction on recursive types, using structural induction. For instance, suppose we say that a term is something of the form $c$ (a constant), or $t_1+t_2$, ...
D.W.'s user avatar
  • 158k
3 votes

What are the difference and relation between type checking and type reconstruction?

What are the difference and relation between type checking and type reconstruction? Type reconstruction is a class of problem that involves coming up with a type for a term. For example given a ...
Apoorv's user avatar
  • 659
3 votes
Accepted

Free variables in constraint-typing derivation?

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 ...
frabala's user avatar
  • 801
3 votes

Free variables as defined in TAPL seems wrong

Although you don't actually need to do this to define free variables, it helps to think about bound and free occurrences of a variable in a term. An occurrence of a variable $x$ is bound in a term $t$ ...
Gilles 'SO- stop being evil''s user avatar
2 votes
Accepted

how type checking fails?

I finally figured it out. The key is using sub-typing rules. ...
alim's user avatar
  • 994
2 votes

What are the rules for positive recursive types in dependent type theory?

A pretty comprehensive reference is Peter Dybjer's Inductive Families paper that presents a very general class of inductive types (I've rarely seen them called "recursive types"). Note that ...
cody's user avatar
  • 8,154
2 votes
Accepted

Does Types and Programming Languages use a recursive equation to define a recursive type or its generator?

You've stumbled across the difference between isorecursive and equirecursive types. Equi-recursive types say "types are (possibly) infinite trees, and a recursive type is the solution to a recursive ...
Joey Eremondi's user avatar
2 votes
Accepted

Find typing derivation of STLC term with reference types

The expression $t$ does not contain any free variables, so one can start typing it with an empty context: $\emptyset\,|\,\Sigma~\vdash~t : \mathrm{Int}$, and attempt to build the full derivation tree ...
frabala's user avatar
  • 801
2 votes
Accepted

Isoecursive Types When to Fold and Unfold

As you've stated, the type of IntObject is mu X. {val: int, add: (X -> X)}. fold and <...
Derek Elkins left SE's user avatar
2 votes
Accepted

Are type abstraction values and universal types not for non functions, but only for functions?

Short Answer: In λX₁. λX₂. ... λXₙ. t it doesn't matter if t is not a function, but if so, it may not be an interesting example ...
nekketsuuu's user avatar
2 votes

Is `→` a type operator?

Yes, these can all be viewed as operators at the type level, but they're not all completely analogous. Most of these are type constructors in that they're formation operators for types, though type-...
varkor's user avatar
  • 661
2 votes
Accepted

Types and Programming Languages - proof for theorem about principles of induction of terms

While you should get in the habit of providing definitions so your question is self-contained, especially when the original text is not easily accessible, the first thing to note is that the theorem ...
Derek Elkins left SE's user avatar

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