Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [type-theory]

formal systems to specify properties of objects

5
votes
1answer
76 views

Pure type systems and let-expressions

I can not find any simple and detailed source of how to add non-recursive let-expressions to pure type systems. The best I found is the Henk paper by Simon Peyton Jones, but his explanation of this ...
0
votes
1answer
56 views

How CompCert “proves” different things in its codebase

In order to understand examples of formal proofs, I am interested in how CompCert applies "proof" techniques. Specifically, I am wondering what a particular example is of something CompCert "proves" ...
0
votes
1answer
46 views

Meaning of $\mu t$ terms in dependent type theory

What is the meaning of the term $\mu t$ in the type theory formalized in this paper (section 2.1, page 2)?
2
votes
2answers
189 views

Confusion about the definition of de Bruijn terms in the TAPL book

I'm working through Types and Programming Languages right now, and I'm a little confused about the recursive definition given for nameless/de Bruijn terms (chapter 6, definition 6.1.2). Below is the ...
2
votes
1answer
46 views

What does “terms evaluated in related environments yield related values” means in the context of typing judgements?

I am reading Theorems for free! by Philip Wadler which is a paper about how to derive theorems from the type signature of a function. Parametricity is just a reformulation of Reynolds’ abstraction ...
2
votes
1answer
38 views

Restrictions needed on ADT for totality

In the paper Total Functional Programming by D.A. Turner three rules are given for a programming language to remain total: complete case analysis covariant type recursion (type constructor should not ...
3
votes
1answer
402 views

How to Efficiently Define the Natural Numbers in Type Theory

A while ago I wondered about how Proof Assistants like Coq prove $m \leq n$ and the like. It looks like they actually need to traverse the natural numbers based on the successor/predecessor ...
7
votes
1answer
490 views

Is Coq synthetic or analytic?

In CMU's HoTT course, lecture 1, which can be found here: https://scs.hosted.panopto.com/Panopto/Pages/Viewer.aspx?id=0945cc7f-48b7-4803-81af-e7193a3f461d At 33:52, Harper was giving parallel ...
1
vote
0answers
58 views

Combinatory logic equivalent to System F

Simply typed lambda calculus has a combinatory logic equivalent with the same expressive power without the need of defining names via lambda abstraction. Is there a formalism as powerful as System F ...
4
votes
2answers
967 views

Understanding the Reasoning Behind These Typing Rules

So the expression $\Gamma \ \vdash \ e:\sigma$ states that under assumptions $\Gamma$, the expression $e$ has type $\sigma$. Then we have the following rules: \begin{array}{cl}\displaystyle {\frac {x:...
3
votes
2answers
77 views

The difference between a Hoare Triple/Assertion and a Typed Function

I have been trying to wrap my head around applying Hoare Logic and am running into the question of how Hoare triples are any different from (simply) a typed function. That is, say you have a typed ...
4
votes
1answer
52 views

When do we need U(n+2) to solve a problem that can be formulated in U(n)?

I understand the need for a universe hierarchy, and that each new level brings additionnal proof-theoretic strength. In the HoTT book there are examples of proofs that need to use the next level in ...
2
votes
1answer
90 views

Assertion of Type Inference Rules/Type Checking

I have a problem in a book I am trying to accomplish. I understand the overall type of the expression is boolean and how it derives. (y * x) will be rule 4 (counting from top right). (y * x) + x when ...
3
votes
1answer
49 views

How should I describe the relationships between type expressions?

Lets say I have two type expressions: Maybe a (X) and Maybe Integer (Y), where Maybe is a ...
4
votes
3answers
105 views

Meaning of the notation Typ := TVar | (Typ → Typ)

In the paper "introduction to type theory" by Herman Geuvers, it states the following definition for the type theory of propositional logic (I've added "convention 2" just for reference): Given ...
28
votes
4answers
2k views

What exactly is the semantic difference between set and type?

EDIT: I've now asked a similar question about the difference between categories and sets. Every time I read about type theory (which admittedly is rather informal), I can't really understand how it ...
5
votes
1answer
100 views

Is there a formal difference between $f:X \to X$ and $f\in X \to X$?

We can denote by $X\to X$ the set of all functions from $X$ to $X$. Therefore, we can use the following statement to say that $f$ is a function from $X$ to $X$: $$f\in X\to X$$ But we usually state ...
7
votes
0answers
143 views

Advantages of algorithm W over algorithm J for type inference in Hindley-Milner type system

According to A modern eye on ML type inference Furthermore, for some unknown reason, W appears to have become more popular than J, even though the latter is viewed—with reason!—by Milner as ...
0
votes
1answer
39 views

How to represent a map data structure mathematically

Wondering how to represent a map object such as the following mathematically: var foo = { a: 10, b: 'bar', c: true } You could say that it was a function ...
10
votes
2answers
377 views

How to derive dependently typed eliminators?

In dependently-typed programming, there are two main ways of decomposing data and performing recursion: Dependent pattern matching: function definitions are given as multiple clauses. Unification ...
4
votes
1answer
152 views

What are some examples of types that can't be derived set theoretically?

I'm hoping for examples that aren't too abstract or useless in day-to-day programming, though not with a lot of hope, since in Bartosz Milewski's book, it is stated that generally speaking, the ...
4
votes
1answer
67 views

Agda: Which part does this type introduce universe inconsistency?

I was trying to prove following lemma, ...
0
votes
1answer
114 views

Can the foundation of computer science be implemented to include new rules of inference so that computer can do causal reasoning?

The idea I'm thinking of is about a top-down approach for AI. I would like to know if there can be a model for computers so that they can perform causal reasoning. It seems that causal relation can be ...
2
votes
0answers
36 views

How can I prove impossibility of generalizing a given higher order function from pure to monadic or applicative?

There is a great divide in Haskell between pure and monadic algorithms. While the latter are indistinguishable from their usual imperative counterparts, the former can get much more magical. What this ...
4
votes
1answer
164 views

Some points about type checking of simply typed $\lambda$-calculus?

type checking I was preparing examples of type checking in simply typed $\lambda$-calculus. I wanted to explain it to my audience in the way of implementation. And I found a bit tricky point in the ...
7
votes
2answers
106 views

Ackerman hierarchy for higher order primitive recursion in System T

Gödel defines in his System T primitive recursion over higher types. I found notes from Girard where he explains the implementation of System T on top of simply typed lambda calculus. On page 50 he ...
2
votes
2answers
79 views

Origins of the numerical notation for types in type theory

In several papers on type theory it's possible to see some sort of numerical notation for types based on the number of possible constructors for the type. For example, the unit type is usually written ...
3
votes
0answers
73 views

Semantic parsing with Grammatical Framework - is this possible?

So far I have learned about categorial grammars, type logical grammars and formal semantics of natural language, the relevant tools are Cornell Semantic Parsing Framework https://github.com/clic-lab/...
5
votes
1answer
98 views

Introduction to type theory for a beginner?

I'm interested to read about type theory, but I'm quite a beginner. I know what sets are and how to work with them, but I don't have a deep understanding of set theory. I don't really understand the ...
4
votes
1answer
64 views

How is type safety handled differently between reference and value types?

I'm trying to understand how type safety is preserved for value types and for reference types, specifically in languages with managed memory (such as C#). I understand that reference types (i.e. ...
5
votes
1answer
98 views

Is impredicative Set consistent with the excluded middle?

While studying Coq, I found a few references that impredicative Set might not work well with classical axioms, in particular the axiom of choice. I'm working on a dependent type system based on the ...
4
votes
2answers
83 views

What defines negative and non-negative type operators?

I'm working through some exercises in Robert Harper's "Practical Foundations for Programming Languages" and I'm not certain I understand what makes an occurrence of a type operator non-negative or ...
6
votes
2answers
128 views

What are the rules for positive recursive types in dependent type theory?

I've recently started independently learning type theory, using a combination of papers found online and ncatlab.org (but have not worked with category theory), and am about to start reading TAPL. I'...
0
votes
1answer
31 views

Grammar types constraint after adding a couple of types (and a statement involving them) to a “typeless” language

Foreword : by "typeless programming language", I naively mean "language in which you don't write statements like type x (=) ... to declare(define) ...
1
vote
1answer
44 views

Is implication(function) more fundamental than lets say conjunction(product) in type theory?

According to the answer at (How to define function type in AGDA) the function type is kind of a fundamental thing in Agda and needed for bootstrapping, hence end user can not define it like what they ...
2
votes
1answer
41 views

How to define function type in AGDA

The "function" type $\rightarrow$ is predefined in Agda. But how would one define it if it was not predefined? Specifically I am talking about $\rightarrow$ in: ...
2
votes
1answer
57 views

What is the type system (or class of type systems) that that ensures all your tree Branches end in Leaves?

I've come across this situation numerous times in the past few years where I have some classes like (pseudo-Java): ...
5
votes
0answers
68 views

How could one write typing rules with variables defined at call-site?

I'm trying to write typing rules for a simple language, which is basically a lambda calculus with SSA-like $\phi$-nodes, which basically exchange formal parameters for actual parameters. For ...
4
votes
2answers
94 views

When does a type generalise another type?

In languages like Haskell, with a Hindley-Milner type system, when does a type $t$ generalise a type $u$? I use the definition: $t$ generalises $u$ iff $\forall\ v: v \text{ unifies with } u \...
11
votes
2answers
163 views

Reducing products in HoTT to church/scott encodings

So I am currently going though the HoTT book with some people. I made the claim that most inductive types we will see can be reduced to types containing only dependent function types and universes by ...
17
votes
4answers
2k views

Why must a function with polymorphic type `forall t: Type, t->t` be the identity function?

I am new to programming language theory. I was watching some online lectures in which the instructor claimed that a function with polymorphic type ...
7
votes
1answer
926 views

Is there a difference between type safety and type soundness?

I've been trying to tease apart the definitions of type safety and type soundness and I'm having a heck of a time of it. I asked a professor recently and after a bit of thought he said that there ...
4
votes
1answer
93 views

Relation between Hoare Type Theory and pointers

My understanding is that in Hoare Type Theory every imperative statement has a type of the form {Pre}res:T{Post} where T is the ...
4
votes
1answer
95 views

Linear/affine lifetimes without subtyping

Are there any type systems similar to rust that don't depend on subtyping ? Can we express that one value must be consumed or dropped before another? For instance if I had an array of huge values on ...
4
votes
1answer
250 views

Why product type is a dependent SUM?

It might just be a stupid question but I simply see no obvious reason why dependent sum type is a generalized form of product type. Concretely, the sigma type $\Sigma(x:S)T$ degenerates to a product ...
7
votes
2answers
209 views

Can the formalisms of category theory replace those of type theory?

The subtleties of the correspondence between type theory and category theory are outside my ken. However, by my naive understanding of the relationship between the two historically convergent ...
6
votes
1answer
488 views

The C3 linearization algorithm for method resolution in multiple inheritance OO languages: Looking for a justification for some implementation detail

According to this description of Python's method resolution order (mro), a.k.a. C3 linearization, the algorithm can be described recursively as follows: ...
3
votes
2answers
451 views

What would “sum types with functions” look like in OOP?

It's fair to summarize classes in OOP as "product types with functions." However, couldn't there be something like "sum types with functions"? How would inheritance work with them? I'm trying to ...
2
votes
1answer
43 views

“Type” of a function template?

In C++ a simple function like int id_int(int x){return x;} has type id_int :: int->int a class template like ...
7
votes
1answer
354 views

Curry Howard correspondence to Predicate Logic?

So I'm trying to get my head round Curry-Howard. (I've tried at it several times, it's just not gelling/seems too abstract). To tackle something concrete, I'm working through the couple of Haskell ...