--- Day changed Fri Feb 10 2017
ocharlesHello, having a bit of an odd problem getting Agda to agree that two types are equal10/02 10:08
ocharlesTried to explain it all here https://www.irccloud.com/pastebin/1KpKMytX/10/02 10:08
Saizan_ocharles: which agda version are you using?10/02 12:47
ocharles2.5.210/02 12:47
ocharlesIt seems that things change depending on whether or not my program has any holes. If I comment out "strings-are-quoted", I the normalised form of "parse (display (render-pretty 80 (char '"' <> text s <> char '"')))" is (just (lit (string []))). but if there are holes, then it gets stuck and doesn't normalise10/02 12:48
ocharlesI'm also writing this up as a StackOverflow question atm with a bit more context10/02 12:48
Saizan_If you give enough sources to be able to load the file that's helpful10/02 12:50
ocharlesYep, I'll share a repository10/02 12:51
ocharlesit needs Ulf's prelude10/02 12:51
{AS}ocharles: if you try to evaluate parse (display (render-pretty (fromNat 80) (char '\"' <> text [] <> char '\"')))10/02 12:54
{AS}what do you get?10/02 12:54
{AS}I mean normalize in agda10/02 12:54
ocharles{AS} with agda-compute-normalised-maybe-toplevel?10/02 12:54
{AS}Yeah10/02 12:55
ocharlesit depends on whether pretty-lit is in scope with holes or not. Just about to post my question with source code10/02 12:55
{AS}ocharles: Ah yeah10/02 12:56
{AS}If your function you are trying to prove things about have holes, I don't think it will work10/02 12:56
ocharleshttp://stackoverflow.com/questions/42159948/agda-compute-normalised-maybe-toplevel-shows-the-correct-type-yet-refl-isnt question and link to source there10/02 12:56
{AS}ocharles: you have to write the functions without holes before you do proofs about them10/02 12:57
{AS}I don't think Agda has a sound theory to do proofs on functions with holes10/02 12:57
ocharlesok, but then filling the hole in should be enough. but I guess maybe the problem is that the second pattern match has a hole which also needs to be filled10/02 12:58
{AS}Oh wait, I misundersood10/02 12:58
{AS}what happens if you just fill the hole with refl?10/02 12:59
{AS}you get the same error?10/02 12:59
ocharlessee the bottom of my SO question -Agda still rejects it10/02 12:59
ocharlesit doesn't seem to compute parse ... at all10/02 12:59
{AS}yeah10/02 13:00
{AS}ocharles: if you try to normalize the type10/02 13:00
{AS}while looking at the hole, what do you get?10/02 13:01
ocharlesit doesn't change/normalise - it's the same as what I put in10/02 13:01
ocharlesit's only when I comment out that whole function that it computes10/02 13:02
{AS}ocharles: yeah, so this means that you are not reducing things10/02 13:02
{AS}ocharles: oh, render-pretty is non-terminating10/02 13:02
{AS}that is your issue10/02 13:02
ocharlesohhh10/02 13:03
ocharlesso even though it does terminate in this case, agda doesn't even try?10/02 13:03
{AS}No10/02 13:03
{AS}you can rewrite it to use fuel, if you want to reason about it10/02 13:03
{AS}why is it non-terminating anyway?10/02 13:03
ocharlesIt is terminating, but agda seems to think it isn't10/02 13:04
ocharlesline, union and nest all cause problems10/02 13:04
ocharlesI'm surprised about the line case, union and nest I can see might be a bit more problematic10/02 13:05
ocharlesthis is just a 1-1 rewrite of text-wlpprint, basically10/02 13:05
{AS}ocharles: you could just use *erhm* {-# TERMINATING #-}10/02 13:05
{AS}This will assert termination10/02 13:06
ocharlesoh, I didn't know that was even a thing10/02 13:06
ocharles:)10/02 13:06
{AS}it's a bit bad10/02 13:06
ocharleswoohoo, it works!10/02 13:06
{AS}but it allows you to deal with termination later10/02 13:06
ocharlesawesome10/02 13:06
{AS}cool :)10/02 13:06
ocharlesI'm sure these structures I'm working with will be horrific to actually write proofs with, but at least I can carry on now10/02 13:07
{AS}ocharles: have you seen parsing with derivatives?10/02 13:08
ocharlesnope, I've not heard of that10/02 13:08
{AS}ocharles: http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.pdf10/02 13:09
ocharlesthank you!10/02 13:09
{AS}np10/02 13:09
ocharlesthis is fascinating10/02 13:24
Saizan_what's weird is that it normalizes in some contexts and in others it doesn't10/02 13:26
Saizan_also, you can prove stuff reasonably well about functions that still have holes in them10/02 13:26
mietekIf you use the right logic… ;)10/02 15:03
SuprDewdwhere can I find information about the inductive/coninductive annotations in record types?10/02 15:09
SuprDewdhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#recursive10/02 15:09
SuprDewdthis is what I found, but it doesn't give an explanation of why ... these things10/02 15:10
{AS}SuprDewd: you just need to add inductive or coinductive in the record namespace10/02 15:10
SuprDewdyeah, I got it working10/02 15:12
SuprDewdbut I just wanted a better understanding of why this works10/02 15:12
SuprDewdand why this isn't the default10/02 15:13
mietekRead the source, Dewd10/02 16:59
mietekSuprDewd: maybe there’s something in http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Publications ?10/02 17:00
pgiarrussoSuprDewd: there was a ticket about hyper-experimental status of inductive records10/02 17:13
pgiarrussoSuprDewd: “You're only allowed to mark a recursive record as inductive if you are Thorsten Altenkirch.” — Ulf Norell: https://github.com/agda/agda/issues/2197#issuecomment-24820325210/02 17:14
mietekOh?10/02 17:14
pgiarrussowhile that bug was fixed, I still got out of that (a) a big laugh and (b) the idea they’re really advanced10/02 17:15
mietek:D10/02 17:16
mietekWait… so what possible record annotations are there?10/02 17:16
mietekhaaa... I’ve been using inductive records in my old formalisation of ILP10/02 17:17
mietekThat worked out 10/02 17:17
pgiarrussoQuestion: for me records are easy, for everything else there’s Mastercard ^H^H datatypes10/02 17:17
pgiarrussoso why inductive records?10/02 17:17
mietekExplicit names for fields10/02 17:18
mietekhttps://mietek.github.io/hilbert-gentzen/html/BasicILP.Syntax.DyadicGentzen.html10/02 17:18
mietekThe entire thing is insanely mutually-recursive10/02 17:18
mietekOr inductive?10/02 17:18
mietekWho knows.10/02 17:18
mietekI think I know a better way now, but I haven’t finished it yet.10/02 17:19
SuprDewdmietek: pgiarrusso: thanks for the links!10/02 18:02
SuprDewda bit unfortunate that I am not Thorsten Altenkirch, though :(10/02 18:03
pgiarrussoWhat I think I learned today: definitional equalities are only in scope in lines *after* they’re declared (somewhat obvious) *even in mutually recursive blocks*10/02 19:58
pgiarrussobut refining holes doesn’t account for that10/02 19:58
pgiarrussoso if I declare a type T1 : Set, use it in a function f, and then define T1 = … f …, the definition of T1 doesn’t reduce in f10/02 19:59
pgiarrusso(so I can predeclare f and move the definition of T1 before f’s body)10/02 20:00
jonsterlingmietek: BTW, all these different variations and developments are very helpful! Combined, one could almost imagine it comprising a thesis.10/02 20:28
pgiarrussomietek: Achievement “jonsterling approved” unlocked :-)10/02 20:50
comietekjonsterling: thanks. There's still much left to do. :)10/02 21:36
SuprDewdwould be nice if we could write `record { f = \lambda x \-> x+1 }` as `record { f x = x+1 }`10/02 21:42

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