# Questions tagged [type-theory]

formal systems to specify properties of objects

345 questions
Filter by
Sorted by
Tagged with
9k views

### Dependent types vs refinement types

Could somebody explain the difference between dependent types and refinement types? As I understand it, a refinement type contains all values of a type fulfilling a predicate. Is there a feature of ...
5k views

### What makes type inference for dependent types undecidable?

I have seen it mentioned that dependent type systems are not inferable, but are checkable. I was wondering if there is a simple explanation of why that is so, and whether or not there is there a limit ...
3k views

### Intro to Martin-Löf type theory

What would be the best introduction to Per Martin-Löfs ideas about type theory? I've looked at some lectures from the Oregon PL summer school, but I'm still sort of puzzled by the following question: ...
6k views

### What can Idris not do by giving up Turing completeness?

I know that Idris has dependent types but isn't turing complete. What can it not do by giving up Turing completeness, and is this related to having dependent types? I guess this is quite a specific ...
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 ...
779 views

### What is a brief but complete explanation of a pure/dependent type system?

If something is simple, then it should be completely explainable with a few words. This can be done for the λ-calculus: The λ-calculus is a syntactical grammar (basically, a structure) with a ...
2k views

### Does there exist a Turing complete typed lambda calculus?

Do there exist any Turing complete typed lambda calculi? If so, what are a few examples?
2k views

### How are programming languages and foundations of mathematics related?

Basically I am aware of three foundations for math Set theory Type theory Category theory So in what ways are programming languages and foundations of mathematics related? EDIT The original ...
568 views

1k views

### Relation between Russellian type theory and type systems

I recently realized that there is some sort of relation between Russellian type theory and type systems, as found e.g. in Haskell. Actually, some of the notation for types in Haskell seems to have ...
711 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 ...
178 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 ...
488 views

### Inferring refinement types

At work I’ve been tasked with inferring some type information about a dynamic language. I rewrite sequences of statements into nested let expressions, like so: <...
140 views

### Can properties such as memory usage of a function be expressed in a dependently typed language?

Suppose one wants to reason about properties of code beyond things like totality and functional purity - one also cares about the memory consumption, or algorithmic complexity of a function. Can this ...
446 views

### Constraint-based Type Inference with Algebraic Data

I am working on an expression based language of ML genealogy, so it naturally needs type inference >:) Now, I am trying to extend a constraint-based solution to the problem of inferring types, based ...
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 ...
834 views

### Strict positivity

From This reference : Strict positivity The strict positivity condition rules out declarations such as ...
1k views

I am reading about dependent types theory in the Homotopy Type Theory online book. In section 1.3 of the Type Theory chapter, it introduces the notion of hierarchy of Universes: $\mathcal{U}_0 : \... 2answers 838 views ### Universal/existential quantification? I'm struggling to understand the purpose of universal and existential quantification of types. I'm playing around with writing a toy language based on the calculus of constructions. I've been reading ... 2answers 460 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 ... 1answer 229 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 ...
2k views

### Define a list using only the Hindley-Milner type system

I'm working on a small lambda calculus compiler that has a working Hindley-Milner type inference system and now also supports recursive let's (not in the linked code), which I understand should be ...
6k 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 ...