Questions tagged [dependent-types]
An overlapping feature of type theory and type systems.
14
questions
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
4
votes
1
answer
231
views
Definition of extensional and propositional equality in Martin-Lof extensional type theory
Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.[4-5]) that:
A similar situation occurs in extensional Martin-Lof type theory where propositional and definitional ...
- 621
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
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
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
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
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
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
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
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
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
3
votes
1
answer
579
views
Does types being terms imply your dependend theory is considered polymorphic?
In the introduction of the book by B.Jacobs, "Categorical Logic and Type Theory" (it's online here), he classifies type systems into three general flavours: Simply typed ones, depended typed (term ...
- 175
3
votes
0
answers
239
views
What is the runtime (time complexity) of Type Inference in Simply Typed Lambda Calculus?
I was told that the runtime of OCAML or Scala is EXPTIME - which seems really bad! However, since people use type inference (deciding the type of a term or program or expression) in practice - it must ...
- 3,000
3
votes
1
answer
305
views
Is it possible that the universe of types could be closed?
I asked a pretty vague question. I wasn't able to make it precise, but I can now. It seems to be out of the scope of the previous question, so I open another one.
In dependently-typed languages such ...
- 934