20

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 similar thing happens in category theory, where we say contravariant and covariant instead of negative and positive, respectively. In physics they speak of ...


16

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 explanations in the Forsberg & Setzer's paper A finite axiomatisation of inductive-inductive definitions illuminating. Induction-recursion An inductive-recursive ...


9

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 for free by Philip Wadler). I guess the origin of the term 'negative position' stems from the notion of contravariance ('contra' means opposite). It is not allowed to have the type being defined ...


9

Inductive types are similar to Haskell's data, but they are more general. An inductive definition in Set describes a way to build a piece of data from smaller pieces. For example, the following definition defines a type called prod which allows taking two pieces of data and bundling them together. Inductive prod (A B : Set) : Set := pair : A -> B -> ...


8

The canonical reference for this is Peter Dybjer, Inductive Families, which gives a pretty comprehensive treatment of inductive families based on eliminators.


8

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 the video Anton mentioned is Daniellson's work in Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. This does indeed use a ...


7

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 $$ \dfrac{\qquad}{0} \qquad \dfrac{x}{x+1} $$ This induces the (monotonic, Scott-continuous) function $f : \mathcal{P}(\mathbb{R}) \to \mathcal{P}(\mathbb{R})$ ...


7

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 form $$T = \Phi(T).$$ (If this is not clear, please ask.) Sometimes $\Phi$ depends on a parameter $p : P$ of some given type $P$, so we have a parameterized ...


6

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 basic technique applied just to the Nat type.


6

Any set is a fixed point of the empty set of rules or of the trivial rule $x\in X\Rightarrow x\in X$.


6

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 match t as x in T1 return T2 with | C1 a1 ... an ... In particular, ommiting any of the as, in or return clauses can prevent type inference of the statement. Intuitively, if the type of (say) ...


5

If you want a type system for finite sets that enforces the validity and unicity of all representations, then your type system must be able to model equality of elements. (Informal proof: insert x (insert y empty) has differently-shaped representations depending on whether x and y are equal.) This is impossible with algebraic datatypes alone, unless you're ...


5

I can't image they end up equivalent. That's where you're wrong! In fact, starting with two different unfoldings of some expression you can always keep unfolding them in such a way that they "meet" again. This property is formally called confluence. More formally: define $$ T \rightarrow_\tau T'$$ If $T'$ is the result of a repeated number of unfoldings ...


4

A code is prefix-free if there does not exist any distinct two values v, w such that encode(v) is a prefix of encode(w). So, to prove that your encoding is prefix-free, you start by considering two arbitrary distinct values v, w and demonstrate that encode(v) is not a prefix of encode(w). I suggest you use proof by induction on the "size" of the largest ...


4

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 here is an inductive definition. The base case is implicit because $\epsilon \in T^*$ even if $T = \emptyset$; making is explicit, the definition is (reading $a$ ...


4

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 correct, so I'd give it a little time. The work is certainly very promising. One thing to note is that these restrictions are actually quite non-trivial to ...


4

We can prove (x : Nat) (y : Nat) -> x + y = y + x (they are propositionally equal). I'm using Agda-ish notation here rather than the notation in the HoTT book because type setting is hard. Note that we can prove this in standard intensional type theory. This gives a function from Nat to Nat to a proof of equality. In intensional type theory we don't ...


4

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 You can do this with a parameterized type by taking an argument: data T (n : ℕ) : Set where t : n ≡ 5 → T n But ≡ is itself an indexed type, so you need something indexed at the bottom (≡ can ...


4

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 the infinite lists are not even a fixed point, since applying $F$ will add $\mathrm{Nil}$, which is not infinite. However, adding the infinite lists is the right ...


3

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}-\text{Introduction}$$ You can define the natural numbers by setting $A=Bool$ and $B(a) = \text{if}\; a\; \text{then}\; ⟂\; \text{else}\; Unit$. Where $⟂$ is the ...


3

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 typical trick in this situation is to pick a C such that you can pretend you are defining a function on the whole family when, in fact, you're only focusing on the ...


3

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 exactly as mappings $f\colon \{1,\ldots,n\} \to \Sigma$ for some $n \in \mathbb{N}$. There are several different ways of understanding your definition, which is ...


3

You have misunderstood why A stands there in the definition of list. Let us first look at how we might define lists of booleans: Inductive ListBool : Set := | nilBool : ListBool | consBool : bool -> ListBool -> ListBool. And here is how we might define lists of natural numbers: Inductive ListNat : Set := | nilNat : ListNat | consNat : nat -&...


2

Set-theoretic thinking is creating trouble, as you are trying to do things in non-Coq ways. Let me show you a solution which works better, and then you can explain what your actual non-simplified problem is -- we can probably optimize that one to. If we have two lists A and B then we do not have to tag the elements of the first list with 0 and the second ...


2

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} \bigcup_{m \in \mathbb{N}} \{ a(t_1 \ldots t_m) : t_1,\ldots,t_m \in T_n \}. $$ I claim that $$ T = \bigcup_{n \in \mathbb{N}} T_n. $$ Indeed, you can prove by ...


2

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$. Assume $t \in T$ and lets call such strings "well-structured", those which do not look like "$a)($". Base case: $t = a()$ where $a \in \Sigma$. Clearly ...


2

The constraint covariant type recursion (type constructor should not appear in negative position in a constructor argument) excludes this data Bad r = Bad (r -> r) ^ ^--- positive position ^-------- negative position Indeed, all the occurrences of r must appear in positive position. Should all type ...


2

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 intersection preserves satisfaction of the criterion). So "smallest" here means "is a subset of every set satisfying this criterion". Consequently, no proper subset ...


2

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 are not parametrized, say you have Inductive Foo := foo : Bar -> Foo with Bar := bar : Foo -> Bar (with some constants if you want to make the types ...


1

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 product of a family indexed by an empty set iff there exists an empty family of morphisms such that for every object $A$ and every empty family of morphisms, ...


Only top voted, non community-wiki answers of a minimum length are eligible