Questions tagged [type-theory]

formal systems to specify properties of objects

Filter by
Sorted by
Tagged with
2
votes
1answer
39 views

What are the implications of Homotopy Type Theory?

I've recently come across the topic of homotopy type theory and I'm interested to learn more. I have a very limited background in type theory. Can anyone tell me, in functional programming terms or ...
0
votes
0answers
14 views

Is the borrow checker mechanism in Rust based on quantitative types?

I was trying to understand if the borrow checking mechanism for references is actually a quantitaive type in disguise because it does look very similar. In case these are just similar but unrelated ...
2
votes
1answer
48 views

How does the undecidability of Extensional Martin-Löf Type Theory apply to real type-checking compilers?

It is claimed in many sources (for example, here) that adding a rule like "if Id(X,Y) then X really equals ...
0
votes
1answer
38 views

How do you have a type typed “Type” when implementing a programming language?

I am working on the base of a language model, and am wondering how to represent the base type, which is a type Type. I have heard of an "infinite chain of ...
2
votes
4answers
410 views

Is there such thing as “sequential types”?

I am wondering how you could possibly define the implementation of an imperative function as a type. Is it possible? Currently I only see the input parameters and output result used in the definition ...
0
votes
0answers
75 views

Can we think of a non-symmetric product type in Haskell?

Meta note: I asked this question here a while ago. It got an answer: type a /\!! b = (a, ((b -> Void) -> Void)) Unfortunately, I do not reckon it to be ...
0
votes
2answers
70 views

Interpreting a proof of $2^\mathbb{N}$ being uncountable

Suppose I have the following proof: ...
1
vote
1answer
56 views

What's the difference between Row Polymorphism and Structural Typing?

The definitions I've stumbled across seem to indicate they express the same idea. That's that the relationship between record types is determined by their fields (or properties) rather than their ...
1
vote
1answer
34 views

Example of Dependent Types?

Say you have 3 objects, a global MemoryStore, which has an array of MemorySlabCache objects, and each ...
0
votes
0answers
64 views

Consistency of a set of bidirectional typing rules

Main Is there any way to algorithmically check the consistency of a set of bidirectional typing rules, e.g. the absence of cycles and the uniqueness of the derivation tree? This problem is naturally ...
2
votes
1answer
45 views

Does canonicity imply weak normalization?

Context: type theory. My understanding of: WN: every term can rewrite to NF. Canonicity: every term rewrites into canonical form. Then it leads to an intuition where if canonicity holds, then we get ...
3
votes
0answers
47 views

Semantics of “write-once” variables for complex data structures

Question My use case for what is described below is not a language or compiler implementation, but finding a reasonable semantics for this feature in a an abstract calculus. Ideally, you give me a ...
3
votes
1answer
348 views

Why do we need a separate notation for П-types?

Main I am confused about the motivation behind the need for a separate notation for П-types, that you can find in type systems from λ2 on. The answer usually goes like so - think about how one can ...
1
vote
1answer
99 views

Creating a large tuple from smaller tuples via a monad or applicative

Suppose I have a term $a :\alpha$ of the Simply-Typed Lambda Calculus (in the following, $\alpha, \beta, \gamma$ stand for arbitrary types) and I want to lift it to a term $\lambda x_{\beta}. \;(x, \, ...
2
votes
0answers
43 views

Difference between the logic and the type system of a proof assistant?

In Comparing Mathematical Provers (section 4.1), Wiedijk classifies logics and type systems of different proof assistants? I do not see what he means by type system of the assistant. He only says: A ...
3
votes
0answers
86 views

(Co)-monads and terminating implementations

The bounty above should read 'I would like to know whether the example I discuss is a com-monad and why (why not).' Suppose we set $\mathbb{M} \alpha := r \to \alpha$, where $r$ is some fixed type, ...
3
votes
1answer
252 views

The meaning and relevance of the locution ''no terminating implementation'' in type theory

In the context of a discussion of Haskell https://stackoverflow.com/questions/62509788/the-intuition-behind-the-definition-of-the-co-reader-monad, I was told that There is no terminating ...
1
vote
0answers
85 views

How do type classes make ad-hoc polymorphism less ad hoc?

The title of the paper that introduced type classes is "How to make ad-hoc polymorphism less ad hoc". It seems the type classes approach is being compared to how OOP does ad-hoc polymorphism....
1
vote
2answers
77 views

How to express a type that represents an associative array whose keys determine the type of the value?

I'm fairly new to type systems and theory, so I would appreciate some guidance in a problem that sparked my interest. I would like to understand what type system features are required so a compiler ...
2
votes
0answers
48 views

Inhabitation of STLC is in PSPACE

Urzyczyn: Inhabitation in Typed Lambda-Calculi (A syntactic approach) gives a proof that STLC inhabitation problem is in PSPACE (section 2, lemma 1). I don't understand certain aspects of the proof: ...
1
vote
1answer
42 views

Terms for different models of sum types

There seem to be at least a couple different possible ways of modeling sum types in a type system, but I haven't been able to find consistent terms for referring to them: A sum type is formed from a ...
4
votes
1answer
710 views

Question on the “Tutorial implementation of dependently typed lambda calculus”

I have a slight technical struggle with this marvelous tutorial. On page 5 the tutorial talks about typing rules for Simply Typed Lambdas and presents following judgement as derivable via rules on ...
1
vote
0answers
20 views

Does Quantitative Type Theory make the Prop universe obsolete?

Coq (and other type theories such as Setoid Type Theory) have a Prop universe for propositions. As far as I understand this universe is needed to be sure that the propositions can be erased. In ...
0
votes
0answers
28 views

Is Observational Equality better than intensional equality?

The Observational Equality from Epigram 2 seems to be intensional equality (like Coq and Agda have), but it also supports function extensionality. In that sense it seems that Observational Equality is ...
1
vote
0answers
22 views

Is there a most general fixpoint?

We can write inductive types in terms of a fixpoint type: ...
2
votes
1answer
61 views

Difference between assignment, binding, and substitution?

I am trying to understand the difference of assignment, binding, and substitution. I know the three things are related, but to me it's not exactly clear what word refers to what. Example, illustration,...
1
vote
1answer
51 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
39 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
24 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 ...
0
votes
2answers
60 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 ...
2
votes
1answer
48 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
39 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
68 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
72 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
42 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
32 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
249 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 ...
2
votes
2answers
63 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
39 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
39 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
48 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
32 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 ...
5
votes
2answers
582 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
50 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 ...
2
votes
2answers
54 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
144 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
24 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
89 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
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 ...

1
2 3 4 5
10