Questions tagged [type-theory]

formal systems to specify properties of objects

Filter by
Sorted by
Tagged with
1
vote
1answer
37 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 \...
1
vote
0answers
28 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 ...
0
votes
0answers
14 views

Cayley diagram for Frieze group

In Type Theory there is Rule: Every action is reversible. There are 7 groups for 1d repeating pattern (Frieze groups). Group 1: only translations. Group 2: only glide reflection. Why Cayley ...
-1
votes
0answers
33 views

Why are the domains of operations in the existential type that represents a dynamic dispatch product types not sum types?

Regarding dynamic dispatching, Practical Foundation of Programming Languages by Harper says: Dynamic dispatch is an abstraction given by the following components: An abstract type $t_{obj}$...
0
votes
2answers
42 views

What is the single type in a dynamic typing language?

Regarding static typing and dynamic typing, Practical Foundation of Programming Languages by Harper says: There have been many attempts by advocates of dynamic typing to distinguish dynamic from ...
1
vote
1answer
38 views

Do dynamic/static languages associate types or classes to values or variables?

In Practical Foundation of Programming Languages by Harper There have been many attempts by advocates of dynamic typing to distinguish dynamic from static languages. It is useful to consider ...
0
votes
1answer
32 views

Doubts on the behavior of Unit Type in a type system

I have a doubt about the Unit Type in the context of Type Theory and its use in different case scenarios. To start with, a Unit Type can be seen as a nullary Product Type, namely Unit, with one only ...
3
votes
1answer
58 views

What are Contexts in Lambda Calculus?

What is a Context? Is it like a scope in C? Does it have a start and an end? Can contexts contain other contexts? I see Contexts being used in lambda calculi type system rules, but I don't understand ...
3
votes
1answer
47 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 ...
3
votes
1answer
66 views

What is the formalism to prove statements about uniqueness of functions with certain signatures

Suppose I want a function like f: ((A, B) -> C) -> A -> B -> C A statement I've often seen made is that f has just one implementation, namely the '...
1
vote
1answer
33 views

Why F-bounded polymorphism and F-bounded quantification are called, well, F-bounded

It's claimed in Wikipedia that: F-bounded quantification or recursively bounded quantification, introduced in 1989, allows for more precise typing of functions that are applied on recursive ...
1
vote
1answer
25 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 - ...
2
votes
2answers
57 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 ...
3
votes
1answer
234 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 ...
5
votes
2answers
565 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
27 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
34 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
45 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
28 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 ...
0
votes
1answer
93 views

Is it possible to interpret some Martin-Löf types as abelian monoids in such a way that any abelian monoid can be represented as a type?

For instance, I can interpret the unit type as the trivial monoid with one element. Non-dependent pairs $A \times B$ can be interpreted as the direct sum $A ⊕ B$ when $A$ and $B$ can both be ...
1
vote
2answers
104 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
vote
0answers
43 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
1answer
38 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
vote
1answer
49 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
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
2answers
47 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
110 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. ...
6
votes
2answers
83 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 ...
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 ...
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
44 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 ...
11
votes
1answer
1k views

What is induction-induction?

What is induction-induction? The resources I found are: the HoTT book, at the end of chapter 5.7. nLab's article a paper called Inductive-inductive definitions this blog post also mentions inductive-...
1
vote
1answer
47 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
86 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
31 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 ...
2
votes
0answers
65 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
259 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
45 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
120 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
42 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. ...
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
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
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- ...
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
49 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 ...

1
2 3 4 5
9