# Questions tagged [inductive-datatypes]

The tag has no usage guidance.

31 questions
29 views

### How can one flip a stream using corecursion

Following is the definition of codata stream: codata Stream where hd : Stream −> A tl : Stream −> Stream For simplicity I assume I have just a ...
69 views

### In Agda's GADT, is “parameterized” and “indexed” different semantically?

I know they have difference in scoping: data a (n : Set) : Set where introA : a n data b : Set -> Set where introB : {n : Set} -> b n That's not ...
40 views

### How to define the natural numbers as a W-type?

I'm having trouble understanding the rules for W-types in type theory as defined here: https://ncatlab.org/nlab/show/W-type#wtypes_in_type_theory Can someone give an example of how these rules could ...
88 views

### Finite list induction principle and the tail eliminator

In Dybjer's Inductive Families the author present a method to derive an eliminator/induction principle for every inductive family of types. In particular for the type of finite lists, namely List' \...
40 views

### Restrictions needed on ADT for totality

In the paper Total Functional Programming by D.A. Turner three rules are given for a programming language to remain total: complete case analysis covariant type recursion (type constructor should not ...
412 views

### How to derive dependently typed eliminators?

In dependently-typed programming, there are two main ways of decomposing data and performing recursion: Dependent pattern matching: function definitions are given as multiple clauses. Unification ...
36 views

### Bridging inductive natural number and bits?

Most popular representation for the natural numbers in type systems is: Inductive nat : Set := | 0 : nat | S : nat -> nat. However, digital computers ...
80 views

### In Coq, what does it mean to have an inductive type where the right-hand side of “:” is Prop?

I'm new to Coq, and my (rather limited) understanding is that inductive types are like algebraic datatypes in Haskell, so there is a constructor data T = A a with ...
261 views

### “Smallest set” term in the trees set definition

I often meet such kind of the definition of the set of trees, as: The set of unranked $\Sigma$-trees, denoted by $T$, is the smallest set of strings over $\Sigma$ and the parenthesis symbols ‘)’ and ‘...
153 views

### Prefix encoding of algebraic data types

I'm new to coding theory and formal proofs, and am struggling to understand how to construct and reason about prefix-free encoding algorithms on algebraic data types. I hope it's clear if I use ...
384 views

### Example of inductive sets that are neither least nor greatest fixed point

Do there exist a set of inductive rules and a fixed point of these rules but is neither the least nor the greatest fixed points?
126 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 ...
131 views

### Can properties such as memory usage of a function be expressed in a dependently typed language?

Suppose one wants to reason about properties of code beyond things like totality and functional purity - one also cares about the memory consumption, or algorithmic complexity of a function. Can this ...
1k views

### What is induction-induction?

What is induction-induction? The resources I found are: the HoTT book, at the end of chapter 5.7. nLab's article a paper called Inductive-inductive definitions this blog post also mentions inductive-...
79 views

### What kinds of problems are modeled by a recursive definition of a set of strings?

Given this definition: The set $\Sigma^*$ of strings over the alphabet $\Sigma$ is defined recursively by: BASIS STEP: $\lambda \in \Sigma^*$ (where $\lambda$ is the empty string) RECURSIVE ...
710 views

### Strict positivity

From This reference : Strict positivity The strict positivity condition rules out declarations such as ...
54 views

### Can we simulate any dependent datatype with Eq?

Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
393 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 ...
292 views

### Do Self Types make the Calculus of Inductive Constructions obsolete?

Self Types are an extension of the Calculus of Constructions  that allow the language to express algebraic datatypes encoded through the Scott Encoding. The Scott Encoding provides one the ability ...
62 views

### Self referential data

Can anyone show me step by step how to do a proof on self referential structures. For example, this example is in scala ...
404 views

### Is the strictly positive condition in Coq and Agda an aproximation?

Languages like Coq and Agda enforce that their inductive types occur "strictly positively" in their definitions. That is, the type should not occur to the left of an arrow of an argument of a ...
33 views

### How do algebraic datatypes relate to free structures?

I know that: Binary leaf trees are free magmas. Non-empty lists are free semigroups. Lists are free monoids. The generalized algebraic datatype ...
70 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 ...
209 views

### Simple question COQ

I'm a beginner in the coq proof assistant, so sorry if my question is silly. I would like to prove properties of a mathematical object. For clarity I will describe an over-simplified version of my ...
147 views

### How can finite sets be represented as a type?

Manually self-migrated from stack overflow. A set of objects of a type T is often represented using its indicator function (set T = ...
116 views

### Unrolling multi-variable mu (μ) expressions in type theory

Unrolling an iso-recursive μ-type expression such as, say, one isomorphic to natural numbers: μα.1+α using ...
119 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 ...
298 views

### Inductive vs. recursive definition

When should I call a definition recursive and when should I call it inductive? I have read Carl Mummert's nice answer on MSE. So if I understand correctly we refer to definitions of objects like ...
204 views

### Is constant a variable or subtype?

I think of type as a range of values that the variable can take whereas the rest is known constant or does not matter. Variables (instances or objects), which share common properties, are considered ...