Questions tagged [type-theory]

Type structure is a syntactic discipline for enforcing levels of abstraction.

Filter by
Sorted by
Tagged with
6
votes
2answers
420 views

“Correctness” of type theory

How to "proof" that type theory is correct? Or at least explain that it's meaningful in some sense. In what extent is this a mathematical question and in what is a philosophical one? When type ...
9
votes
1answer
243 views

Example of where violation of strict positivity condition in inductive types leads to inconsistency

Most dependent typed systems have a strict positivity conditions for inductive types. Does anybody know an example where violation of the condition leads to inconsistency in the system?
4
votes
2answers
147 views

Well-formedness condition for inductive types

I work on implementing a simple dependently typed language. I want to implement inductive types there. However, I want them to be well formed. From what I've seen in Coq not all types are acceptable. ...
10
votes
1answer
640 views

Algorithm to determine function equality on the simply typed lambda calculus?

We know that beta-equality of simply typed lambda-terms is decidable. Given M,N:σ→τ, is it decidable whether for all X:σ, MX $≃_β$ NX?
12
votes
1answer
316 views

Algebraically Compact Categories

I read Freyd's paper "Algebraically Complete Categories" in the famous Como90 and I have two questions about the notion of algebraic compactness he defined in that paper. (If you are not familiar with ...
22
votes
1answer
890 views

What are the practical issues with intersection and union types?

I'm designing a simple statically typed functional programming language as a learning experience. It appears that the type system I have implemented so far could (with a little extra work) ...
5
votes
1answer
1k views

In what sense are Scala's Try[T] and Future[T] dual?

In a recent course based on Scala I found a hint that the Scala types Try[T] and Future[T] are dual. This was explained only ...
13
votes
3answers
1k views

How can relational parametricity be motivated?

Is there some natural way to understand the essence of relational semantics for parametric polymorphism? I have just started reading about the notion of relational parametricity, a la John Reynolds' ...
10
votes
2answers
678 views

Formalizing the theory of finite sets in type theory

Most proof assistants have a formalization of the concept of "finite set". These formalizations, however, differ wildly (although one hopes that they are all essentially equivalent!). What I don't ...
24
votes
2answers
2k views

Why do Agda and Coq disagree on strict positivity?

I've stumbled across a confusing disagreement between Agda and Coq that is not obviously related to the most well known distinctions between their type theories (e.g., (im)predicativity, induction-...
6
votes
1answer
191 views

Typing relations terminology – how do I read typing relations?

I am currently trying to read up on type theory and have some quick questions on terminology. In the following rule, $$ \frac{x:T_1 \vdash t_2 : T_2}{\vdash \lambda x:T_1.t_2:T_1\to T_2} $$ How ...
11
votes
2answers
2k views

Difference between Types and Sorts

This may be a very simple question. But what is the difference between types and sorts? My current understanding is that you have a type theory with type rules that give a notion of a well-typed ...
9
votes
2answers
853 views

Certified compiler and optimizations in Coq/Agda

I am interested in verified compilers formalized in Martin-Löf type theory, i.e. Coq/Agda. At the moment I’ve written a small toy example. Therewith I can prove that my optimizations are correct. For ...
5
votes
1answer
166 views

Nested automatization of type inference of forall elimination

Following a previous question about how to automatize the type inference in a forall elimination of an application, now suppose we want to do the same but for a nested forall, say $(\Lambda X_1.\...
17
votes
1answer
534 views

What is the categorical semantics of subtyping?

Starting from Curry-Howard-Lambek, there has been a nice trinity of type theories, logics, and categories. I'm curious what categorical semantics you get when you add (coercive) subtyping to a type ...
3
votes
1answer
186 views

Decidability in Extensional Type Theory

What are the ways in which one can add a decidable equivalence relation in a type system with undecidable type checking/extensional equality?
7
votes
1answer
736 views

Constraint types (IBM/X10) compared to dependent types

Constraint types have been proposed by IBM in their X10 programming language (it's a commercial programming language, not open source software). Nystrom, Nathaniel, et al. "Constrained types for ...
18
votes
3answers
865 views

funsplit and polarity of Pi-types

In a recent thread on the Agda mailing list, the question of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark. My understanding is that $\eta$ laws come with negative ...
27
votes
2answers
4k views

What is the logarithm or root operation in type-space?

I was recently reading The Two Dualities of Computation: Negative and Fractional Types. The paper expands on sum-types and product-types, giving semantics to the types ...
44
votes
3answers
3k views

How do 'tactics' work in proof assistants?

Question: How do 'tactics' work in proof assistants? They seem to be ways of specifying how to rewrite a term into an equivalent term (for some definition of 'equivalent'). Presumably there are formal ...
0
votes
0answers
83 views

Semantics of a programming language [duplicate]

A newbie question, if I may... Could you be so kind and explain to me in plain english meaning of 'denotational semantics' and 'operational semantics'? I'm familiar with the definitions and have read ...
4
votes
0answers
189 views

Type-and-effect systems, stochasticism and effect squelching: how about quicksort?

There's a feature of Haskell's type system which bugs me: you can't implement a randomized sorting algorithm without the use of randomness spilling out into all of its callers. That seems undesirable....
28
votes
6answers
2k views

Why naturals instead of integers?

I'm interested in why natural numbers are so beloved by the authors of books on programming languages theory and type theory (e.g. J. Mitchell, Foundations for programming languages and B. Pierce, ...
5
votes
0answers
256 views

Commonalities and differences between canonical structures and the implicit calculus

There is a paper on The Implicit Calculus as a generalization of type classes. Coq's canonical structures are also a generalization of type classes. The paper does not mention canonical structures ...
12
votes
3answers
690 views

How is duality of types defined?

In Wadler's Recursive Types for Free! [1], he demonstrated two types, $\forall X . (F(X) \rightarrow X) \rightarrow X$ and $\exists X . (X \rightarrow F(X)) \times X$, and claimed they are dual. In ...
11
votes
3answers
724 views

“Guarded” negative occurrences in definition of inductive types, always bad?

I know how some negative occurrences can definitively be bad: ...
9
votes
1answer
416 views

A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?

Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a ...
9
votes
1answer
795 views

Will Martin-Löf Type Theory lead to a greater ability to write provably correct code?

This post refers to the Curry-Howard isomorphism and the Martin-Löf Type Theory. The post makes the claim of a future 'unification' between the the describing language of math, and the operation ...
0
votes
1answer
131 views

How to generalize a map of type for many operators?

I am formalizing the type system for a small language, and thus writing inference rules. Taking unary - operator for example, its entry may be a number as well as ...
21
votes
2answers
3k views

What's the difference between ADTs, GADTs, and inductive types?

Might anyone be able to explain the difference between: Algebraic Datatypes (which I am fairly familiar with) Generalized Algebraic Datatypes (what makes them generalized?) Inductive Types (e.g. Coq) ...
15
votes
2answers
383 views

Proof theory of biproducts?

A category has biproducts when the same objects are both the products and coproducts. Has anyone investigated the proof theory of categories with biproducts? Perhaps the best-known example is the ...
9
votes
2answers
214 views

Closure ordinals for inductive types with function spaces

Functors built from finite products and sums have closure ordinal $\omega$, detailed nicely in this manuscript by Francois Metayer. i.e. we can reach the inductive type $nat := \mu X. 1 + X$ by ...
28
votes
1answer
875 views

Inductive types for large countable ordinal notations.

I'm looking to build notations for large countable ordinals in a "natural way". By "natural way" I mean that given an inductive data type X, that equality should be the usual recursive equality (the ...
8
votes
1answer
317 views

Reading list on rewriting systems?

I am new to studying rewriting systems as a first year PhD student. I would like to propose a special topics course on rewriting theory, and I want to make sure I don't leave any of the original ...
5
votes
2answers
613 views

Do Higher-Order Functions provide more power to Functional Programming?

My original question was: Is Kappa calculus less powerful than Lambda calculus? Does the lack of Higher-Order functions on a programming language excludes some programs that could only be written in ...
15
votes
1answer
3k views

How does inheritance differ from subtyping?

In programming language perspective, what is mean by subtyping? I heard that "Inheritance is not Subtyping". Then what are the differences between inheritance and subtyping?
3
votes
2answers
337 views

Confusing (to me) statement from “Type Classes in Haskell”

I'm reading up on type classes, and started looking at the paper Type Classes in Haskell. In Section 2.2 - Superclasses, the authors use the following example: ...
12
votes
6answers
2k views

Functions that typed lambda calculus cannot compute

I just want to know some examples of the functions that can be computed by the untyped lambda calculus but not by typed lambda calculi. As I am a beginner, some reiteration of background information ...
7
votes
1answer
259 views

How to define eta-equivalence for F-omega types?

There are (at least) two styles for defining a (declarative) equivalence judgement for a typed lambda calculus: via a plain relation $t_1 = t_2$, via an indexed relation $\Gamma \vdash t_1 = t_2 : T$...
6
votes
3answers
593 views

Boolean as subtype of integer

In languages oriented towards systems programming, digital logic and hardware design, it's common to treat boolean as a subtype of integer. In languages oriented towards mathematics and type theory, ...
9
votes
2answers
322 views

Research on call-site based type inference?

I'm trying to learn more about whole-program type checking and type inferencing systems that use information from function call sites to compute type information (in addition to the standard approach ...
12
votes
1answer
377 views

Barendregt's proof of subject reduction for $\lambda2$

I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of Lambda calculi with types). The last step of the proof (page 60), says: "and hence by Lemma 4.1.19(1), $\quad\Gamma,x:\rho\...
15
votes
3answers
890 views

Can we prove weak normalization for System F by induction on a transfinite ordinal

Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
9
votes
2answers
286 views

Does the order of declarations in an inductive type matter?

I was wondering if the order of declarations of an inductive type can matter. For example in Coq you can define Nat either by: ...
23
votes
2answers
1k views

Is there an expressiveness hierarchy for type systems?

Inspired by the extensive hierarchies present in complexity theory, I wondered if such hierarchies were also present for type systems. However, the two examples I've found so far are both more like ...
13
votes
2answers
436 views

What are the equational laws for zero types?

Disclaimer: while I care about type theory, I don't consider myself an expert on type theory. In the simply typed lambda calculus, the zero type has no constructors and a unique eliminator: $$\frac{\...
7
votes
1answer
324 views

Implications of the rule of cumulativity in the Calculus of Constructions

Please help me understand some type theory research. As suggested in "Type Checking with Universes" by Robert Harper and Robert Pollack, we can add the following rule to our otherwise standard COC or ...
16
votes
1answer
649 views

Seeking Scott's original LCF paper

Is the following manuscript publically available? Dana Scott, 1969, A theory of computable functions of higher type. Unpublished seminar notes, 7 pages, University of Oxford. There is a discussion ...
11
votes
2answers
431 views

Does the System F with pairs have the strong normalisation and subject reduction properties?

It is easy to look in a lot of textbooks the proofs of subject reduction and strong normalisation for System F, also, sometimes there are definitions of System F with pairs, where (t,r) is a term, not ...
6
votes
2answers
422 views

With equirecursive types are there downsides to making all types potentially recursive?

By this I mean to ask, is it a bad idea to have all type constructor term expressions abstracted with $\mu$ just in case they need to be recursive? For example, $Bool : Type;$ $Bool = (\mu Bool' ...