Questions tagged [type-theory]

formal systems to specify properties of objects

410 questions
Filter by
Sorted by
Tagged with
10k 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 ...
4k 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 ...
3k 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 ...
832 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 ...
614 views

2k views

Why will the Hindley-Milner algorithm never yield a type like t1 -> t2?

I'm reading about the Hindley-Milner typing algorithm while writing an implementation, and see that, as long as every variable is bound, you'll always get either atomic types or types where the ...
344 views

Is the derivative of a graph related to adjacency lists?

Some of Conor McBride's works, Diff, Dissect, relate the derivative of data types to their "type of one-hole contexts". That is, if you take the derivative of the type you are left with a data type ...
350 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-...
555 views

Reference request: Category theory as it applies to type systems

I keep hearing about how one must learn category theory to truly understand programming language theory. So far, I've learned a good deal of PL without ever stepping foot into the realm of categories. ...
189 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 ...
2k views

What does the leading turnstile operator mean?

I know that different authors use different notation to represent programming language semantics. As a matter of fact Guy Steele addresses this problem in an interesting video. I'd like to know if ...
1k views

Is there any use case for the bottom type as a function parameter type?

If a function has return type of ⊥ (bottom type), that means it never returns. It can for example exit or throw, both fairly ordinary situations. Presumably if a function had a parameter of type ⊥ it ...
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 ...
774 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 ...
238 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 ...
187 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 ...
1k views

What is induction-induction?

What is induction-induction? The resources I found are: the HoTT book, at the end of chapter 5.7. nLab's article a paper called Inductive-inductive definitions this blog post also mentions inductive-...
518 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: <...
145 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 ...
458 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 ...
2k 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 ...
1k views

Strict positivity

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

Universes in dependent type theory

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 : \...
892 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 ...
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 ...
503 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 ...