Questions tagged [type-theory]
formal systems to specify properties of objects
400
questions
5
votes
2answers
210 views
Are “logarithm types” a thing?
I'm attempting to formalize some thoughts I've had about paths into data structures. For example, a path into a list of Ts might be a pair of an index with a path ...
2
votes
0answers
36 views
Simulating extensible sums with dependent types?
ML-style languages have a concept of "extensible" or "open" sum types, where variants can be declared at any point, and there's not a fixed number of constructors for the type. They're usually used to ...
5
votes
0answers
39 views
Rules for consistency with mutual inductive families?
I'm trying to use a proof assistant to define a type and a relation that are mutually dependent on each other:
...
0
votes
1answer
96 views
Is this statement of P = NP in Agda correct?
Looking for a self-contained statement of P = NP in type theory, I stumbled upon this short Agda formalization (a cleaned up version is reproduced below).
The statement here does seem to express the ...
0
votes
0answers
33 views
How is substitution in type theory the composition of classifying morphisms in category theory?
In the article at nlab about relation between category theory and type theory, it is said that substitution in type theory is the same as composition of classifying morphisms in category theory.
...
1
vote
0answers
24 views
Is, beta reduction in type theory being considered as counit for hom-tensor adjunction in category theory, a denotational or operational semantic?
In the article at nlab about the relation between type theory and category theory, it is said that "beta reduction" in type theory corresponds to "counit for hom-tensor adjunction" in category theory ...
0
votes
1answer
70 views
What is the language feature which allows a variable to be associated with values of different types?
In Python, I can change the types of values associated with a variable:
>>> x=1
>>> x="abc"
In C, I can't do the same.
What is the name of ...
-1
votes
1answer
45 views
Is the choice of static and dynamic typing not visible to the programmers of the languages? [closed]
From Design Concepts in Programming Languages by Turbak
Although some dynamically typed languages have simple type markers (e.g., Perl variable names begin with a character that indicates the type ...
2
votes
2answers
36 views
Are type variables really only used in mathematical conversation about types?
Are type variables really only used in mathematical conversation about types? i.e. are type variables (meta-variables that only contain the type classification label) only exist in proofs for types ...
0
votes
1answer
56 views
What is the difference between $ \alpha \to \alpha $ vs $ \forall \alpha. \alpha \to \alpha$?
I was studying polymorphic types and I was finding the distinction with monomorphic types difficult to pin down (context CS 421). From the course I linked the have the following (vague attempt) at a ...
5
votes
1answer
73 views
What does $ \forall \alpha_1, \dots , \alpha_n . \tau $ mean formally as a type?
I was learning about polymorphic types but I couldn't understand the notation, can someone explain it means (context cs421 UIUC):
$$ \forall \alpha_1, \dots , \alpha_n . \tau $$
its supposed to be a ...
0
votes
1answer
42 views
How do you define and parse variables (free or bound) from user-entered strings?
I'm writing an application in which the user might enter expressions such as $\text{lim}_{i \in I} \beta(i)$ where $\beta$ is a functor. That's just an example, the expressions, which contain ...
2
votes
1answer
47 views
How is β-reduction a 2-morphism in Category theory?
According to Categorifying CCCs: Computation as a Process, computation or β-reduction process in untyped-lambda calculus is in fact a 2-morphism in category theory.
Can someone please describe me ...
1
vote
0answers
20 views
Do Rank-1 (prenex) polymorphism and Predicative polymorphism mean the same?
https://en.wikipedia.org/wiki/Parametric_polymorphism says:
Rank-1 (prenex) polymorphism
In a prenex polymorphic system, type variables may not be instantiated with polymorphic types.[4] ...
1
vote
0answers
22 views
What are the relation and differences between reification and type passing semantics?
https://en.wikipedia.org/wiki/Type_erasure says
type erasure refers to the load-time process by which explicit type annotations are removed from a program, before it is executed at run-time. ...
0
votes
0answers
20 views
What are the relations between these two descriptions of let polymorphism?
In Types and Programming Languages by Pierce, there are two descriptions of let-polymorphism.
Sec23.8 Fragments of SystemF on p359 says
This has led to various proposals for restricted fragments ...
0
votes
1answer
29 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
votes
1answer
46 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 ...
2
votes
0answers
21 views
Does Hindley-Milner refer to the unification algorithm for type reconstruction, a type system, or a form of polymorphism?
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.
...
0
votes
0answers
22 views
Is it possible to deduce type from the lambda form?
I was continuing the exploration of lambda world this summer. When I take a look at the simply typed lambda calculus, it looks like there is no use for usual chuch numerals and boolean forms anymore. ...
1
vote
1answer
49 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 ...
0
votes
1answer
26 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
vote
2answers
50 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 ...
9
votes
1answer
1k views
Why does Coq include let-expressions in its core language
Coq includes let-expressions in its core language.
We can translate let-expressions to applications like this:
let x : t = v in b ~> (\(x:t). b) v
I understand ...
1
vote
1answer
25 views
Does an ADT have multiple or only one representations/implementations?
Section 24.2 in Types and Programming Languages by Pierce defines ADTs in existential types:
A conventional abstract data type (or ADT) consists of (1) a type name A, (2) a concrete representation ...
0
votes
1answer
19 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
votes
1answer
43 views
What order logic does a system correspond to under Curry–Howard correspondence?
In Types and Programming Languages by Pierce,
Section 9.4 Curry–Howard correspondence on p109 has a table
Does the table mean that the simply typed lambda calculus ...
0
votes
0answers
10 views
Can two type expressions in different kinds have subtyping relation and equivalence relation?
In Higher-order bounded quantification ($F^ω_{<:}$), introduced in Ch31 in Types and Programming Langauges by Pierce, its subtyping and equivalence rules are:
Does subtyping relation only exist ...
0
votes
0answers
33 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 ...
0
votes
0answers
23 views
Does λ→ have type operators?
In Types and Programming Languages by Pierce, Ch11 Simple Extensions introduces λ→ as the simply
typed lambda calculus with simple extensions, and introduces <...
0
votes
0answers
24 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 ...
0
votes
0answers
14 views
How can we directly reaching inside and looking at the state of a partially existential object?
Types and Programming Languages by Pierce says in Section 26.5 Bounded Existential Types, about partial existential objects implemented in terms of bounded existential types:
We can make a similar ...
0
votes
0answers
26 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 ...
0
votes
1answer
45 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?
...
0
votes
1answer
58 views
Why are ADT packages opened immediately after they are built, while existential objects opened as late as possible?
Section 24.2 in Types and Programming Languages by Pierce defines ADTs in existential types:
A conventional abstract data type (or ADT) consists of (1) a type name A, (2) a concrete representation ...
0
votes
1answer
59 views
How can mainstream OO languages support strong binary operations by classes?
Section 24.2 in Types and Programming Languages by Pierce compares ADT and existential objects,in terms of how well they support strong binary operations:
Other binary operations cannot be ...
0
votes
1answer
38 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".
...
0
votes
1answer
36 views
How does this allow list operations to be applied to lists with elements of any type?
In Types and Programming Languages by Pierce, Chapter 11 is simple extensions of the simply typed lambda calculus with any simple base types. Section 11.12 introduces Lists.
How does the section ...
0
votes
1answer
26 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 ...
0
votes
1answer
26 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 ...
0
votes
1answer
68 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
vote
1answer
22 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
vote
1answer
28 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:
...
0
votes
0answers
31 views
General term for upcasting and downcasting?
Is there a more precise term than simply "casting"? "Casting" often includes for example integer -> float or ...
3
votes
0answers
54 views
Calculus of constructions, type-in-type and recursion
Does adding type-in-type to the calculus of constructions lead to (general) recursion? Such that one can write the Y combinator.
0
votes
0answers
34 views
How do you derive a type $∃e(e)$ in terms of universally quantified types, without invoking Void initially?
I wrote a "proof" for this, and though it was enough to convince myself, there are a few things that bother me about it. Primarily I'm not sure about the loose way in which I'm swapping between first-...
0
votes
1answer
35 views
Could following be a counter example to Church-Rosser (Confluence) theorem?
According to the "Type Theory and Formal Proof" book, Church-Rosser theorem (confluence) is as follow:
Suppose that for a given term $M$, we have $M \twoheadrightarrow_\beta N_1$ and $M\...
5
votes
1answer
138 views
What does canonicity property mean in Type Theory?
The "Computational Component" section of the Type Theory - Wikipedia (as well as a few papers about cubical type theory and 2d type theory) talk about canonicity property.
Would you please explain ...
2
votes
1answer
80 views
Difference between computation in proposition proof and definitional computation?
As stated in equality at nLab, "computational equality" is about computational steps which take for example, $s(s(0))+ s(0)$ to $s(s(s(0)))$ and it acts exactly and can be considered same as ...
4
votes
2answers
66 views
Why values can not be replaced with their extensionally equal values in an intensional system?
Thomas Streicher states in Investigations into Intensional Type Theory(§Introduction p.5) that:
Although in Intensional constructive set theory (Intensional Type Theory) one can do most of the ...
