Questions tagged [codata]
13 questions
19
votes
0 answers
Why not always use Inf instead of Lazy in Idris?
I find that Lazy and Inf is very close:
Lazy and Inf are closely related (in fact, the underlying
implementation uses the same type). The only difference in practice is
in totality checking, where Lazy is erased (i.e. terms are checked for
…
luochen1990
- 3,689
- 1
- 22
- 37
13
votes
1 answer
Why there is no filter function of Stream in idris?
There is filter : (a -> Bool) -> List a -> List a for List, but there is no filter : (a -> Bool) -> Stream a -> Stream a for Stream, why?
Is there some alternatives to do the similar jobs?
luochen1990
- 3,689
- 1
- 22
- 37
13
votes
1 answer
What is the difference between codata and data?
There is some explanation here. Intuitively I understand how finite data structures differ from infinite data structures like streams. Nevertheless, it's interesting to see other explanations of differences, characteristics, types of codata.
I…
Bad
- 4,967
- 4
- 34
- 50
10
votes
1 answer
What constitutes codata in the context of programming?
This is a corecursive algorithm, because with each iteration it calls itself on data that is greater then what it had before:
iterate f x = x : iterate f (f x)
It is similar to tail recursion accumulator style, but its accumulator is implicit…
user5536315
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
2 answers
Terminology for example of codata in Clojure
Imagine the following function to give an infinite lazy sequence of fibonacci in Clojure:
(def fib-seq
(concat
[0 1]
((fn rfib [a b]
(lazy-cons (+ a b) (rfib b (+ a b)))) 0 1)))
user> (take 20 fib-seq)
(0 1 1 2 3 5 8 13 21 34 55 89…
hawkeye
- 34,745
- 30
- 150
- 304
3
votes
0 answers
Should NFData have a dual?
Haskell has a type called NFData with the following shape:
class NFData a
where
rnf :: a -> ()
Types that are more "data-ish" than "function-ish" can be equipped with instances of NFData. Each such instance thoroughly case analyzes a given…
Asad Saeeduddin
- 46,193
- 6
- 90
- 139
2
votes
1 answer
Is the only difference between Inductive and CoInductive the well-formedness checks on their uses (in Coq)?
To phrase the question differently: if we were to remove termination-checking and the guardedness condition on uses of inductive and coinductive data types, respectively, would there cease to be a fundamental difference between inductive/coinductive…
Max Heiber
- 14,346
- 12
- 59
- 97
2
votes
1 answer
Agda: Simplifying recursive definitions involving Thunk
I'm trying to implement a type that represents a (possibly) infinite path on an infinite binary tree. The definition currently resembles that of Conat in the stdlib.
open import Size
open import Codata.Thunk
data BinaryTreePath (i : Size) : Set…
Bubbler
- 940
- 6
- 15
2
votes
1 answer
Pithy summary for codata (Where a comonad is a 'type for input impurity')
In terms of pithy summaries - this description of Comonads seems to win - describing them as a 'type for input impurity'.
What is an equivalent pithy (one-sentence) description for codata?
hawkeye
- 34,745
- 30
- 150
- 304
1
vote
1 answer
Detecting cheapest way to build independent iterators
Suppose I'm writing a function taking in an iterable, and my function wants to be agnostic as to whether that iterable is actually an iterator yet or not.
(This is a common situation, right? I think basically all the itertools functions are written…
Eric Auld
- 1,156
- 2
- 14
- 23
1
vote
1 answer
How to encode corecursion/codata in a strictly evaluated setting?
Corecursion means calling oneself on data at each iteration that is greater than or equal to what one had before. Corecursion works on codata, which are recursively defined values. Unfortunately, value recursion is not possible in strictly evaluated…
user5536315
1
vote
1 answer
Is there any idea to solve the floating-number-precision-prob in the future?
We can not store a decimal in infinite precision, but there may be some way to represent them just like we represent infinite lists in haskell.
The first idea came to me is to represent a decimal number via something similar to Codata, so that for…
luochen1990
- 3,689
- 1
- 22
- 37