Stack Overflow
Stack Overflow

Questions tagged [coinduction]

43 questions
31
votes
3 answers

Are Lists Inductive or Coinductive in Haskell?

So I've been reading about coinduction a bit lately, and now I'm wondering: are Haskell lists inductive or coinductive? I've also heard that Haskell doesn't distinguish the two, but if so, how do they do so formally? Lists are defined inductively,…
Crazycolorz5
  • 747
  • 6
  • 12
15
votes
1 answer

How do I convert an inductive type into a coinductive type efficiently (without recursion)?

> {-# LANGUAGE DeriveFunctor, Rank2Types, ExistentialQuantification #-} Any inductive type is defined like so > newtype Ind f = Ind {flipinduct :: forall r. (f r -> r) -> r} > induction = flip flipinduct induction has type (f a -> a) -> Ind f ->…
PyRulez
  • 10,513
  • 10
  • 42
  • 87
13
votes
3 answers

Are codatatypes really terminal algebras?

(Disclaimer: I'm not 100% sure how codatatype works, especially when not referring to terminal algebras). Consider the "category of types", something like Hask but with whatever adjustment that fits the discussion. Within such a category, it is said…
Sylvain Hubert
  • 384
  • 1
  • 9
8
votes
1 answer

How to define constant heterogeneous streams in Haskell?

I understand how to define both homogeneous and heterogeneous streams in Haskell. -- Type-invariant streams. data InvStream a where (:::) :: a -> InvStream a -> InvStream a -- Heterogeneous Streams. data HStream :: InvStream * -> * where …
Mario Román
  • 600
  • 7
  • 12
8
votes
1 answer

Trouble to understand Agda's Coinduction

I'm trying to code a functional semantics for IMP language with parallel preemptive scheduling as presented in section 4 of the following paper. I'm using Agda 2.5.2 and Standard library 0.13. Also, the whole code is available at the following…
Rodrigo Ribeiro
  • 3,198
  • 1
  • 18
  • 26
7
votes
3 answers

Is an infinite list of ones sane?

In Prolog, is the unification X = [1|X] a sane way to get an infinite list of ones? SWI-Prolog does not have any problem with it, but GNU Prolog simply hangs. I know that in most cases I could replace the list with one(1). one(X) :- one(X). but my…
Kijewski
  • 25,517
  • 12
  • 101
  • 143
5
votes
1 answer

How can i prove that cons after uncons over coinductive list(a.k.a Stream) are identity, in Agda?

I'm studying coinductive and copatterns through https://agda.readthedocs.io/en/v2.6.0.1/language/coinduction.html . I thought I understood the article code, so I decided to work on the following proposition. cons-uncons-id : ∀ {A} (xs : Stream A) →…
いとうかつとし
  • 95
  • 4
5
votes
1 answer

CoNat : proving that 0 is neutral to the left

I am experimenting with the definition of CoNat taken from this paper by Jesper Cockx and Andreas Abel: open import Data.Bool open import Relation.Binary.PropositionalEquality record CoNat : Set where coinductive field iszero : Bool …
Dave
  • 147
  • 5
5
votes
1 answer

Is equality decidable on any coinductive type?

this is my first post, apologies if it I have made mistakes. I suspect that, in Coq, coinductive types like Stream do not have decidable equality. That is, given two streams s and t, it is not possible identify whether s=t or ~(s=t). I suspect that…
Mitchell Buckley
  • 118
  • 6
5
votes
1 answer

Proof of stream's functor laws

I've been writing something similar to a Stream. I am able to prove each functor law but I can not figure out a way to prove that it's total: module Stream import Classes.Verified %default total codata MyStream a = MkStream a (MyStream…
Brian McKenna
  • 45,528
  • 6
  • 61
  • 60
4
votes
0 answers

Coq: Proving conat is either finite or infinite

I have a definition of conat which can represent both finite and infinite values, a conversion from nat, a definition of infinity, and a bisimulation relation: CoInductive conat : Set := O' | S' (n : conat). Fixpoint toCo (n : nat) : conat := match…
Bubbler
  • 940
  • 6
  • 15
4
votes
2 answers

Termination checker fails after abstracting the call site

Problem I have a simple coinductive record with a single field of a sum type. Unit gives us a simple type to play with. open import Data.Maybe open import Data.Sum data Unit : Set where unit : Unit record Stream : Set where coinductive …
Emily Horsman
  • 195
  • 1
  • 7
4
votes
0 answers

Agda: how to do non-terminating IO (getLine) without (the deprecated?) ∞-style coinduction?

In this question about how to do getLine in Agda the main answer suggests using the partiality monad to deal with the possible non-termination of working with the resulting Costring. On the other hand, in version 2.5.3 the manual page on Coinduction…
André Gustavo Rigon
  • 73
  • 4
4
votes
2 answers

Compute an (infinite) tree from fixpoint operator using delay modality

Here is a functional programming puzzle involving loop-tying and infinite data structures. There is a bit of background, so hang tight. The setting. Let us define a data type representing recursive data types: type Var = String data STerm = SMu Var…
Edward Z. Yang
  • 26,325
  • 16
  • 80
  • 110
3
votes
0 answers

corecursive Agda functions without sized types

I've been doing some experiments with the "old" and "new" ways of dealing with coinduction in Agda, but I think I'm still missing some important facts about the behavior of Agda's termination checking of corecursive functions when Size is not…
Luca
  • 31
  • 1
1
2 3