Questions tagged [types-and-programming-languages]
For questions about the book "Types and Programming Languages" by Benjamin Pierce, and the exercises from the book.
66
questions
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₁...
- 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 ...
- 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? ...
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 ...
- 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 \...
- 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 ...
- 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 ...
- 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 \;...
- 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 ...
- 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 \...
- 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$
...
- 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 ...
- 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 ...
- 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 = (\...
- 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 \...
- 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 ...
- 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 ...
- 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 ...
- 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-
...
- 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 ...
- 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.
...
- 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 ...
- 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
...
- 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 ...
- 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 Fω
30.4.1 Definition: In System F1 , the only kind is ...
- 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 ...
- 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 ...
- 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 ...
- 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?
...
- 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".
...
- 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 ...
- 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 ...
- 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 ...
- 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 [...
- 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:
...
- 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 ...
- 151
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 ...
- 1,024
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 ...
- 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 ...
- 175
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$, ...
- 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 ...
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 ...
- 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 ...
- 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 ...
- 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'...
- 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 ...
- 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.
...
- 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 ...
- 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 ...
- 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 ...
- 331