Questions tagged [types-and-programming-languages]

For questions about the book "Types and Programming Languages" by Benjamin Pierce, and the exercises from the book.

Filter by
Sorted by
Tagged with
1 vote
2 answers
77 views

Free variables as defined in TAPL seems wrong

In "Types and Programming Languages" by Benjamin C. Pierce (WorldCat) 5.3.2 Definition: The set of free variables of a term t, written FV(t), is defined as follows: FV(x) = {x} FV(λx.t₁...
user avatar
  • 5,032
3 votes
2 answers
57 views

What does "lambda terms modulo convertibility" mean?

In "The Lambda Calculus - Its Syntax and Semantics" by H.P. Barendregt (WorldCat) is this statement, the first sentence of chapter 2 after the introduction chapter, so in a way this sets the ...
user avatar
  • 5,032
5 votes
1 answer
133 views

Free variables in constraint-typing derivation?

In Types and Programming Language's constraint typing rules (Figure 22-1), is it possible for any part of the typing derivation to contain free type variables that aren’t part of the fresh variables? ...
user avatar
1 vote
1 answer
43 views

Category Set language using simply typed lambda calculus

I am currently self learning Category Theory and Simply typed lambda calculus (STLC). For learning purposes, I have implemented an STLC interpreter as given in Types and Programming Languages book ...
user avatar
  • 11
1 vote
1 answer
82 views

Substitution lemma for types

TAPL (page 549) proposes the following lemma in order to prove soundness of System F type system: Substitution lemma for types: $E, X, \Delta \vdash t: T \implies E, [X \mapsto S] \Delta \vdash [X \...
user avatar
  • 2,220
1 vote
0 answers
64 views

The abstract interpretation corresponding to the pure simply typed lambda calculus

In Types as Abstract Interpretation, Patrick Cousot sketched how different type systems could be constructed from the collecting semantics of a language. However, the notation of the paper is very old ...
user avatar
  • 2,220
6 votes
2 answers
194 views

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

How do you prove that there exists no term with the type $\forall t. t$ in System F? I tried searching through Pierce's TAPL and Reynold's ToPL, but could not find anything. I suspect that the proof ...
user avatar
  • 619
2 votes
1 answer
57 views

Dynamic testing of down casts as explained in TAPL

On page 195 of Pierce's TAPL book, he states that one can replace a down-cast operator by some sort of dynamic type test. Then he gives the following rules: T-Typetest: $\dfrac{\Gamma \vdash t_1:S \;...
user avatar
  • 2,220
1 vote
0 answers
45 views

How does progress fail in system $F_{\omega}$ when types $T_1 \to T_2$ and $T_2 \to T_1$ are equivalent?

Pierce's TAPL book gives in exercise 30.3.17 the setting where $T_1 \to T_2 \equiv T_2 \to T_1$ (the function type are assumed to be equivalent). In the solutions, he claims that this assumption ...
user avatar
  • 2,220
2 votes
1 answer
104 views

Confluence to show equivalent terms have one common reduct

In lemma 30.3.9, Pierce states a confluence property for $F_{\omega}$: $S \to_* T \land S \to_* U \implies \exists V. T \to_* V \land U \to_* V$ He then states the following proposition: $S \...
user avatar
  • 2,220
3 votes
0 answers
42 views

On the diamond property for $F_{\omega}$ in TAPL

In page 455, of Pierce´s TAPL and page 560, the single-step diamond property of reduction: $S \Rrightarrow S' \land T \Rrightarrow T' \implies \exists V. T \Rrightarrow V \land U \Rrightarrow V$ ...
user avatar
  • 2,220
2 votes
0 answers
80 views

Are the permutation or weakening lemmas needed for term substitution?

In TAPL book, page 453, Pierce discusses the following lemma: $\Gamma , x:S , \Delta \vdash t:T \land \Gamma \vdash s:S \implies \Gamma, \Delta \vdash [x \mapsto s]t:T$ He claims that when $t$ is ...
user avatar
  • 2,220
1 vote
2 answers
62 views

Are these two sensible and related or unrelated ways of regarding a logic system as a programming language?

When I am trying to understand logic programming languages e.g. Prolog, I am immediately confused by the following two ways of relating logic systems and programming languages or type systems. In ...
user avatar
  • 1
1 vote
0 answers
75 views

Equivalent terms in call-by-name but not in call-by-value

Working in the untyped lambda-calculus, I'm asked to give two terms that are equivalent in call-by-name semantics but not in call-by-value. Call $\text{fls} = \lambda x. \lambda y. y$ and $\Omega = (\...
user avatar
  • 2,220
2 votes
1 answer
33 views

Finding two store typings that make the same store valid (lambda-calculus with references)

Problem 13.5.2 of Pierce's TAPL's book (page 167) asks: Can you find a context $\Gamma$, a store $\mu$ and two different store typings $\Sigma_1,\Sigma_2$ such that both $\Gamma | \Sigma_1 \vdash \...
user avatar
  • 2,220
7 votes
1 answer
169 views

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

The simply typed lambda-calculus with numbers and fix has long been a favorite experimental subject for programming language researchers, since it is the simplest language in which a range of subtle ...
user avatar
  • 2,220
3 votes
1 answer
88 views

An operational semantics for lambda-calculus normal order evaluation strategy

TAPL book, page 56 reads: Under the normal order strategy, the leftmost, outermost redex is always reduced first. I understand this as a restriction of the full beta-reduction evaluation ...
user avatar
  • 2,220
3 votes
1 answer
70 views

Is $\Gamma \vdash x x : T$ possible in the simply typed lambda calculus?

Is $\Gamma \vdash x x : T$ possible? This problem appears on page 104 of Benjamin Pierce's "Types and Programming Languages". My conclusion is that it is was the case then we would get $x: T_1 \to ...
user avatar
  • 2,220
1 vote
1 answer
55 views

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

In Types and Programming Languages by Pierce, ML-style let-polymorphism was first described by Milner (1978). A num- ber of type reconstruction algorithms have been proposed, notably the clas- ...
user avatar
  • 1
-1 votes
1 answer
121 views

What is "Hindley-Milner (i.e., unification-based) polymorphism"?

In Types and Programming Languages by Pierce, Ch11 Simple Extensions extends the typed lambda calculus. Section 11.5 Let Bindings says: In Chapter 22 we will see another reason not to treat let as ...
user avatar
  • 1
3 votes
0 answers
131 views

Does Hindley-Milner refer to the unification algorithm for type reconstruction, a type system, or a form of polymorphism? [closed]

What does Hindely-Milner refer to? In Types and Programming Languages by Pierce, I only find that Section 22.4 Unification mentions "Hindley" and "Milner", when introducing the unification algorithm. ...
user avatar
  • 1
1 vote
1 answer
128 views

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

Types and Programming Languages book introduces a theorem about principles of induction on term (p. 31, theorem 3.3.4): Suppose P is a predicate on terms. Induction on depth: If, for each ...
user avatar
  • 113
1 vote
1 answer
70 views

What does valid method overriding mean?

In Types and Programming Languages by Pierce, from p257 to p258, about featherweight Java, The predicate override(m, D, C→C0) judges whether a method ...
user avatar
  • 1
1 vote
2 answers
94 views

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

In Types and Programming Languages by Pierce, Section 18.6 Simple Classes in Chapter 18 Imperative Objects says: We should emphasize that these classes are values, not types. Also we can, if we ...
user avatar
  • 1
1 vote
1 answer
43 views

Why can System F1 a.k.a. λ → have kind `*`, but no quantification `∀`?

In Types and Programming Languages by Pierce, on p461 in Section 30.4 Fragments of 30.4.1 Definition: In System F1 , the only kind is ...
user avatar
  • 1
1 vote
1 answer
66 views

Is `→` a type operator?

In Types and Programming Languages by Pierce, The level of types contains two sorts of expressions. First, there are proper types like Nat, Nat→Nat, Pair Nat Bool, and ∀X.X→X, which are ...
user avatar
  • 1
1 vote
0 answers
85 views

Is the language "untyped arithmetic expressions" in Types and Programming Languages not Turing complete?

In Types and Programming Languages by Pierce, is it correct that the language introduced in Chapter 3 Untyped Arithmetic Expressions is not Turing complete? Because it doesn't provide recursion. the ...
user avatar
  • 1
2 votes
1 answer
81 views

What are the differences and relations between a type constructor and a type operator?

What are the definitions of a type constructor and a type operator? What are their differences and relations? I think a type operator is a function whose parameters are n types and return is a type. A ...
user avatar
  • 1
1 vote
2 answers
282 views

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

In Types and Programming Languages by Pierce, how does the following achieve the definition of an existential type in terms of universal type, by polymorphic version of Church encoding of pairs? ...
user avatar
  • 1
1 vote
1 answer
58 views

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

In Types and Programming Languages by Pierce, Chapter 23 Universal Types has a summary of System F in the following figure, in particular, "type abstraction values" and their types "universal types". ...
user avatar
  • 1
1 vote
1 answer
39 views

What is the purpose of erasing a type application to a term-application in parametric polymorphism?

From Types and Programming Languages by Pierce 23 Polymorphism 23.7 Erasure and Evaluation Order in a full-blown programming language, which may include side- effecting features such as ...
user avatar
  • 1
1 vote
1 answer
93 views

Does a term being normalizable mean the same as the term has a normal form?

From Types and Programming Languages by Pierce A term $t$ is in normal form if no evaluation rule applies to it— i.e., if there is no $t'$ such that $t -→ t'$. and A term $t$ is typable (or ...
user avatar
  • 1
0 votes
1 answer
108 views

Do the following concepts belong to syntax or semantics?

I am not very sure about the difference between syntax and semantics. Does each of the following concepts belong to syntax or semantics? terms values: terms that are possible final results of ...
user avatar
  • 1
1 vote
1 answer
253 views

Do determinacy of one-step evaluation and uniqueness of normal forms apply to all (or most) languages in TAPL?

In Types and Programming Languages by Pierce, when talking about untyped arithmetic expressions in Chapter 3, there are two theorems: $-→$ is single-step evaluation relation: 3.5.4 Theorem [...
user avatar
  • 1
1 vote
1 answer
64 views

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

In Types and Programming Languages by Pierce et al: The recursive equation specifying the type of lists of numbers is similar to the equation specifying the recursive factorial function on page 52: ...
user avatar
  • 1
2 votes
0 answers
33 views

Region-based memory management for recursive type

In the chapter 4 of Pierce's TAPL which discusses the implementation of untyped arithmetic expressions, the author said The most important [for the implementation requirements] are automatic ...
user avatar
1 vote
1 answer
97 views

Find typing derivation of STLC term with reference types

The problem is to find the typing derivation of a term of the call-by-value STLC extended with reference types. The evaluation and typing rules for this language is given in Types and Programming ...
user avatar
7 votes
1 answer
145 views

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

In "Types and Programming Languages", Pierce gives a translation from recursive types ($\mu$ types) to types expressed as regular trees: possibly infinite trees, but with finitely many distinct ...
user avatar
  • 29.1k
2 votes
1 answer
129 views

Isoecursive Types When to Fold and Unfold

I'm trying to implement recursive types into my programming language. I've implemented extensible rows and was hoping to add some recursive typing in order to get something like ...
user avatar
2 votes
1 answer
59 views

T&PL: Language grammar with terms

I'm autodidacting Pierce's Types and Programming Languages. On page 27 he states a definition for "terms, concretely" in constructing a language of terms, thus: For each natural number $i$, ...
user avatar
  • 131
1 vote
0 answers
71 views

Mathematical resource material accompanying TAPL

I'm currently reading Types and Programming Languages by Benjamin C. Pierce and just arrived at chapter 21 Metatheory of Recursive Types. Prior to this chapter I found the book challenging but ...
user avatar
1 vote
1 answer
89 views

Bounded Quantification: Full F<: intuition

I'm currently looking into Chapter 26 of Types and Programming Languages and am a bit confused by the "intuition" for Full F<: (p. 395): A type T = ∀X<:T1.T2 describes a collection of ...
user avatar
  • 13
2 votes
2 answers
275 views

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

I'm working through Types and Programming Languages right now, and I'm a little confused about the recursive definition given for nameless/de Bruijn terms (chapter 6, definition 6.1.2). Below is the ...
user avatar
  • 123
4 votes
1 answer
482 views

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

type checking I was preparing examples of type checking in simply typed $\lambda$-calculus. I wanted to explain it to my audience in the way of implementation. And I found a bit tricky point in the ...
user avatar
  • 1,042
6 votes
2 answers
367 views

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

I've recently started independently learning type theory, using a combination of papers found online and ncatlab.org (but have not worked with category theory), and am about to start reading TAPL. I'...
user avatar
  • 163
6 votes
3 answers
391 views

Proving property of a term using Induction

This is one of the example lemma that has been proved in TAPL book which I'm unable to grasp. The objective is to prove |Consts(t)| <= size(t) where ...
user avatar
  • 161
4 votes
1 answer
91 views

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

The book "Types and Programming Languages" said System F sub type checking introduce exposure typing rules alongside algorithmic typing and sub-typing rules. ...
user avatar
  • 1,042
3 votes
1 answer
195 views

how type checking fails?

I was doing a type checking example in system f sub on paper to understand how it works. according to Pierce's book Types and Programming Languages, numbers and their types are following in system f ...
user avatar
  • 1,042
6 votes
1 answer
1k views

call by value: what is a value?

In the 'call by value' evaluation of lambda-calculus, I am bit confused with 'value'. On page 57 of the book Types and Programming languages, it is said: The definition of call by value, in which ...
user avatar
  • 1,042
5 votes
1 answer
346 views

Why injection into sum type apparently leads to ambiguity?

I have been reading Benjamin Pierce's Types and Programming Languages, plus a couple of course notes on type systems and typed $\lambda$-calculus, and there is one thing I don't get: it seems that ...
user avatar
  • 331