--- Day changed Wed Mar 08 2017 | ||

subttle | hi, is there any way/namespace trick to access functions defined in the "where" block of library code? | 08/03 02:59 |
---|---|---|

subttle | I would like to use https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Properties.agda#L488 | 08/03 02:59 |

subttle | or are those essentailly private? | 08/03 03:02 |

subttle | essentially* | 08/03 03:29 |

subttle | Also, I have some Agda code I'm working on for Regular Expressions which is essentially my first Agda project (still very much a work-in-progress) but if anyone has the time to give me any feedback, it would be greatly appreciated. Thanks! | 08/03 03:49 |

subttle | https://github.com/subttle/regular-expressions/ | 08/03 03:49 |

subttle | Structural.agda is essentially complete but could use some polish, I'm still working on Algebraic.agda because my Haskell version which I'm porting to Agda uses unique sorted lists which I'll need to spend some time working on | 08/03 03:51 |

subttle | Gah, sorry it's public now | 08/03 04:13 |

mudri | Quick thing: is it possible to read command line arguments in an Agda program? I don't see anything for it in stdlib. | 08/03 10:43 |

Cale | mudri: Looking at IO.Primitive's code makes me wonder if you could just import Haskell's getArgs and use that somehow via pragma magic. | 08/03 10:48 |

mudri | Cale: yeah, maybe I should try that. Thanks. | 08/03 10:49 |

gallais | mudri: https://github.com/gallais/agdARGS 0:-) | 08/03 11:29 |

gallais | But if you just want bindings to getArgs, this is basically what to do: https://github.com/gallais/agdARGS/tree/master/agdARGS/System/Environment | 08/03 11:31 |

mudri | gallais: ooh, thanks. What's the best way of using this in my project? Copy the source code? | 08/03 11:31 |

gallais | If it's just the bindings to getArgs, yeah that'll be easiest | 08/03 11:32 |

mudri | I'm not doing much, so yeah, that should be enough. | 08/03 11:34 |

gallais | subttle: I'm not sure why you'd want an ordering on regular expressions. | 08/03 11:51 |

Cale | gallais: I can imagine a decent preorder on them :) | 08/03 12:47 |

Cale | (specifically, r <= s whenever L_r ⊆ L_s) | 08/03 12:51 |

gallais | Cale: it's not the case here though | 08/03 13:40 |

subttle | gallais: if you see page 5 here http://www21.in.tum.de/~krauss/papers/rexp.pdf | 08/03 15:03 |

subttle | for the algebraic union implementation it helps to have a total ordering | 08/03 15:04 |

subttle | my Haskell implementation just used "deriving Ord" but for this Agda implementation I defined it all manually | 08/03 15:06 |

subttle | Cale: I'm working my way up to that :D | 08/03 15:06 |

subttle | The union implementation in that paper is very similar to the one I used in Haskell but I'm writing a much different implementation for the Agda version because that one actually messes up if anyone intermixes the | and ⨁ operators | 08/03 15:09 |

subttle | for example specifically, (1 ∣ 0) ⨁ (1 ∣ 0) outputs (0 ∣ (1 ∣ 0)), which I realized was why I couldn't prove idempotence for ⨁ | 08/03 15:19 |

subttle | so now I'm working on an implementation that uses a foldr₁ over a sorted-unique list, | 08/03 15:25 |

subttle | something like | 08/03 15:25 |

subttle | foldr₁ (λ x acc → if atomic x then (x ∣ acc) else (x ⨁ acc)) | 08/03 15:26 |

subttle | foldr₁ (λ x acc → if atomic x then (x ∣ acc) else (x ⨁ acc)) | 08/03 15:26 |

subttle | but then that means I have to convince the termination checker that my recursion is well founded | 08/03 15:26 |

gallais | The paper states that (⨁) is supposed to act on already normalised subterms. So I guess it's only supposed to be idempotent on these | 08/03 15:34 |

gallais | Anyway, if you want a nice Agda treatment of a very similar approach, this report is nice: http://www.cse.chalmers.se/~bassel/regex_agda/report.pdf | 08/03 15:36 |

subttle | gallais: hmm, I get a 404 | 08/03 15:36 |

gallais | argh, it seems to have moved: http://web.student.chalmers.se/~bassel/regex_agda/report.pdf | 08/03 15:38 |

subttle | wow, nice, thanks! | 08/03 15:39 |

subttle | cool, yeah DFAs were next on my TODO list | 08/03 15:39 |

akr[m] | How do I define the colist of all natural numbers? | 08/03 15:55 |

subttle | akr[m]: iterate suc zero | 08/03 15:57 |

subttle | which is actually a Stream ℕ | 08/03 15:58 |

akr[m] | hmm, interesting | 08/03 16:00 |

akr[m] | iterate f z = z ∷ (♯ (iterate f (f z))) | 08/03 16:00 |

akr[m] | I didn't think this would typecheck | 08/03 16:00 |

akr[m] | the flats and sharps are magical | 08/03 16:01 |

akr[m] | if this typechecks, why doesn't this: ℕ's = 0 ∷ ♯ (map suc ℕ's) | 08/03 16:03 |

rntz | hm. imagine if you defined map to take the tail of the stream it was handed | 08/03 16:04 |

rntz | then that definition wouldn't be productive | 08/03 16:04 |

rntz | so maybe agda doesn't have enough information to know that map doesn't do that? what's the type of map? | 08/03 16:04 |

akr[m] | map : {A B : Set} → (A → B) → Colist A → Colist B | 08/03 16:04 |

rntz | yeah, if map took the tail of that (Colist A) before it mapped, then it would still have that type, I think. so I think there's the reason that can't typecheck. | 08/03 16:05 |

akr[m] | so I guess it must be as you say | 08/03 16:05 |

rntz | I don't really understand how flats and sharps work, though | 08/03 16:06 |

akr[m] | me neither :( | 08/03 16:06 |

rntz | so I can't explain why your first example, `iterate f z = ...`, typechecks | 08/03 16:06 |

akr[m] | well, thanks anyway | 08/03 16:09 |

subttle | akr[m]: when your goal is ∞ (Colist A) use # to make the goal Colist A | 08/03 16:14 |

akr[m] | well, sure, I can see that from the types :) | 08/03 16:14 |

subttle | :D | 08/03 16:14 |

akr[m] | this is what I have right now https://gist.github.com/osense/3af9771b534535c555e876792d9f2306 | 08/03 16:15 |

subttle | cool | 08/03 16:16 |

akr[m] | tips on how to prove odd' are welcome :P | 08/03 16:16 |

subttle | hmm, that looks like fun... I have HW due today but maybe I can give it a whirl tonight | 08/03 16:20 |

akr[m] | the goal printing is pretty bad :( | 08/03 16:30 |

akr[m] | Goal: (x' ∷ .Coalgebra.♯-2 xs x' xs' x) ≡ (even (x' ∷ xs') | ♭ xs') | 08/03 16:30 |

byorgey | akr[m]: you can't prove that two functions are propositionally equal without assuming function extensionality | 08/03 16:48 |

byorgey | even then, I'm not sure whether you can prove that two Colists are propositionally equal. | 08/03 16:49 |

byorgey | But you could certainly define a (coinductive) bisimulation relation between Colists, i.e. two colists are bisimilar if the heads are equal and the tails are bisimilar. | 08/03 16:49 |

byorgey | then you should be able to prove that for any colist x, tail (even x) is bisimilar to odd x | 08/03 16:50 |

byorgey | incidentally, you have even = odd . tail but I don't think that's true, the head of the colist is in 'even' but not in 'odd . tail' | 08/03 16:51 |

byorgey | I think you want even . tail = odd | 08/03 16:51 |

serendependy | byorgey: From the goal it looks like akr[m] is trying to prove that the results are equal, not that the functions are. But I may have missed some context from before I joined the channel | 08/03 16:55 |

lpaste_ | gallais pasted “AllNat using Coinductive Sized Types” at http://lpaste.net/353318 | 08/03 17:00 |

gallais | akr[m]: ^ that's why it's better to use the new style of codata | 08/03 17:00 |

gallais | It's still not perfect but it's better than the musical notations | 08/03 17:01 |

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!