--- Day changed Wed Mar 08 2017
subttlehi, is there any way/namespace trick to access functions defined in the "where" block of library code?08/03 02:59
subttleI would like to use https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Properties.agda#L48808/03 02:59
subttleor are those essentailly private?08/03 03:02
subttleessentially*08/03 03:29
subttleAlso, 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
subttlehttps://github.com/subttle/regular-expressions/08/03 03:49
subttleStructural.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 on08/03 03:51
subttleGah, sorry it's public now08/03 04:13
mudriQuick 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
Calemudri: 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
mudriCale: yeah, maybe I should try that. Thanks.08/03 10:49
gallaismudri: https://github.com/gallais/agdARGS 0:-)08/03 11:29
gallaisBut if you just want bindings to getArgs, this is basically what to do: https://github.com/gallais/agdARGS/tree/master/agdARGS/System/Environment08/03 11:31
mudrigallais: ooh, thanks. What's the best way of using this in my project? Copy the source code?08/03 11:31
gallaisIf it's just the bindings to getArgs, yeah that'll be easiest08/03 11:32
mudriI'm not doing much, so yeah, that should be enough.08/03 11:34
gallaissubttle: I'm not sure why you'd want an ordering on regular expressions. 08/03 11:51
Calegallais: 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
gallaisCale: it's not the case here though08/03 13:40
subttlegallais: if you see page 5 here http://www21.in.tum.de/~krauss/papers/rexp.pdf08/03 15:03
subttlefor the algebraic union implementation it helps to have a total ordering08/03 15:04
subttlemy Haskell implementation just used "deriving Ord" but for this Agda implementation I defined it all manually08/03 15:06
subttleCale: I'm working my way up to that :D08/03 15:06
subttleThe 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 ⨁ operators08/03 15:09
subttlefor 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
subttleso now I'm working on an implementation that uses a foldr₁ over a sorted-unique list, 08/03 15:25
subttlesomething like08/03 15:25
subttlefoldr₁ (λ x acc → if atomic x then (x ∣ acc) else (x ⨁ acc))08/03 15:26
subttlefoldr₁ (λ x acc → if atomic x then (x ∣ acc) else (x ⨁ acc))08/03 15:26
subttlebut then that means I have to convince the termination checker that my recursion is well founded08/03 15:26
gallaisThe paper states that (⨁) is supposed to act on already normalised subterms. So I guess it's only supposed to be idempotent on these08/03 15:34
gallaisAnyway, 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.pdf08/03 15:36
subttlegallais: hmm, I get a 40408/03 15:36
gallaisargh, it seems to have moved: http://web.student.chalmers.se/~bassel/regex_agda/report.pdf08/03 15:38
subttlewow, nice, thanks!08/03 15:39
subttlecool, yeah DFAs were next on my TODO list08/03 15:39
akr[m]How do I define the colist of all natural numbers?08/03 15:55
subttleakr[m]: iterate suc zero08/03 15:57
subttlewhich is actually a Stream ℕ08/03 15:58
akr[m]hmm, interesting08/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 typecheck08/03 16:00
akr[m]the flats and sharps are magical08/03 16:01
akr[m]if this typechecks, why doesn't this: ℕ's = 0 ∷ ♯ (map suc ℕ's)08/03 16:03
rntzhm. imagine if you defined map to take the tail of the stream it was handed08/03 16:04
rntzthen that definition wouldn't be productive08/03 16:04
rntzso 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 B08/03 16:04
rntzyeah, 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 say08/03 16:05
rntzI don't really understand how flats and sharps work, though08/03 16:06
akr[m]me neither :(08/03 16:06
rntzso I can't explain why your first example, `iterate f z = ...`, typechecks08/03 16:06
akr[m]well, thanks anyway08/03 16:09
subttleakr[m]: when your goal is ∞ (Colist A) use # to make the goal Colist A08/03 16:14
akr[m]well, sure, I can see that from the types :)08/03 16:14
subttle:D08/03 16:14
akr[m]this is what I have right now https://gist.github.com/osense/3af9771b534535c555e876792d9f230608/03 16:15
subttlecool08/03 16:16
akr[m]tips on how to prove odd' are welcome :P08/03 16:16
subttlehmm, that looks like fun... I have HW due today but maybe I can give it a whirl tonight08/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
byorgeyakr[m]: you can't prove that two functions are propositionally equal without assuming function extensionality08/03 16:48
byorgeyeven then, I'm not sure whether you can prove that two Colists are propositionally equal.08/03 16:49
byorgeyBut 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
byorgeythen you should be able to prove that for any colist x,  tail (even x) is bisimilar to odd x08/03 16:50
byorgeyincidentally, 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
byorgeyI think you want even . tail = odd08/03 16:51
serendependybyorgey: 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 channel08/03 16:55
lpaste_gallais pasted “AllNat using Coinductive Sized Types” at http://lpaste.net/35331808/03 17:00
gallaisakr[m]: ^ that's why it's better to use the new style of codata08/03 17:00
gallaisIt's still not perfect but it's better than the musical notations08/03 17:01

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