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
2answers
283 views

What terms type systems exclude?

I understand type systems like the simply typed lambda calculus, system F and the calculus of constructions include a different subset of all lambda terms. But what, precisely, are the terms each of ...
9
votes
5answers
1k views

Daily Applications of Type Theory

I want to understand type theory but I have to know first how I can apply it. Could there be more non-obvious applications of type theory aside from in type systems in programming? Could there be ...
6
votes
2answers
575 views

In the Curry-Howard isomorphism as applied to Hindley-Milner types, what proposition corresponds to a -> [a]?

(Using Haskell syntax, since the question is inspired by Haskell, but it applies to general Hindley-Milner polymorphic type systems, such as SML or Elm). If I have a type signature ...
7
votes
2answers
243 views

What is the Curry-Howard analogue for linear logics?

As defined by Wikipedia, (The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the ...
2
votes
1answer
44 views

Can big-step semantics express evaluation order?

Can you express evaluation order using big-step semantics? For example, in a simple language consisting of only if t then t else t and ...
6
votes
2answers
277 views

Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?

Chapter 7 of The Haskell Road to Logic Math and Programming discusses induction and recursion. Haskell is strongly typed and we can define the natural numbers ...
14
votes
3answers
3k views

Which research languages have a stronger typesystem than Haskell and why?

Here I read that: Haskell definitely does not have the most advanced type system (not even close if you count research languages) but out of all languages that are actually used in production ...
5
votes
1answer
74 views

How to prove $0\neq1$ using the J rule?

Suppose I have a simple dependent type theory with bottom, unit, sums, dependent pairs, dependent functions, natural numbers and homogeneous identity with J-elimination. Is there a way to prove $(0 = ...
1
vote
1answer
68 views

What is the rationale behind implicitly widening integer types in numeric operations?

Languages such as Java and C specify implicit widening of integer types for numeric operators, especially arithmetic operators, to a minimum of 32 bits. What is the rationale behind doing this? My ...
7
votes
0answers
34 views

Is there any type system which can assign a type to any halting lambda calculus term? [duplicate]

Some lambda terms, such as the church number 3: (f x -> (f (f (f x)))), are easily typeable on the simply typed lambda calculus. Others, such as ...
19
votes
1answer
910 views

What are the strongest known type systems for which inference is decidable?

It's well known that Hindley-Milner type inference (the simply-typed $\lambda$-calculus with polymorphism) has decidable type inference: you can reconstruct principle types for any programs without ...
3
votes
1answer
154 views

Top-down typing strategy - is there a name for this?

In most statically typed languages, each expression has an intrinsic type. E.g. in Java, 3 is an int, 3.0 is a double, ...
3
votes
3answers
135 views

Isn't Domain of a variable nothing but a constraint?

In Constraint programming we have Variables and their Domains and then all the constraints, but if you at the concept of a domain of a variable it is nothing but another type of constraint, you are ...
6
votes
0answers
373 views

Is the strictly positive condition in Coq and Agda an aproximation?

Languages like Coq and Agda enforce that their inductive types occur "strictly positively" in their definitions. That is, the type should not occur to the left of an arrow of an argument of a ...
2
votes
1answer
34 views

Rearranging function in 'Theorems for free'

I'm reading Wadler's 'Theorems for free'. In section 3.5 he states that $m_{AA}(I_A)$ is a rearranging (i. e. injective) function. $I_A$ is the identity function on the type A. $$m : \forall X.\forall ...
10
votes
1answer
5k views

Meaning of “positive position” and “negative position” in type theory?

What does "in positive position" and "in negative position" mean in the context of type theory? The only thing I understood from Bob Harper's blog post on the topic is that there is a connection ...
4
votes
1answer
68 views

How to understand equivalence of indexes of a family of types that are not definitionally equal

So I've been reading things about HoTT and trying to get solid on the foundations before getting too much further into the book. I am confused by a certain point; maybe I just haven't read far enough ...
2
votes
2answers
166 views

Why have a numeric type hierarchy?

The more I think about it, the stranger the concept of having a number type, which is a super-type of integers, rationals and reals seems to be. One thing that ...
0
votes
1answer
74 views

Can polymorphism be simulated by lazy type operators?

In the definition of lambda cubes, type polymorphism is distinguished from type operators/constructors. I have the nagging feeling that type polymorphism can be constructed through type operators ...
6
votes
1answer
355 views

type theory notation troubles

I'm working through "Types and Programming Languages" by Benjamin Pierce and I don't quite understand the notation. Particularly on Page 106, (chapter 9 Simply Typed Lambda-Calculus) there is a lemma (...
6
votes
0answers
338 views

Main differences between intuitionistic type theory and calculus of constructions (CoC)

Quoting Wikipedia "Many systems of type theory, such as the simply-typed lambda calculus, intuitionistic type theory, and the calculus of constructions, are also programming languages." I'm a Coq user ...
13
votes
0answers
171 views

Why do we have to forbid non-conforming lower and upper type bounds?

(it's a repost of my unanswered question from scala-user@googlegroups.com about Scala) In the Scala Language Specification, §4.4 Type Parameters, there is a requirement: The most general form of a ...
4
votes
2answers
168 views

Algorithmic type checking for Calculus of Inductive Constructions

So from reading "Advanced Topics in Types and Programming Languages" (ATTPL) I know of the calculus of constructions (CoC). It also presents the "algorithmic" type checking rules. Reading Coq's ...
5
votes
2answers
574 views

Application of set theory subjects as ordinals, forcing, generic filters in software engineering

I am going to teach a course in set theory for software engineering students. I am going to talk in this course about: ordinal numbers, partial orders, well ordering, generic filters and maybe some ...
1
vote
0answers
22 views

Importance of indexes in Type(i) in calculus of inductive constructions [duplicate]

So I am reading about the calculus of inductive constructions. And I see here and here that there hidden indexes that the user does not know about in the $Type$ sort. It says that they are ...
5
votes
2answers
440 views

Given the “programs as proofs” isomorphism, how do we know that the program isn't lying?

I've been studying constructive type theory (CTT) and one of the things that I'm not clear on is the proof part: Proving the correctness of a program in a form of a proof that's nothing but the ...
12
votes
2answers
301 views

What do we gain by having “dependent types”?

I thought I understood dependent typing (DT) properly, but the answer to this question: https://cstheory.stackexchange.com/questions/30651/why-was-there-a-need-for-martin-l%C3%B6f-to-create-...
3
votes
0answers
660 views

Row polymorphism, union and intersection types

It seems that row polymorphism with union types can be used in dynamic languages to approximate overloading, e.g. given the following python function: ...
2
votes
0answers
94 views

Is there a formalization of automatic-splicing data structures?

I'm wondering if there is some formalization, type theoretical analysis, or similar for data structures that automatically "splice" in an associative way. Barring a perfect citation, I'd be interested ...
2
votes
0answers
114 views

Test cases for subtyping with dependent types

I implemented a simple type system inside Agda and I'm trying to understand, how expressive it is. The system consists from a predicative hierarchy of universes in the style of Russell, natural ...
4
votes
2answers
85 views

Definition of a size of type

In B. Pierce's book "Types and Programming Languages", he talks about the size of types (see pictures below). I searched the book for a definition but could not find one. I only found a definition ...
2
votes
0answers
56 views

Understanding a paper on polynomial recursion in all finite types

So I wasn't sure weather or not this counted as "research level" or not but I figured it wasn't so I decided to post it here. There is a paper by S. Bellantoni et al. called "Higher Type Recursion, ...
1
vote
1answer
117 views

Pierce's Types and Programming Languages : circular definition of terms?

In Pierce's book, on page 26-27 it is given a definition of terms for a simple language using inference rules. In the picture below it is marked by red highlighting the problematic part. What is ...
12
votes
1answer
610 views

Why aren't we researching more towards compile time guarantees?

I love all that is compile time and I love the idea that once you compile a program a lot of guarantees are made about it's execution. Generally speaking a static type system (Haskell, C++, ...) seems ...
2
votes
2answers
147 views

Understanding constraint formula concept in Java

JLS defined a concept called "constraint formula". There is a formal definition: Constraint formulas are assertions of compatibility or subtyping that may involve inference variables. The ...
15
votes
2answers
744 views

Does the Y combinator contradict the Curry-Howard correspondence?

The Y combinator has the type $(a \rightarrow a) \rightarrow a$. By the Curry-Howard Correspondence, because the type $(a \rightarrow a) \rightarrow a$ is inhabited, it must correspond to a true ...
3
votes
1answer
137 views

How can finite sets be represented as a type?

Manually self-migrated from stack overflow. A set of objects of a type T is often represented using its indicator function (set T = ...
8
votes
2answers
625 views

Which fixpoint is Haskell list type?

Let's say that lists are defined as List a = Nil | Cons a (List a) Then, in Haskell is List x the greatest or least fixpoint? ...
1
vote
1answer
152 views

Weakening and Contraction

Wikipedia says that weakening is a structural rule where the hypotheses or conclusion of a sequent may be extended with additional members and that contraction is a rule where two equal (or unifiable) ...
7
votes
1answer
185 views

Can coq express its own metatheory?

I'm learning about language metatheory and type systems, and am using coq to formalize my study. One of the things I'd like to do is examine type systems that include dependent types, which I ...
6
votes
2answers
669 views

What is the connection between data structures and data types?

I have read some books and wikipedia, which seem to give not completely consistent definitions and notations. I try to understand the concepts, regardless of what they are called. Here are what I have ...
1
vote
1answer
77 views

Does modern type theory include specifications and implementations?

Good programming practice distinguishes between specification (at the API level) and implementation. I would have thought that this same distinction would be found in type theory. Perhaps I just don't ...
6
votes
0answers
89 views

Bounded existential polymorphism

In his "Types and Programming Languages", Pierce, at the very end, presents the most powerful system in the book: $F^{\omega}_{<:}$. He, however, does not explain how bounded existential ...
10
votes
1answer
211 views

What is $Prop$ in the calculus of constructions?

I'm looking at the Calculus of Constructions and its place in the Lambda Cube. If I understand correctly, each axis of the cube can be thought of as adding another operation involving types to the ...
2
votes
1answer
199 views

Video lectures on type systems

For my job, I need to pick up a working understanding of the implementation of type systems (in particular, how to write typing rules based on a design document). I've been given a copy of Types and ...
11
votes
1answer
360 views

Can I have a “dependent coproduct type”?

I'm reading through the HoTT book and I have a (probably very naive) question about the stuff in the chapter one. The chapter introduces the function type $$ f:A\to B $$ and then generalizes it by ...
2
votes
0answers
129 views

Are there models of type theory that allow the real numbers to be a type?

Do there exist models of type theory that allow types to contain an uncountable number of inhabitants? Traditionally type theory seems to be swirled in with computable programs as constructive proofs ...
5
votes
1answer
114 views

Unrolling multi-variable mu (μ) expressions in type theory

Unrolling an iso-recursive μ-type expression such as, say, one isomorphic to natural numbers: μα.1+α using ...
4
votes
1answer
438 views

Why are dependently typed languages such as Agda used for proofs, if supercompilers for simpler typed languages can do the same?

Proof assistants such as Agda can be used to assert properties about programs, such as "the double of a number is even". Interestingly, supercompilers can be used for the same purpose, creating ...
6
votes
2answers
102 views

Type of a return satement

I'm creating a experimental toy language for my own education purposes (an impure typed Lisp based on Clojure - https://github.com/mikera/kiss) I think I understand the concept of each expression in ...