Questions tagged [types-and-programming-languages]
For questions about the book "Types and Programming Languages" by Benjamin Pierce, and the exercises from the book.
71
questions
2
votes
1
answer
135
views
Difference between Data Type and Data Structure
I don't get what is the difference between a Data Type and Data Structure.
As per Wikipedia, "Some types are very useful for storing and retrieving data and are called data structures". But:
...
- 21
0
votes
0
answers
32
views
Completeness of bidirectional type checking by inversion
I'm currently reading through the completeness proof of the paper "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism" by Dunfield et al.
In the second case Dunfield ...
2
votes
1
answer
34
views
Benjamin Pierce Types and Programming Languages 6.1.5 Clarification
I'm currently following Pierce's Types and Programming Languages, and I find myself stuck at exercise 6.1.5 (the implementations of removenames? and restorenames?). The rules are as follows:
...
- 23
1
vote
2
answers
69
views
How are conflicts between free and bound de Bruijn indices resolved?
On page 77 (section 6.1) of Types and Programming Languages by Benjamin C. Pierce (1st and only edition thus far), there is the following quote regarding naming contexts and de Bruijn indices:
Γ = x ...
- 175
1
vote
0
answers
37
views
What logical system does hindley-milner correspond to, according to the curry howard correspondence?
If I understand CHC correctly, simply typed lambda calculus corresponds to propositional logic. As HM allows polymorphic definitions by let-expressions, my guess is that it would correspond to a ...
- 36
0
votes
0
answers
82
views
Semantics Equivalence of Structural Semantics of While Programming Language
I'm taking a course about the formality of programming languages and while reading Semantics with Applications: An Appetizer by H.R Nielson and F. Nielson
I came across the following exercise:
I'm ...
2
votes
2
answers
169
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,131
3
votes
2
answers
144
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,131
5
votes
1
answer
251
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? ...
- 183
1
vote
1
answer
70
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
143
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,204
1
vote
0
answers
81
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,204
6
votes
3
answers
296
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 ...
- 659
2
votes
1
answer
63
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,204
1
vote
0
answers
50
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,204
2
votes
1
answer
111
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,204
3
votes
0
answers
56
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,204
2
votes
0
answers
100
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,204
1
vote
2
answers
72
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 ...
- 4,975
2
votes
1
answer
38
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,204
8
votes
1
answer
269
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,204
3
votes
1
answer
117
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,204
3
votes
1
answer
82
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,204
1
vote
1
answer
85
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-
...
- 4,975
-1
votes
1
answer
216
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 ...
- 4,975
4
votes
0
answers
198
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.
...
- 4,975
3
votes
1
answer
276
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 ...
- 133
1
vote
1
answer
89
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
...
- 4,975
1
vote
2
answers
110
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 ...
- 4,975
1
vote
1
answer
53
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 ...
- 4,975
1
vote
1
answer
92
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 ...
- 4,975
2
votes
0
answers
109
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 ...
- 4,975
2
votes
1
answer
194
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 ...
- 4,975
1
vote
2
answers
454
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?
...
- 4,975
1
vote
1
answer
73
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".
...
- 4,975
1
vote
1
answer
52
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 ...
- 4,975
1
vote
1
answer
122
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 ...
- 4,975
0
votes
1
answer
131
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 ...
- 4,975
2
votes
1
answer
354
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 [...
- 4,975
1
vote
1
answer
90
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:
...
- 4,975
2
votes
0
answers
43
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
121
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,250
7
votes
1
answer
168
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.9k
2
votes
1
answer
176
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 ...
- 205
2
votes
1
answer
78
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
79
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
92
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
312
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 ...
- 163
5
votes
1
answer
626
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,024
6
votes
2
answers
593
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