Questions tagged [dependent-types]
An overlapping feature of type theory and type systems.
117
questions
76
votes
4
answers
16k
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 ...
- 29.7k
50
votes
1
answer
8k
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 ...
- 695
42
votes
2
answers
8k
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 ...
- 531
27
votes
1
answer
3k
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 ...
- 29.7k
21
votes
1
answer
3k
views
Difference between Dependent type , refinement type and Hoare Logic
I know little dependent type theory. From wikipedia :
A dependent type is a type whose definition depends on a value.
And from my Type theory course i recall that a dependent type is :
Family ...
- 933
20
votes
1
answer
2k
views
if (λ x . x x) has a type, then is the type system inconsistent?
If a type system can assign a type to λ x . x x, or to the non-terminating (λx . x x) (λ x . x x), then is that system ...
- 4,117
20
votes
3
answers
2k
views
Is path induction constructive?
I'm reading through the HoTT book and I have a hard time with path induction.
When I look at the type in the section 1.12.1:
$$\text{ind}_{=_A}:\prod_{C:\prod\limits_{x,y:A}(x=_Ay)\to \mathcal{U}}
\...
- 473
18
votes
2
answers
638
views
"Minimal" intuitionistic type theory?
I'm surprised that people keep adding new types in type theories but no one seems to mention a minimal theory (or I can't find it). I thought mathaticians love minimal stuff, don't they?
If I ...
- 934
16
votes
2
answers
884
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 ...
- 473
16
votes
1
answer
5k
views
What is different between Set and Type in Coq? [closed]
AFAIU types can be a Set whose elements are programs or a proposition whose elements are Proofs. So based on this understanding:
...
- 271
12
votes
2
answers
2k
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 : \...
- 223
12
votes
2
answers
2k
views
Standard constructive definitions of integers, rationals, and reals?
Natural numbers are defined inductively as (using Coq syntax as an example)
Inductive nat: Set :=
| O: nat
| S: nat -> nat.
Is there a standard way to define ...
- 263
12
votes
2
answers
309
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 ...
- 3,790
12
votes
1
answer
429
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 ...
- 243
12
votes
2
answers
985
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 ...
- 29.7k
11
votes
1
answer
2k
views
Why does Coq include let-expressions in its core language
Coq includes let-expressions in its core language.
We can translate let-expressions to applications like this:
let x : t = v in b ~> (\(x:t). b) v
I understand ...
- 565
11
votes
1
answer
184
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 ...
10
votes
2
answers
492
views
Proving a sorting operation in type system
I want to know how far a type system in a programming language can be beneficial. For example, I know that in a dependently typed programming language, we can create a ...
- 293
10
votes
1
answer
350
views
Why are recursive types needed as primitives for proofs in dependent type systems?
I'm relatively new to type theory and dependent programming. I've been studying the calculus of constructions (CoC) and other pure type systems. I'm particularly interested in using it as a proof-...
- 711
9
votes
2
answers
552
views
What are the difference between and consequences of using type parameters and type indexes?
In type theories, like Coq's, we can define a type with parameters, like this:
...
- 602
9
votes
2
answers
261
views
Domain Theory and Polymorphism
Domain theory gives an amazing theory of computability in the presence of simple types. But when parametric polymorphism is added there doesn't seem to be a nice theory that explains whats going on ...
- 3,790
9
votes
1
answer
394
views
Relationship between inductive families and type-returning functions
Dependently typed languages such as Agda support inductive families, also called indexed datatypes, which allow type parameters to vary between constructors. This can be used to define a set of ...
- 304
9
votes
2
answers
2k
views
Is it possible to do Dependent Types in Typed Racket?
Is it possible to use Dependent Types in the existing Typed Racket implementation? (ie do they exist in it?)
Is it reasonably possible to implement a Dependent Types System using Typed Racket?
- 1,199
8
votes
1
answer
819
views
What does canonicity property mean in Type Theory?
The "Computational Component" section of the Type Theory - Wikipedia (as well as a few papers about cubical type theory and 2d type theory) talk about canonicity property.
Would you please explain ...
- 621
8
votes
1
answer
850
views
What fragment of Martin-Löf dependent type theory can be expressed using generic types in Java?
I have recently come to realize that a number of problems I had a few years ago trying to implement various mathematical theories in Java came down to the fact that the typing system in Java is not ...
- 183
7
votes
2
answers
471
views
Generating constraints to solve dependently-typed metavariables?
In dependent-types, Miller pattern unification is used to solve a decidable fragment of higher-order unification. This allows dependently-typed languages to contain metavariables or implicit arguments....
- 29.7k
7
votes
2
answers
296
views
Example of existence proof in dependent typing?
I understand that $\Pi$ types are generalizations of functions and can be interpreted similar to $\forall$ in logic. I also know that $\Sigma$ types are generalizations of tuples and can be ...
- 71
7
votes
1
answer
415
views
Is there any difference between extensible records and dependent maps
In a typed setting, records can be thought of as a map from field to type. If there is a well-typed record merge operation (which allows overlapping fields), is there any real difference between the ...
- 463
7
votes
1
answer
268
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 ...
- 209
7
votes
0
answers
147
views
Extensional constructs in minimal extensional type theory without eta equality
The extensional version of Intuitionistic Type Theory is usually formulated in a way that makes extensional concepts like functional extensionality derivable. In particular, equality reflection, ...
- 71
6
votes
1
answer
819
views
Where are C++ templates inside of the lambda cube?
C++ templates have type variables and can express lambdas, so they must have System F embedded. But is that exactly where they are located in the lambda cube? Can C++ templates produce new types or ...
- 71
6
votes
2
answers
488
views
What are the rules for positive recursive types in dependent type theory?
I've recently started independently learning type theory, using a combination of papers found online and ncatlab.org (but have not worked with category theory), and am about to start reading TAPL.
I'...
- 163
6
votes
1
answer
219
views
Difference between "sort" and "universe"
A very basic question.
As title, what is the difference between "sort" and "universe" in type theory?
Are they interchangable?
Or are there only finite number of sorts, but infinite universes?
- 934
6
votes
1
answer
90
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 = ...
- 341
6
votes
1
answer
863
views
Typing dependent pattern matching
I'm curious on how to type a dependent pattern matching in a functional language. What should the rule for typing
...
- 398
6
votes
1
answer
221
views
What is the difference between ∀ and Π in the Calculus of Constructions?
As I've learned, the Calculus of Constructions has only two binders - $\lambda$ and $\Pi$. Morte, for example, has $\forall$ as a mere alias of $\Pi$. Yet, on the paper Self Types for Dependently ...
- 4,117
6
votes
1
answer
525
views
Non-termination of types in Martin-Löf's Type:Type?
In the pre-history of dependent type theory, Per Martin Löf
introduced a calculus that is in some sense the simplest dependent
type theory and the most general form of impredicative polymorphism.
It ...
- 8,308
6
votes
1
answer
196
views
Is it possible to prevent arithmetic errors with a dependent type system?
In a functional programming language I have functions like
$$f\colon Int \times Int \times \cdots \times Int \to Int$$ which do some computation. However for certain arguments $(x_0, \dots, x_n)$ the ...
- 361
6
votes
1
answer
1k
views
Is it possible to implement dependent types by any object oriented language supporting inheritance and classes?
When I was reading Agda tutorial, I noticed resemblance between dependent type declarations and class definitions which I've been primarily used to work with. I'm not totally sure how much sense this ...
- 385
5
votes
2
answers
633
views
Decidability of dependent typing on primitive recursive languages
With a dependent type system in a normal functional language type checking may never halt. This is partially because dependent typing removes the isolation between types, and code. My question is this:...
- 459
5
votes
1
answer
236
views
Relation between Hoare Type Theory and pointers
My understanding is that in Hoare Type Theory every imperative statement has a type of the form {Pre}res:T{Post} where T is the ...
- 53
5
votes
1
answer
204
views
Dependent type system with different computation model
There exist various Turing-equivalent models of computation, such as lambda calculus, Turing machines, or register machines.
It seems that dependent type systems (like Coq, Agda, Idris, homotopy type ...
- 290
5
votes
1
answer
490
views
Dependent Type Theory Implementation of a Graph
In Haskell you find graphs defined like this:
data Graph a = GNode a (Graph a)
Or this:
...
- 2,163
5
votes
1
answer
573
views
Resources for implementing dependent type theory
I want to implement Martin Löf's intuitionistic type theory in a functional language such as Haskell, preferably also implementing a lexer/parser for the language. How should I start approaching it? ...
- 347
5
votes
1
answer
400
views
Definitional equality of two propositions about propositional equality
Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.3) that:
It is important that definition equality is pervasive so if M and N are definitionally equal then P(M) is ...
- 621
5
votes
1
answer
98
views
What untyped term inhabits induction on natural numbers in CoC?
Induction on Church-encoded natural numbers (which I will call indNat) can not be defined within the Calculus of Constructions.
If we assumed ...
- 565
5
votes
2
answers
126
views
Identity types and universes
Let us consider Martin-Löf type theory with a cumulative hierarchy of universes
$$
\mathcal{U}_0\colon\mathcal{U}_1\colon\ldots
$$
If $A, B\colon \mathcal{U}_i$, we can form an identity type $A=_{\...
- 153
5
votes
1
answer
104
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 ...
- 3,790
5
votes
0
answers
61
views
Rules for consistency with mutual inductive families?
I'm trying to use a proof assistant to define a type and a relation that are mutually dependent on each other:
...
- 29.7k
5
votes
0
answers
64
views
Can we simulate any dependent datatype with `Eq`?
Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
- 29.7k