The type-theory tag has no wiki summary.
2
votes
0answers
44 views
Forms of types in the calculus of constructions
In the usual presentations of the calculus of constructions (CC) with two kinds Prop and Type such that Prop:Type and impredicative on Prop, it is easy to show the following result:
every closed term ...
3
votes
1answer
249 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?
10
votes
2answers
235 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. ...
3
votes
2answers
197 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:
class (Eq a) => Ord a where
...
5
votes
0answers
191 views
Can boolean algebra be expressed in simply typed lambda caclulus?
Boolean algebra can be expressed in untyped lambda calculus in (for example) this way.
true = \t. \f. t;
false = \t. \f. t;
not = \x. x false true;
and = \x. \y. x y false;
or = \x. \y. x ...
13
votes
6answers
502 views
What is the difference between propositions and judgments?
I get confused by the subtle difference between propositions and judgments when exposed to intuitionistic type theory. Can any one explain to me what is the point to distinguish them and what ...
5
votes
3answers
318 views
Type system based on naive set theory
As I understand, in computer science data types are not based on set theory because of things like Russell's paradox, but as in real world programming languages we can't express such complex data ...
11
votes
2answers
313 views
Type classes vs object interfaces?
I don't think I understand type classes. I'd read somewhere that thinking of them as "interfaces" (from OO) that a type implements is wrong and misleading. The problem is, I'm having a problem seeing ...
5
votes
6answers
671 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
112 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 : ...
9
votes
3answers
197 views
Modeling objects (OOP) in dependent type theory
I am interested in modeling objects, from object oriented programming, in dependent type theory. As a possible application, I would like to have a model where I can describe different features of ...
6
votes
3answers
352 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, ...
7
votes
2answers
168 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 ...
8
votes
2answers
596 views
Type inference for imperative statements other than assignment
In my search for research papers about type systems for imperative languages, I only find solutions for a language with mutable references but without genuine imperative control structures such as ...
11
votes
1answer
178 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), ...
12
votes
3answers
242 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 ...
14
votes
2answers
384 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 ...
12
votes
0answers
183 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 ...
6
votes
0answers
184 views
What's the relation and difference between Calculus of Inductive Constructions and Intuitionistic Type Theory?
As stated in the title, I wonder any relation and difference between CIC and ITT. Could someone explain or point to me some literature that compares these two systems? Thanks.
5
votes
1answer
190 views
What is the role of the Bicolored Calculus of Constructions?
So, I'm reading a bit about elaboration, particularly, algorithms based on the Bicolored Calculus of Construction, and I'm a bit confused. I don't understand what exactly the purpose of the $CC^{bi}$ ...
12
votes
2answers
271 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:
...
15
votes
1answer
425 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 ...
6
votes
1answer
214 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 ...
5
votes
2answers
190 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' ...
8
votes
2answers
175 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:
Inductive Nat :=
| O : Nat
| S : Nat -> Nat.
or
Inductive Nat ...
14
votes
2answers
356 views
Do dependent types give you everything subtyping does?
Types and Programming Languages focuses quite a bit on subtyping, but as far as I can tell, subtyping doesn't seem especially fundamental. Does subtyping give you anything more than dependent types ...
24
votes
1answer
467 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 ...
15
votes
5answers
722 views
What is the most intuitive dependent type theory I could learn?
I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles ...
10
votes
3answers
358 views
What is the role of predicativity in inductive definitions in type theory?
We often want to define an object $A \in U$ according to some inference rules. Those rules denote a generating function $F$ which, when it is monotonic, yields a least fixed point $\mu F$. We take $A ...
11
votes
2answers
221 views
References to programming languages based on conditional logics
Conditional logics are logics which augment traditional logical implication with modal operators corresponding to other notions of condition (for example, the causal conditional $A\; ...
15
votes
1answer
392 views
Are types propositions? (What are types exactly?)
I've been reading a lot on type systems and such and I understand roughly why they were introduced (in order to resolve Russel's paradox). I also understand roughly their practical relevance in ...
15
votes
3answers
395 views
How would I go about learning the underlying theory of the Coq proof assistant?
I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
8
votes
3answers
356 views
Classification of Typed/Untyped Lambda Calculi
Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi?
I'm particularly ...
18
votes
2answers
393 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 ...
17
votes
4answers
434 views
Relationship between contracts and dependent typing
I've been reading some articles on dependent types and programming contracts. From the majority of what I've read, it seems that contracts are dynamically checked constraints and dependent types are ...
9
votes
1answer
432 views
Prove proof irrelevance in Coq?
Is there a way to prove the following theorem in Coq?
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.
EDIT: An attempt to give a brief explanation for "what proof irrelevance ...
10
votes
1answer
359 views
Data structures in programming language with linear types
Assume we are dealing with a programming language that has support for linear types (terms of linear type can be used at most once, so to say). This allows for treating some computational effects ...
1
vote
0answers
205 views
Well Defined Ordering Relations in Object Oriented Type Systems [closed]
In any Object-Oriented type system the type relation of two objects A and B can be characterized in exactly one of the following ways:
A has the same type as B
A is a subtype of B
B is a subtype of ...
10
votes
2answers
199 views
Are there semi-decision procedures for this theory?
I have the following typed theory
|- 1_X : X -> X
f : A -> B, g : B -> C |- compose(g,f) : A -> C
F, f : A -> B |- apply(F,f) : F(A) -> F(B)
with equations for all terms:
f : A ...
13
votes
2answers
668 views
Implicit vs explicit subtyping
This page asserts that
many languages do not use implicit subtyping (structural equivalence), prefering explicit/declared subtyping (declaration equivalence)
I've mostly used programming ...
25
votes
6answers
1k 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, ...
6
votes
2answers
343 views
An example of a totally computable function that is not definable in system T?
Could you give me an example of a totally computable function of type N × N → N that is not definable in System T? Thanks.
11
votes
2answers
260 views
What happens if we try to extract a witness but it actually does not exist from a term of existential type?
Given a term t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y)) in Martin-Lof's type theory, what's the value of w(t(0)), where w is the operator that extracts the witness of a term of existential type?
20
votes
2answers
580 views
Context Sensitive Grammars and Types
1) What, if any, is the relationship between static typing and formal grammars?
2) In particular, would it be possible for a linear bounded automaton to check whether, say, a C++ or SML program was ...
5
votes
1answer
107 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 ...
3
votes
2answers
221 views
Type a variable-argument function?
Is it possible to type a variable-argument function?
EDIT: like those defined in Scheme.
8
votes
1answer
207 views
In System F à la Church, can we automatize type inference for the for-all elimination?
The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.
Now, suppose ...
9
votes
2answers
287 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
0answers
190 views
Type inference with subtype constraints and polymorphism using Trifonov and Smith's constraint maps
Trifonov and Smith's Subtyping Constrained Types (1996) introduces constraint maps to represent consistent closed constraint sets (such maps providing sets of lower and upper bounds to each variable ...
