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

[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. :)

On Sun, Feb 11, 2018 at 4:17 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> 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 <
> apostolis.xekoukoulotakis at gmail.com> wrote:
>
>> 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
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180211/956b7968/attachment-0001.html>