<div dir="ltr"><div><div><div>Yes, I need to remove Inf and insert a finite version of it. There are some repercussions though which I need to deal with.<br><br></div>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.<br></div><br></div><div>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.<br></div><div>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.<br><br></div><div>That would force people to split the stream into two infinite parts and then give each part to the corresponding function.<br><br></div><div>(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.)<br><br></div><div>I hope it works.<br><br></div><div>ps : an "element of a datatype" is too big of a phrase to use. :)<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Feb 11, 2018 at 4:17 PM, Jesper Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Hi Apostolis,<br><br>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.<br><br></div><div>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.<br><br></div><div>I hope this helps.<br><br>-- Jesper<br></div><div><br><br></div>ps: A remark about terminology: you seem to be using the word 'datatype' when you mean 'element of the datatype'.<br></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Sat, Feb 10, 2018 at 7:56 PM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@<wbr>gmail.com</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div dir="ltr"><div><div><div><div><div>I have a datatype (called "Bob") that tracks whether a variable has been used or not.<br></div>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.<br><br></div>The datatype "Belongs" depends on an Index and Bob. It proves that all the variables pointed by the index are actually available.<br><br></div>Every time Bob, changes, a new Belongs datatype is needed. I want this proof to be generated by instance resolution.<br><br></div>I am not sure if this is possible when the index points to an infinite number of variables, ie if we have coinductive types. <br><br></div>Here is the example.<br><br>-------------------------<br><br>module Test where<br><br>open import Data.Bool<br>open import Size<br><br>mutual<br><br> data Bob (i : Size) : Set where<br> more : Bob i → Bool → Bob i<br> none : Bob i<br> twoPaths : Bob i → Bob i → Bob i<br> inf : Bob∞ i → Bob i<br><br> record Bob∞ (i : Size) : Set where<br> coinductive<br> field<br> bob : {j : Size< i} → Bob j <br><br>open Bob∞<br><br>data Bel : Set where<br> bel : Bel<br> nbel : Bel<br> <br>mutual<br><br> data Index (i : Size) : Set where<br> here : Index i<br> more : Index i → Bel → Index i<br> left : Index i → Index i<br> right : Index i → Index i<br> inf : Index∞ i → Index i<br> <br> record Index∞ (i : Size) : Set where<br> coinductive<br> field<br> index : {j : Size< i} → Index j<br><br>open Index∞<br><br>mutual<br><br> data Belongs {i : Size} : Index i → Bob i → Set where<br> instance<br> here : ∀{b} → Belongs here (more b true)<br> moreBel : ∀{ind b} → {{is : Belongs ind b}} → Belongs (more ind bel) (more b true)<br> morenBel : ∀{ind b bool} → {{is : Belongs ind b}} → Belongs (more ind nbel) (more b bool)<br> left : ∀{ind bl br} → {{is : Belongs ind bl}} → Belongs (left ind) (twoPaths bl br)<br> right : ∀{ind bl br} → {{is : Belongs ind br}} → Belongs (right ind) (twoPaths bl br)<br> inf : ∀{ind∞ bob∞} → {{is∞ : Belongs∞ ind∞ bob∞}} → Belongs (inf ind∞) (inf bob∞)<br><br> record Belongs∞ {i : Size} (ind∞ : Index∞ i) (bob∞ : Bob∞ i) : Set where<br> coinductive<br> field<br> belongs : {j : Size< i} → Belongs (index ind∞) (bob bob∞)<br><br>open Belongs∞<br><br>mutual<br><br> b : ∀{i} → Bob i<br> b = more (inf b∞) true<br><br> b∞ : ∀{i} → Bob∞ i<br> bob b∞ = b<br><br><br>mutual<br><br> ind : ∀{i} → Index i<br> ind = more (inf ind∞) bel<br><br> ind∞ : ∀{i} → Index∞ i<br> index ind∞ = ind<br><br><br>data R : Set where<br> r : R<br><br>test : {{bl : Belongs ind b}} → R<br>test = r<br><br><br>-- I want instance resolution to create this datatype.<br><br>mutual<br><br> bl : {i : Size} → Belongs {i} ind b<br> bl = moreBel {{inf {{bl∞}}}}<br><br> bl∞ : {i : Size} → Belongs∞ {i} ind∞ b∞<br> belongs bl∞ = bl <br><br><br>f : R<br>f = test<br><br></div>
<br></div></div>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>