# Questions tagged [type-theory]

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

247 questions
3k views

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) ...
336 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: ...
886 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. ...
9k 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 ...
1k 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 ...
2k views

### Type classes vs object interfaces

I don't think I understand type classes. I'd read somewhere that thinking of type classes as "interfaces" (from OO) that a type implements is wrong and misleading. The problem is, I'm having a problem ...
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 ...
251 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$...
725 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 ...
517 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, ...
315 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 ...
2k 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 ...
364 views

285 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: ...
1k 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 do?...
866 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 ...
5k 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 ...
1k views

1k 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 ...
3k 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 ...
2k 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 ...
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 ...
2k 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 ...
2k 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 ...
2k 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 (...
447 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 A ...
333 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) ...
2k 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 ...
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, ...
725 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.
439 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 ...
1k 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 ...
165 views