Questions tagged [dependent-types]

An overlapping feature of type theory and type systems.

Filter by
Sorted by
Tagged with
45
votes
1answer
6k 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 ...
4
votes
1answer
327 views

Can we add dependent type into an existing imperative programming language?

As we know, dependent type allows programmers to write bugless programs. But as I know there's only very few languages support dependent type, like Haskell with extensions, Idris, Agda, F*, etc. ...
6
votes
2answers
269 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'...
1
vote
1answer
63 views

Is implication(function) more fundamental than lets say conjunction(product) in type theory?

According to the answer at (How to define function type in AGDA) the function type is kind of a fundamental thing in Agda and needed for bootstrapping, hence end user can not define it like what they ...
11
votes
2answers
232 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 ...
5
votes
1answer
156 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 ...
14
votes
1answer
3k 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: ...
8
votes
0answers
140 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, ...
3
votes
1answer
162 views

Partial type inference for dependent types

I'm looking for resources on (partial) type inference for dependent types. For example there could be a type inference scheme that fails if the term doesn't have a principal type, or a scheme that ...
8
votes
2answers
209 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 ...
8
votes
1answer
742 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 ...
4
votes
2answers
238 views

What's the difference between the rank and the degree of a type function?

1 Context Near pg. 184 of Lambda Calculus and Combinators, the author is discussing the theory of dependent types. In particular, we are extending the lambda calculus to look at terms of form $$ \Pi ...
18
votes
2answers
504 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 ...
10
votes
1answer
291 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-...
2
votes
0answers
105 views

Dependent types as regular expressions

Would be possible to encode dependent types as regular expressions? if so, ¿is there some work about? It's common to represent restrictions for elements in a traversable data structure with them, ...
11
votes
1answer
174 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 ...
3
votes
2answers
373 views

About the Identity function in Agda

I've defined the identity function in Agda as follows: idd : (∀ {ℓ} {A: Set ℓ}) → A → A idd a = a I want to ask you if the ...
20
votes
1answer
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 ...
10
votes
2answers
383 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 ...
7
votes
1answer
364 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 ...
6
votes
1answer
184 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 ...
4
votes
1answer
1k views

Examples of Dependent Types

I'm gathering examples from everything that I've read about Dependent Type Theory mainly from Dependent types at Work paper. This is my list so far of some dependent types (with abbreviations of ...
0
votes
1answer
113 views

Indexing a dependent type on a value?

If i'm recalling from Robert Harper's lectures Homotopy type theory A dependent type is a family of type index by a type. If we allow index to be just a value can we gain something instead of allowing ...
1
vote
0answers
69 views

DML , ML with restricted dependent types

Refering to this paper Dependent ML: An Approach to Practical Programming with Dependent Types Have defined datatype 'alist ( int ) Its not clear why they have used int as a parameter rather than a ...
4
votes
1answer
529 views

Family of types in type theory

Can anyone simplify the meaning of families of types index by a type. It looks i get it but quite not understood it. What do you mean by a "family" ? I understand index by a value (n length sequence)...
0
votes
0answers
439 views

Type inference and Type checking

I understand that adding the annotations (dependent typing) may cause the type checking of the programming language to become undecidable. What about type inference ? Whether type checking and type ...
2
votes
1answer
134 views

Variable rule in dependent type theory

This is the = Type variable rule that I'm seeing through out the my course and unable to grasp it completely. $$\dfrac{\phi \vdash \Gamma[\mathrm{ctx}] \qquad \Gamma(x) = \tau} {\phi; \Gamma ...
19
votes
1answer
2k 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 ...
6
votes
1answer
653 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 ...
6
votes
1answer
174 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?
8
votes
2answers
402 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....
5
votes
0answers
60 views

Can we simulate any dependent datatype with `Eq`?

Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
6
votes
1answer
186 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 ...
5
votes
1answer
81 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 = ...
5
votes
1answer
90 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 ...
1
vote
0answers
23 views

Importance of indexes in Type(i) in calculus of inductive constructions [duplicate]

So I am reading about the calculus of inductive constructions. And I see here and here that there hidden indexes that the user does not know about in the $Type$ sort. It says that they are ...
10
votes
2answers
1k 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 ...
4
votes
1answer
526 views

Why are dependently typed languages such as Agda used for proofs, if supercompilers for simpler typed languages can do the same?

Proof assistants such as Agda can be used to assert properties about programs, such as "the double of a number is even". Interestingly, supercompilers can be used for the same purpose, creating ...
3
votes
0answers
130 views

Test cases for subtyping with dependent types

I implemented a simple type system inside Agda and I'm trying to understand, how expressive it is. The system consists from a predicative hierarchy of universes in the style of Russell, natural ...
40
votes
2answers
7k 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 ...
7
votes
1answer
234 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 ...
20
votes
3answers
1k 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}} \...
12
votes
1answer
305 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 ...
1
vote
0answers
96 views

Representing inductive types

I implemented dependently typed lambda calculus in the spirit of this article: http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf The calculus, works and I experimented with it and like it. However, I ...
3
votes
1answer
143 views

Is this a well founded inductive type? Can I express this in Coq?

the standard List type in Coq can be expressed as: Inductive List (A:Set) : Set := nil : List A | cons : A -> List A -> List A. as I understand, W-type ...
8
votes
2answers
438 views
6
votes
1answer
422 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 ...
2
votes
1answer
554 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 ...
6
votes
2answers
254 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 ...
11
votes
2answers
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 : \...

1
2