16

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 ...


11

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

This has come up on the Coq mailing list several times, but I never saw a conclusive answer. Coq isn't as general as it could be; the rules in (Coquand, 1990) and (Giménez, 1998) (and his PhD thesis) are more general and do not require strict positivity. Positivity enough is not enough, however, when you go outside Set; this example came up in several ...


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

Ralph Matthes describes how to simulate types like this in Coq in "A Datastructure for Iterated Powers" (code, paper).


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})$ ...


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

One of the first things Coq does is building the induction principle associated with the inductive type you just defined and understanding the underlying induction principle is a good exercise. For example O : nat | S : nat -> nat will generate the induction principle P O -> (∀ n, P n -> P (S n)) -> ∀ n, P n. What would be the induction ...


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$.


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 ...


5

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

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 ...


5

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 ...


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

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

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 ...


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 -&...


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

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 ...


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

An inductive definition takes some elementary objects of the structure to be defined and combines those to obtain new elements of said structure. Example: Definition of the syntax of many logics. On the contrary, a recursive definition is a rule how to obtain a specific object based on somehow "smaller" objects of the same structure. To see the difference ...


2

This seems very confused. Probably you should state which programming language you are referring to as some of these concepts may have different definitions depending on the language or formalism. Much is arbitrary (possibly not always too consistent). For example, you do not necessarily have booleans as a subtype of integers. One important issue is to ...


2

See: Mini ML Specifically the Type Inference section. This contains sample code in F# for a complete parser of a simple functional language. More importantly the Type Inference section implements the Hindley-Milner algorithm which is what is found in most type inference system. The author also provides links to two other important documents to help in ...


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 ...


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