Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [inductive-datatypes]

The tag has no usage guidance.

2
votes
0answers
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 ...
3
votes
2answers
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 ...
1
vote
1answer
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 ...
4
votes
2answers
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' \...
2
votes
1answer
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 ...
10
votes
2answers
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 ...
4
votes
0answers
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 ...
2
votes
1answer
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 ...
1
vote
5answers
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 ‘...
6
votes
1answer
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 ...
7
votes
2answers
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?
3
votes
1answer
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 ...
11
votes
1answer
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 ...
9
votes
1answer
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-...
2
votes
1answer
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 ...
6
votes
2answers
710 views

Strict positivity

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

Can we simulate any dependent datatype with `Eq`?

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

Do Self Types make the Calculus of Inductive Constructions obsolete?

Self Types are an extension of the Calculus of Constructions [1] that allow the language to express algebraic datatypes encoded through the Scott Encoding. The Scott Encoding provides one the ability ...
2
votes
0answers
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 ...
6
votes
0answers
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 ...
1
vote
0answers
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 ...
4
votes
1answer
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 ...
3
votes
2answers
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 ...
3
votes
1answer
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 = ...
5
votes
1answer
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 ...
3
votes
1answer
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 ...
6
votes
1answer
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 ...
0
votes
1answer
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 ...
11
votes
1answer
413 views

Constraint-based Type Inference with Algebraic Data

I am working on an expression based language of ML genealogy, so it naturally needs type inference >:) Now, I am trying to extend a constraint-based solution to the problem of inferring types, based ...
10
votes
3answers
646 views

Polymorphism and Inductive datatypes

I'm curious. I've been working on this datatype in OCaml: ...