# Tag Info

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....
• 30.9k
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, ...
• 659
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 ...
• 8,328
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 ...
Accepted

• 12.1k
Accepted

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

### 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,...
• 326

### 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, ...
• 30.9k

### 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 ...
• 659
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 ...
• 801

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

### 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 ...
• 8,233
Accepted

### how type checking fails?

I finally figured it out. The key is using sub-typing rules. ...
• 1,024
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 <...
• 12.1k
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 ...
• 29.8k
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 ...
• 801
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 ...
• 997

### 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-...
• 661

### What is "Hindley-Milner (i.e., uniﬁcation-based) polymorphism"?

Yes, in that context Hindley-Milner polymorphism is let-polymorphism, since such language uses $\sf let$ to introduce polymorphic functions. In the untyped lambda calculus, we can consider a (non ...
• 14.6k
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 ...
• 12.1k
### Is $\Gamma \vdash x x : T$ possible in the simply typed lambda calculus?
You are on the right track. The argument you would use is on the lines of size of types defined below: (I am assuming you are in the world of simply typed $\lambda$-calculus) $size(T) = 1$ \$size(T \...