Questions tagged [type-theory]
formal systems to specify properties of objects
544
questions
0
votes
0
answers
31
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 ...
1
vote
1
answer
57
views
How to determine whether two recursive data types overlap
I am working on a type system that supports recursive data types, e.g.:
type a = (a * integer) | integer
type b = integer
would be valid type declarations, where <...
- 13
1
vote
1
answer
57
views
Can and does any statically typed programming language safely support in-place type-conversion?
Here's some hypothetical rust-inspired language syntax to show what I mean
...
- 113
4
votes
1
answer
351
views
Is there a fully combinatorial version of MLTT without lambda abstraction?
I have been learning MLTT and working on implementing its type checker referencing Coq's core language specification. Currently, I am at the stage of implementing its termination checker. I find it ...
- 173
1
vote
1
answer
64
views
Definition of semantics of coinductive type
It is relatively easy to construct an object in set/class theory which has properties of any of the following: dependent sum, dependent product, W-types.
E.g. Dependent sum of a family F is just the ...
- 111
1
vote
1
answer
46
views
In what sense do universes solve the problem of not having type $\Pi_{A:\text{Type}}B(A)$?
One motivation for introducing universes, as I see it, is that without universes, we cannot construct types like $\Pi_{A:\text{Type}}B(A)$ because they would require us to have $\Gamma.\text{Type}\...
user164153
1
vote
0
answers
41
views
Dependent Types in $\lambda P$ vs MLTT
I am trying to understand the difference between $\lambda P$ and MLT, in particular the dependent type features.
What is the difference between dependent types in $\lambda P$ and dependent types in ...
- 131
2
votes
1
answer
43
views
Adding type constructors to universes
Suppse we have a Tarski-style universe $U$, which means, in particular, that the following rules are declared: $$\frac{}{\Gamma \vdash U \text{ type}} \quad \frac{\Gamma \vdash a:U}{\Gamma \vdash \...
user164153
2
votes
0
answers
47
views
Are there type theories for formalizing constructive metric space theory?
I suspect the type theory may not be considered fully constructive, but I am interested in hearing about any type theory that can formalize some amount of metric space theory or analysis.
- 131
1
vote
0
answers
37
views
Analog of semantic paradoxes in type theory?
By semantic paradoxes, I mean like the Liar paradox, Curry paradox, Knower paradox, etc.
In classical (logic) settings, we would need to extend the language with a predicate P (truth or is-known ...
- 246
1
vote
0
answers
41
views
What is the significance of the equation $\langle \pi_1 M, \pi_2 M \rangle = M$ in $\lambda$-calculus?
When extending the simply typed $\lambda$-calculus with products, we extend $\beta$-reduction with the rules $\pi_i \langle M_1, M_2 \rangle \to_\beta M_i$, which makes sense (cf. Sørensen, Urzyczyn, ...
- 131
0
votes
2
answers
50
views
Reference types
Is a reference type (agnostic of PL) the object being pointed at, or the object doing the pointing?
I'm having a hard time wrapping my head around the concept fundamentally (of course, I have ...
- 183
2
votes
1
answer
28
views
Is limiting the input type in subclasses legitimate (does it give a stronger or the same specification)?
Note: I have read a similar post, but my problem seems different from that. Read my attempts to understand the problem for why I believe they are different.
My problem:
I know that (see this and this)
...
- 123
1
vote
1
answer
121
views
Are languages generated from a statically typed language statically typed?
Are languages generated from a statically typed language statically typed?
So say, generating Python from C++.
to generate a language from another language:
You write a transpiler in a static language ...
- 579
2
votes
2
answers
380
views
Algorithm that generates verification program from solution program of NP problem
I don't know complexity class theory well so I might make some categorical errors, but I will try to ask this question anyways.
Suppose you have written a function in some programming language which ...
- 121