27
votes
Accepted
Strict positivity
First a terminological explanation: negative and positive positions come from logic. They are about an assymetry in logical connectives: in $A \Rightarrow B$ the $A$ behaves differently from $B$. A ...
- 30k
18
votes
Accepted
What is induction-induction?
Supplemental 2016-10-03: I mixed up induction-induction and induction-recursion (not the first time I did that!). My apologies for the mess. I updated the answer to cover both.
I find the ...
- 30k
10
votes
In Agda's GADT, are "parameterized" and "indexed" different semantically?
The following explanation lacks mathematicial precision but should explain what is going on.
A GADT is a special case of a recursive type. A recursive type $T$ is a solution of a type equation of the ...
- 30k
10
votes
Strict positivity
The first occurrence of Bad is called 'negative' because it represents a function argument, i.e. is located to the left of the function arrow (see Recursive types ...
- 3,469
9
votes
Accepted
In Coq, what does it mean to have an inductive type where the right-hand side of ":" is Prop?
Inductive types are similar to Haskell's data, but they are more general.
An inductive definition in Set describes a way to ...
8
votes
Accepted
How to derive dependently typed eliminators?
The canonical reference for this is Peter Dybjer, Inductive Families, which gives a pretty comprehensive treatment of inductive families based on eliminators.
- 8,114
8
votes
Can properties such as memory usage of a function be expressed in a dependently typed language?
Yes, it can. While conceptually it's not that difficult, it hasn't been studied all that much. One aspect of the field is cost semantics such as the research done by Guy Blelloch.
In the vein of ...
7
votes
Accepted
Example of inductive sets that are neither least nor greatest fixed point
Here's a non-trivial example:
Suppose we want to define inductively a subset of reals, so we work on the complete lattice $\mathcal{P}(\mathbb{R})$ ordered by inclusion.
Then, consider the rules
$$
\...
- 14.4k
6
votes
How to derive dependently typed eliminators?
You might find some of our recent papers on this useful, as we derive eliminators for lambda-encoded datatypes. For example, see this one for generic derivation of eliminators, and this one for the ...
- 61
6
votes
Example of inductive sets that are neither least nor greatest fixed point
Any set is a fixed point of the empty set of rules or of the trivial rule $x\in X\Rightarrow x\in X$.
- 81.4k
6
votes
Typing dependent pattern matching
In general matching with dependent types can be quite subtle! You'll note that in the Coq documentation that the extended pattern-matching syntax is
...
- 8,114
4
votes
Accepted
Prefix encoding of algebraic data types
A code is prefix-free if there does not exist any distinct two values v, w such that ...
D.W.♦
- 156k
4
votes
"Smallest set" term in the trees set definition
The set of unranked $Σ$-trees, denoted by $T$, is the smallest set of strings over $Σ$ and the parenthesis symbols ‘)’ and ‘(’ such that for each $a∈Σ$ and $w∈T^∗$, $a(w)$ is in $T$.
What we have ...
- 72k
4
votes
Accepted
Do Self Types make the Calculus of Inductive Constructions obsolete?
I'm not an expert in this work, but it seems to me that the major current issue is a lack of SN proof, even with restrictions. These proofs are notoriously tricky though, even when the calculus is ...
- 8,114
4
votes
Accepted
In Agda's GADT, are "parameterized" and "indexed" different semantically?
Yes and no.
The obvious difference is that indexed types are able to vary in the result type of each constructor. So you can do:
data T : ℕ → Set where
t : T 5
...
- 2,619
4
votes
How to define the natural numbers as a W-type?
The formation and introduction rules for W-types, as given on n-cat lab, are:
$$\frac{A:Type\quad x:A⊦B:Type}{(W x:A)B(x):Type}-\text{Formation}$$
$$\frac{a:A\quad t:B(a)\rightarrow W}{sup(a,t):W}-\...
- 341
4
votes
Accepted
Greatest fixpoint of the type of lists
The greatest fixed point cannot contain only the infinite lists, because it must contain all the elements of the least fixed point (and every other fixed point). Another way to see this is that just ...
- 2,619
3
votes
Accepted
Finite list induction principle and the tail eliminator
I am totally lost on how to approach this problem since the eliminator seems to be able to provide just function defined on the whole family List′A(n) and not on the sub-family List′A(s(n)).
The ...
- 573
3
votes
Accepted
What kinds of problems are modeled by a recursive definition of a set of strings?
The definition you quote is a formal definition of strings which is particularly conducive to induction. There are many other ways to define strings, for example as sequences of letters, or more ...
- 275k
2
votes
"Smallest set" term in the trees set definition
You have to prove that $a)($ doesn't belong to $T$. You can start with constructing $T$, as follows. Let $T_0 = \emptyset$, and for $n \in \mathbb{N}$, define
$$
T_{n+1} = \bigcup_{a \in \Sigma} \...
- 275k
2
votes
Accepted
"Smallest set" term in the trees set definition
I think that is trivial according to the rule of how the strings are formed: $a(w)$. But if you need a formal proof then you could prove it as following using induction on the length of strings in $T$....
- 9,757
2
votes
"Smallest set" term in the trees set definition
This use of the phrase "smallest set", or "smallest set with respect to inclusion" is generally taken to be synonymous with "the intersection of all sets satisfying this criterion" (as long as ...
- 310
2
votes
Accepted
Is mutual inductive type definition essential in coq core language?
It is always possible, as you noted, to translate a mutual inductive family into a non-mutual family, in much the same way as you described.
A couple of difficulties though:
If your mutual inductives ...
- 8,114
2
votes
Accepted
Restrictions needed on ADT for totality
The constraint
covariant type recursion (type constructor should not appear in negative position in a constructor argument)
excludes this
...
- 14.4k
1
vote
Accepted
Datatypes as initial algebras
An empty product is the same thing as a terminal object by definition of the product: it's an object $1$ such that for every object $A$, there is a unique morphism $1_A : A \rightarrow 1$. ($1$ is a ...
1
vote
Finite list induction principle and the tail eliminator
What follows is just a little modification of the idea proposed in the accepted answer, nevertheless I think it can be of interest to other readers.
Here's a way to build tail
We can consider the ...
- 153
1
vote
"Smallest set" term in the trees set definition
There are sets $T$ that satisfy the condition given (for each $a \in \Sigma$ and $w \in T^*$, $a(w) \in T$) which do contain badly-structured trees like $a)($; however, there is also a set that doesn'...
- 11
1
vote
Is it possible that the universe of types could be closed?
I'm uncertain what you're referring to exactly, but I can remark on a few things.
The first is that the usual problem with W-types is that encoding inductive types with them does not necessarily give ...
- 2,619
Only top scored, non community-wiki answers of a minimum length are eligible