[Agda] Coinduction and Instance Arguments - is it possible?

[Apostolis Xekoukoulotakis]

I have a datatype (called "Bob") that tracks whether a variable has been
used or not.
I have an index datatype that points to multiple variables in the datatype
Bob without depending on the datatype "Bob" so as to not become invalid
when "Bob" changes to reflect the unavailability of a variable.

The datatype "Belongs" depends on an Index and Bob. It proves that all the
variables pointed by the index are actually available.

Every time Bob, changes, a new Belongs datatype is needed. I want this
proof to be generated by instance resolution.

I am not sure if this is possible when the index points to an infinite
number of variables, ie if we have coinductive types.

Here is the example.

-------------------------

module Test where

open import Data.Bool
open import Size

mutual

data Bob (i : Size) : Set where
more : Bob i → Bool → Bob i
none : Bob i
twoPaths : Bob i → Bob i → Bob i
inf : Bob∞ i → Bob i

record Bob∞ (i : Size) : Set where
coinductive
field
bob : {j : Size< i} → Bob j

open Bob∞

data Bel : Set where
bel : Bel
nbel : Bel

mutual

data Index (i : Size) : Set where
here : Index i
more : Index i → Bel → Index i
left : Index i → Index i
right : Index i → Index i
inf : Index∞ i → Index i

record Index∞ (i : Size) : Set where
coinductive
field
index : {j : Size< i} → Index j

open Index∞

mutual

data Belongs {i : Size} : Index i → Bob i → Set where
instance
here : ∀{b} → Belongs here (more b true)
moreBel : ∀{ind b} → {{is : Belongs ind b}} → Belongs (more ind bel)
(more b true)
morenBel : ∀{ind b bool} → {{is : Belongs ind b}} → Belongs (more ind
nbel) (more b bool)
left : ∀{ind bl br} → {{is : Belongs ind bl}} → Belongs (left ind)
(twoPaths bl br)
right : ∀{ind bl br} → {{is : Belongs ind br}} → Belongs (right ind)
(twoPaths bl br)
inf : ∀{ind∞ bob∞} → {{is∞ : Belongs∞ ind∞ bob∞}} → Belongs (inf
ind∞) (inf bob∞)

record Belongs∞ {i : Size} (ind∞ : Index∞ i) (bob∞ : Bob∞ i) : Set where
coinductive
field
belongs : {j : Size< i} → Belongs (index ind∞) (bob bob∞)

open Belongs∞

mutual

b : ∀{i} → Bob i
b = more (inf b∞) true

b∞ : ∀{i} → Bob∞ i
bob b∞ = b


mutual

ind : ∀{i} → Index i
ind = more (inf ind∞) bel

ind∞ : ∀{i} → Index∞ i
index ind∞ = ind


data R : Set where
r : R

test : {{bl : Belongs ind b}} → R
test = r


-- I want instance resolution to create this datatype.

mutual

bl : {i : Size} → Belongs {i} ind b
bl = moreBel {{inf {{bl∞}}}}

bl∞ : {i : Size} → Belongs∞ {i} ind∞ b∞
belongs bl∞ = bl


f : R
f = test

[Jesper Cockx]

Hi Apostolis,

Instance search is not meant to construct new recursive (or corecursive)
solutions, so it is not able to automatically find your term bl unless
you've already defined it somewhere before.

However, are you sure the types 'Index' and 'Belongs' define what you want
them to mean? Usually you have one infinite datastructure (such as a
stream) and a type of *finite* indices (such as natural numbers). So I
don't think you need the 'inf' constructor for Index and Belongs. Without
these constructors, it should be possible to have instance search construct
proofs of Belongs, since then all proofs are finite.

I hope this helps.

-- Jesper


ps: A remark about terminology: you seem to be using the word 'datatype'
when you mean 'element of the datatype'.

On Sat, Feb 10, 2018 at 7:56 PM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
I have a datatype (called "Bob") that tracks whether a variable has been
used or not.
I have an index datatype that points to multiple variables in the datatype
Bob without depending on the datatype "Bob" so as to not become invalid
when "Bob" changes to reflect the unavailability of a variable.
The datatype "Belongs" depends on an Index and Bob. It proves that all the
variables pointed by the index are actually available.
Every time Bob, changes, a new Belongs datatype is needed. I want this
proof to be generated by instance resolution.
I am not sure if this is possible when the index points to an infinite
number of variables, ie if we have coinductive types.
Here is the example.
-------------------------
module Test where
open import Data.Bool
open import Size
mutual
data Bob (i : Size) : Set where
more : Bob i → Bool → Bob i
none : Bob i
twoPaths : Bob i → Bob i → Bob i
inf : Bob∞ i → Bob i
record Bob∞ (i : Size) : Set where
coinductive
field
bob : {j : Size< i} → Bob j
open Bob∞
data Bel : Set where
bel : Bel
nbel : Bel
mutual
data Index (i : Size) : Set where
here : Index i
more : Index i → Bel → Index i
left : Index i → Index i
right : Index i → Index i
inf : Index∞ i → Index i
record Index∞ (i : Size) : Set where
coinductive
field
index : {j : Size< i} → Index j
open Index∞
mutual
data Belongs {i : Size} : Index i → Bob i → Set where
instance
here : ∀{b} → Belongs here (more b true)
moreBel : ∀{ind b} → {{is : Belongs ind b}} → Belongs (more ind bel)
(more b true)
morenBel : ∀{ind b bool} → {{is : Belongs ind b}} → Belongs (more
ind nbel) (more b bool)
left : ∀{ind bl br} → {{is : Belongs ind bl}} → Belongs (left ind)
(twoPaths bl br)
right : ∀{ind bl br} → {{is : Belongs ind br}} → Belongs (right ind)
(twoPaths bl br)
inf : ∀{ind∞ bob∞} → {{is∞ : Belongs∞ ind∞ bob∞}} → Belongs (inf
ind∞) (inf bob∞)
record Belongs∞ {i : Size} (ind∞ : Index∞ i) (bob∞ : Bob∞ i) : Set where
coinductive
field
belongs : {j : Size< i} → Belongs (index ind∞) (bob bob∞)
open Belongs∞
mutual
b : ∀{i} → Bob i
b = more (inf b∞) true
b∞ : ∀{i} → Bob∞ i
bob b∞ = b
mutual
ind : ∀{i} → Index i
ind = more (inf ind∞) bel
ind∞ : ∀{i} → Index∞ i
index ind∞ = ind
data R : Set where
r : R
test : {{bl : Belongs ind b}} → R
test = r
-- I want instance resolution to create this datatype.
mutual
bl : {i : Size} → Belongs {i} ind b
bl = moreBel {{inf {{bl∞}}}}
bl∞ : {i : Size} → Belongs∞ {i} ind∞ b∞
belongs bl∞ = bl
f : R
f = test
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Apostolis Xekoukoulotakis]

Yes, I need to remove Inf and insert a finite version of it. There are some
repercussions though which I need to deal with.

Let us say that we have a stream that gives two natural numbers at a time.
Now, with agda, you can give the same stream to two different functions.
The first will use the first natural number and the second the second.

In our case, the computation can be destructive. Thus after the first
function, we will have a stream in which the first number has been used.
Because an infinite index on the stream does not allow us to produce a
"belongs" proof with instance resolution, I think that I should call all
the stream as used.

That would force people to split the stream into two infinite parts and
then give each part to the corresponding function.

(Splitting the stream might be tricky because we do not permit "aliasing",
we need to prove that the two new streams do not use a common
resource/memory/variable.)

I hope it works.

ps : an "element of a datatype" is too big of a phrase to use. :)

Post by Jesper Cockx
Hi Apostolis,
Instance search is not meant to construct new recursive (or corecursive)
solutions, so it is not able to automatically find your term bl unless
you've already defined it somewhere before.
However, are you sure the types 'Index' and 'Belongs' define what you want
them to mean? Usually you have one infinite datastructure (such as a
stream) and a type of *finite* indices (such as natural numbers). So I
don't think you need the 'inf' constructor for Index and Belongs. Without
these constructors, it should be possible to have instance search construct
proofs of Belongs, since then all proofs are finite.
I hope this helps.
-- Jesper
ps: A remark about terminology: you seem to be using the word 'datatype'
when you mean 'element of the datatype'.
On Sat, Feb 10, 2018 at 7:56 PM, Apostolis Xekoukoulotakis <

Post by Apostolis Xekoukoulotakis
I have a datatype (called "Bob") that tracks whether a variable has been
used or not.
I have an index datatype that points to multiple variables in the
datatype Bob without depending on the datatype "Bob" so as to not become
invalid when "Bob" changes to reflect the unavailability of a variable.
The datatype "Belongs" depends on an Index and Bob. It proves that all
the variables pointed by the index are actually available.
Every time Bob, changes, a new Belongs datatype is needed. I want this
proof to be generated by instance resolution.
I am not sure if this is possible when the index points to an infinite
number of variables, ie if we have coinductive types.
Here is the example.
-------------------------
module Test where
open import Data.Bool
open import Size
mutual
data Bob (i : Size) : Set where
more : Bob i → Bool → Bob i
none : Bob i
twoPaths : Bob i → Bob i → Bob i
inf : Bob∞ i → Bob i
record Bob∞ (i : Size) : Set where
coinductive
field
bob : {j : Size< i} → Bob j
open Bob∞
data Bel : Set where
bel : Bel
nbel : Bel
mutual
data Index (i : Size) : Set where
here : Index i
more : Index i → Bel → Index i
left : Index i → Index i
right : Index i → Index i
inf : Index∞ i → Index i
record Index∞ (i : Size) : Set where
coinductive
field
index : {j : Size< i} → Index j
open Index∞
mutual
data Belongs {i : Size} : Index i → Bob i → Set where
instance
here : ∀{b} → Belongs here (more b true)
moreBel : ∀{ind b} → {{is : Belongs ind b}} → Belongs (more ind
bel) (more b true)
morenBel : ∀{ind b bool} → {{is : Belongs ind b}} → Belongs (more
ind nbel) (more b bool)
left : ∀{ind bl br} → {{is : Belongs ind bl}} → Belongs (left ind)
(twoPaths bl br)
right : ∀{ind bl br} → {{is : Belongs ind br}} → Belongs (right
ind) (twoPaths bl br)
inf : ∀{ind∞ bob∞} → {{is∞ : Belongs∞ ind∞ bob∞}} → Belongs (inf
ind∞) (inf bob∞)
record Belongs∞ {i : Size} (ind∞ : Index∞ i) (bob∞ : Bob∞ i) : Set where
coinductive
field
belongs : {j : Size< i} → Belongs (index ind∞) (bob bob∞)
open Belongs∞
mutual
b : ∀{i} → Bob i
b = more (inf b∞) true
b∞ : ∀{i} → Bob∞ i
bob b∞ = b
mutual
ind : ∀{i} → Index i
ind = more (inf ind∞) bel
ind∞ : ∀{i} → Index∞ i
index ind∞ = ind
data R : Set where
r : R
test : {{bl : Belongs ind b}} → R
test = r
-- I want instance resolution to create this datatype.
mutual
bl : {i : Size} → Belongs {i} ind b
bl = moreBel {{inf {{bl∞}}}}
bl∞ : {i : Size} → Belongs∞ {i} ind∞ b∞
belongs bl∞ = bl
f : R
f = test
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda