Questions tagged [type-theory]
formal systems to specify properties of objects
422
questions
1
vote
0answers
5 views
Type inference with overloading
I am working on a type system supporting overloading. I have a rough idea of how type inference is usually implemented in such a scenario, but I am wondering how - after type inference is completed - ...
3
votes
1answer
211 views
How to get an element from an existential proposition in Type theory proof assistant (Lean prover)
I am trying to implement set theory in type theory from scratch, just for self pedagogical purposes. Specifically, I'm using the Lean Prover, and defining the element-of relation from scratch using ...
1
vote
2answers
40 views
Tightening application rules for STLC
The syntax STLC is usually written:
$e ::= x |\lambda x : \tau . e|(e \space e)|c$
However, the application rule appears to accept all expressions on the left hand side. Shouldn't the application ...
1
vote
0answers
17 views
Proof of Subject-Expansion Theorem in Type Theory
I am beginning to study type theory, using Hindley's book "Basic Simple Type Theory", and I would like your help in the proof of a theorem. I would like to know whether my idea for how to prove the ...
0
votes
1answer
33 views
Is there any correspondence between SUM type in type theory and arithmetical summation?
Is there any correspondence between the coproduct(sum) type in type theory and arithmetical summation?
For example what does 3+4 or x+6 mean in type theory?
3
votes
2answers
44 views
Parentheses after Typing Environment
I've been reading about System F Omega lately, and I keep stumbling across a construct in typing rules that I cannot find an explanation of: Γ(x) = k. For example, ...
2
votes
1answer
24 views
Type inference with imports
I understand how a type inference algorithm infers types within a single file by building on top of already inferred types and identified constraints (e.g. in the Hindley-Milner type system).
I am ...
4
votes
2answers
543 views
Does the underlying computational calculus in type theories affect decidability?
I'm looking for a high-level explanation although if that isn't possible or difficult, I'd prefer references to books/papers.
I understand that modern type theory is inspired by Curry-Howard ...
1
vote
0answers
39 views
Does Type:Type lead to inconsistency without general inductive types?
In e.g. Agda , it is possible to derive an element of the empty type by enabling the "type in type" option.
Every proof I have seen (and come up with) involves making a special inductive type ...
1
vote
2answers
42 views
What is the differences and similarities between refinement type and liquid types?
Looking at the examples here and here both refinement type and liquid types look very similar. What are the differences and similarities?
3
votes
2answers
101 views
When is cumulative type universes useful?
AFAIK, a hierarchy of type universe(Type^0: Type^1: Type^2: ...) was introduced to avoid inconsistency caused by Type: Type.
...
2
votes
0answers
23 views
Is possible to construct a fixed set of typeclases as powerful as unconstrainde typeclasses?
We can construct a fixed set of combinators with a computational power equivalent to lambda calculus.
Can we do the same with typeclasses (ad-hoc polymorphism)?
For example, construct a finite set ...
6
votes
2answers
77 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 ...
5
votes
2answers
2k views
What do the ∀ and ∃ symbols mean in the Axiom of Choice?
On the Wikipedia page for the Axiom of Choice the following statement is given:
$(\forall x^\sigma)(\exists y^\tau)R(x,y)\rightarrow(\exists f^{\sigma \rightarrow \tau})(\forall x^\sigma)R(x, f(x))$
...
0
votes
0answers
43 views
What is the difference between a Type and an Abstract Type?
In my data structures course we are given definitions for Type and Abstract Type but they confuse me.
A type is a set of values and the operations you can do on them. The set of operations is ...
0
votes
0answers
41 views
in the lambda calculus with products and sums is $f : [n] \to [n]$ $\beta\eta$ equivalent to $f^{n!}$?
$\eta$-reduction is often described as arising from the desire for functions which are point-wise equal to be syntactically equal. In a simply typed calculus with products it is sufficient, but when ...
1
vote
1answer
46 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 \;...
1
vote
0answers
36 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 ...
1
vote
1answer
85 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 \...
3
votes
0answers
30 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
votes
0answers
56 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 ...
3
votes
0answers
25 views
What the type of an overloaded function should be?
Anecdotally, Virgill III language forbids overloading since overloading resolution is at odds with the language support of functions as first-class citizen, when resolution can't happen at compile ...
3
votes
0answers
42 views
Derivation of product type eliminator in type theory
In HoTT book, section 1.5 (Product Types) in order to define the eliminators for the product type it assumes a function of type $g:A \rightarrow B \rightarrow C$ and then goes on to define the ...
2
votes
0answers
60 views
How could 'Complete and Easy Bidirectional Type Checking' handle invariant parameters on type constructors
The paper Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism provides examples for checking if one function type is a subtype of another, which I think demonstrates checking ...
5
votes
2answers
254 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
43 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
41 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
117 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
39 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
26 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
78 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
47 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
45 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 ...
1
vote
1answer
96 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
83 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 ...
-1
votes
1answer
50 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
64 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
36 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
29 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
27 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
32 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
53 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
35 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
24 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
53 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
28 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
63 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
45 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
25 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 ...
