[Agda] Fwd: Coinductive datatypes

[Álvaro García Pérez]

Hi,

I've misunderstood some concepts.

What I was meaning is how to construct an inductive-recursive data type in
agda. Forget about coinduction and the codata keyword.

Is there a way to implement the inductive-recursive DList datatype in Agda2?
Is there a way to avoid scope checking errors in the following program?

...

data DList : Set where
  nil : DList
  cons : (a : Nat) -> (l : DList) -> {True (Fresh a l)} -> DList

Fresh : (a : Nat) -> (DList) -> Bool
Fresh a nil = t
Fresh a (cons b bs) = if (a # b) then (Fresh a bs) else f

...

The compiler raises:
/home/agarcia/Escritorio/Mis documentos/2007-2008/BABEL/
agda/recursive.agda:57,38-56
{True (Fresh a l)} cannot appear by itself. It needs to be the
argument to a function expecting an implicit argument.
when scope checking {True (Fresh a l)}

Thanks again,

Alvaro.

---------- Forwarded message ----------
From: Álvaro García Pérez <agarcia at babel.ls.fi.upm.es>
Date: 2008/9/25
Subject: Coinductive datatypes
To: agda at lists.chalmers.se


Hi to everybody,

I'm trying to implement coinductive datatypes in agda, specifically the data
DList and the Fresh function as they appear in [Dybjer 2000].

Formation rules:
Dlist : set,
Fresh : (Dlist)(A)set

Introduction ruels:
nil : Dlist,
cons : (b : A) (u : Dlist) (b' : Fresh (u, b)) Dlist.

Equality rules:
Fresh(nil, a) = T,
Fresh(cons(b, u, b'), a) = b#a ^ Fresh(u, a).
(where b#a is true if b and a are not equal)

I've used the codata keyword and corecursive functions:
data Zero : Set where

data One : Set where
  tt : One

data Bool : Set where
  t : Bool
  f : Bool

data Nat : Set where
  z : Nat
  s : (n : Nat) -> Nat

_#_ : Nat -> Nat -> Bool
z # z = t
z # s n = f
s n # z = f
s n # s n' = n # n'

if_then_else_ : Bool -> Bool  -> Bool -> Bool
if t then true else false = true
if f then true else false = false

True : Bool -> Set
True t = One
True f = Zero

_and_ : Bool -> Bool -> Bool
f and _ = f
t and f = f
t and t = t

codata DList : Set where
  nil : DList
  cons : (a : Nat) -> (l : DList) -> {True (Fresh a l)} -> DList

Fresh : (a : Nat) -> (DList) -> Bool
Fresh a nil ~ t
Fresh a (cons b bs) ~ if (a # b) then (Fresh a bs) else f

The compiler raises:
/home/agarcia/Escritorio/Mis
documentos/2007-2008/BABEL/agda/recursive.agda:57,38-56
{True (Fresh a l)} cannot appear by itself. It needs to be the
argument to a function expecting an implicit argument.
when scope checking {True (Fresh a l)}

Are codatatypes and corecursive functions in Agda2 intended to be used that
way? How can I point to the compiler that the Fresh function will appear
later in the program, avoiding the scope checking error?

Is it possible to implement the Dlist datatpye as [Dybjer 2000] describes it
or should I used another schema?

Thanks a lot.

Alvaro,

References:
[Dybjer 2ooo]: Dybjer, P. A general formulation of simultaneous
inductive-recursive definitions in type theory, Journal of Symbolic Logic,
2000, vol. 65, p. 2000
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080925/3a76999d/attachment.html