Idris Language - Codata

As an example, imagine we want to represent 1/3, (that is 0.33333 recuring).

We could have a recursive data structure where we can continue adding '3's onto the end and read them out when required.

Perhaps we might represent an infinite sequence of threes like this:

data Threes =
  Threes

but it could never be constructed

Data

 

||| Natural numbers: unbounded, unsigned integers which can be pattern
||| matched.
data Nat =
  ||| Zero
  Z |
  ||| Successor
  S Nat

 

data List : (elem : Type) -> Type where
  ||| Empty list
  Nil : List elem
  ||| A non-empty list, consisting of a head element and the rest of
  ||| the list.
  (::) : (x : elem) -> (xs : List elem) -> List elem

 

CoData

data Stream : Type -> Type where
  (::) : (e : a) -> Inf (Stream a) -> Stream a
  
||| The first element of an infinite stream
head : Stream a -> a
head (x::xs) = x

||| All but the first element
tail : Stream a -> Stream a
tail (x::xs) = xs

 


metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.