Questions tagged [dependent-types]

An overlapping feature of type theory and type systems.

Filter by
Sorted by
Tagged with
3
votes
2answers
295 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 ...
2
votes
1answer
739 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
97 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
60 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
466 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
398 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
120 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 ...
18
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 ...
18
votes
2answers
431 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 ...
6
votes
1answer
158 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
344 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
2answers
373 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:...
5
votes
0answers
58 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
513 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 ...
9
votes
2answers
316 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 ...
6
votes
1answer
169 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
76 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 = ...
22
votes
1answer
2k 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 ...
5
votes
1answer
75 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
22 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 ...
9
votes
2answers
964 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 ...
3
votes
0answers
121 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 ...
7
votes
1answer
213 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 ...
17
votes
3answers
871 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}} \...
11
votes
1answer
236 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 ...
13
votes
2answers
439 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 ...
4
votes
1answer
489 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 ...
1
vote
0answers
84 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 ...
59
votes
3answers
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 ...
3
votes
1answer
134 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 ...
7
votes
2answers
353 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: ...
35
votes
2answers
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 ...
5
votes
1answer
372 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
506 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 ...
8
votes
2answers
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?
6
votes
2answers
236 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 ...
10
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 : \...
42
votes
1answer
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 ...