Questions tagged [dependent-types]

An overlapping feature of type theory and type systems.

Filter by
Sorted by
Tagged with
3
votes
2answers
262 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 ...
3
votes
1answer
66 views

How to determine whether a dependent type that doesn't fit the monad instance is categorically a monad

[Using Idris syntax and terminology, but the question is not about Idris] If a monad interface (or type class) has a constraint requiring applicative functor, a monad instance can be written by ...
3
votes
1answer
166 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. ...
3
votes
1answer
130 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 ...
3
votes
1answer
127 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 ...
3
votes
2answers
165 views

partial (and non deterministic) functions in dependently typed lambda calculus

A partial function is one, that that is only defined on a part of its domain. Haskell gives examples: https://wiki.haskell.org/Partial_functions My end goal is to express types $$ \prod_{D:\mathcal{...
3
votes
1answer
139 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 ...
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 ...
2
votes
1answer
65 views

Show how lack of universe levels would create contradiction in homotopy type theory (in Agda)

The homotopy type theory book claims in section 1.3 that "As in naive set theory, we might wish for a universe of all types" but from this one could "deduce from it that every type, including the ...
2
votes
1answer
620 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 ...
2
votes
2answers
114 views

How to prove this obvious theorem in type theory (LEAN prover)

I have the following code: ...
2
votes
1answer
135 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 ...
2
votes
1answer
76 views

Does co-inductive and co-recursive types also have their recursors?

I'm new to type theory, and recently read introductory materials where dependent type are discussed. One of my friend asked me, "Those dependent types are having recursors & 'inductors'(dependent ...
2
votes
1answer
115 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 ...
2
votes
1answer
475 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 ...
2
votes
1answer
69 views

Difference between computation in proposition proof and definitional computation?

As stated in equality at nLab, "computational equality" is about computational steps which take for example, $s(s(0))+ s(0)$ to $s(s(s(0)))$ and it acts exactly and can be considered same as ...
2
votes
1answer
46 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 ...
2
votes
1answer
234 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 ...
2
votes
0answers
49 views

Are there any interesting terms in pure LF or $\lambda\Pi$?

In my searching, I've seen that if Church numerals are encoded in a dependently typed Lambda calculus, that we can't derive induction or that $0 \neq 1$. I know that LF and the dependently typed ...
2
votes
0answers
95 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, ...
1
vote
1answer
50 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 ...
1
vote
2answers
52 views

Propositional truncation of excluded middle

It is clear to me that it should be impossible to prove : exclMidl = isProp A → ((A) ⊎ (¬ A)) Because it would give deciding oracle for every Proposition. My ...
1
vote
1answer
38 views

Does dependent type checkers need to store lambda parameter type in their core language?

"Core language" refers to the exported well-typed terms that can be evaluated (or reduced). In the core language of MiniAgda, a dependently-typed language, the parameter type of a lambda is not ...
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 ...
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 ...
1
vote
0answers
82 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 ...
0
votes
1answer
95 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 ...
0
votes
1answer
51 views

Meaning of $\mu t$ terms in dependent type theory

What is the meaning of the term $\mu t$ in the type theory formalized in this paper (section 2.1, page 2)?
0
votes
1answer
79 views

Is it possible to interpret some Martin-Löf types as abelian monoids in such a way that any abelian monoid can be represented as a type?

For instance, I can interpret the unit type as the trivial monoid with one element. Non-dependent pairs $A \times B$ can be interpreted as the direct sum $A ⊕ B$ when $A$ and $B$ can both be ...
0
votes
0answers
380 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 ...
-1
votes
2answers
57 views

Defining an HTML Template as an Algebraic Type

Wondering if/how you could define a highly nested structure as a Dependent Type (or an Algebraic or Parameterized type). Specifically, an HTML template. Not that they work like this (HTML templates ...