--- Day changed Tue Jan 23 2018
xcmwDoes agda have something similar to idris's auto implicit?23/01 00:39
xcmwi want to run the agda auto solver on an implicit argument automatically23/01 00:54
mietekxcmw: http://agda.readthedocs.io/en/latest/language/implicit-arguments.html23/01 01:06
mietekxcmw: err… http://agda.readthedocs.io/en/latest/language/instance-arguments.html23/01 01:06
mietekI don’t know if that’s what you mean23/01 01:06
mietekif by “auto solver” you mean, you want Agda to run Agsy automatically23/01 01:06
mietekthen I’m afraid we don’t have that23/01 01:06
mietekthe only proof-searchy thing we do have is instance arguments23/01 01:07
mietekhttp://agda.readthedocs.io/en/latest/tools/auto.html23/01 01:07
mietekright, I see Agsy is also called Auto23/01 01:07
mietekI believe better proof search may be the subject of the upcoming Agda implementors meeting next week23/01 01:08
mietekwish I were there23/01 01:08
mietek:(23/01 01:08
xcmwmietek: No instance of type 2 ≤ 2 was found in scope.23/01 01:10
mietekwell, do you have one?23/01 01:11
xcmwWell I was hoping agda could figure it out for me. Idris can do it.23/01 01:11
mietekare you using https://agda.github.io/agda-stdlib/Data.Nat.Base.html#802 ?23/01 01:11
mietekfor _≤_23/01 01:11
xcmwI am using Data.Nat23/01 01:11
mietekunfortunately the stdlib is not quite helpful here23/01 01:12
mietekthe constructors need to be declared `instance`23/01 01:12
mietekbefore you go all in, try just copying the definition 23/01 01:13
mietek> Left-hand sides are restricted to variables, constructors, defined functions or types, and literals. In particular, lambdas are not allowed in left-hand sides.23/01 12:25
lambdabot <hint>:1:44: error: parse error on input ‘,’23/01 12:25
mieteklambdabot: quiet23/01 12:25
mietekdoes anyone know why the DISPLAY pragma is limited as above?23/01 12:26
mietekin particular, the lambda limitation is really annoying23/01 12:26
mietekbecause one of the annoying things that Agda does is, it expands lambdas in the environment display23/01 12:27
mietekBUT NOT IN THE GOAL DISPLAY23/01 12:27
mietekargh23/01 12:27
mietekthat is, when you do C-C C-, in a hole, the format of the Goal is different from the format of the available lemmas23/01 12:28
mietekyou have to do C-u C-u C-c C-, to get the same expanded format23/01 12:28
mietekbut I would prefer to see the lemmas in contracted format, like the goal…23/01 12:29
mietekit could be fixable using the DISPLAY pragma, but unfortunately in the most annoying cases, it can’t be, because of the lambda limitation23/01 12:29
xcmwmietek: Thanks it worked23/01 12:33
mietekxcmw: cool!23/01 12:33
Saizanmietek: it's a limitation of the implementation afaiu, patches welcome! it's actually annoying me too, I would like to rewrite "PathP (\ _ -> A) x y" to "Path {A = A} x y"23/01 12:34
mietekSaizan: would it be simpler to fix the goal vs environment display difference?23/01 12:35
mietekI’m planning to learn emacs properly and start fixing agda-mode23/01 12:36
mietekbecause it’s driving me insane23/01 12:36
mietekthen, maybe, 10 years later, I’ll graduate on to fixing Agda itself23/01 12:37
mietekin the 2.5.3 release, agda-mode stopped inserting parentheses correctly around lambdas23/01 12:38
mieteknow, if you fill a hole with a lambda, you get no parentheses, even when the resulting file doesn’t typecheck23/01 12:38
mietekbut if you explicitly fill a hole with a lambda in parentheses, you get *double parentheses*23/01 12:38
Saizanhave you reported these as issues?23/01 12:38
mieteksorry, not this one yet23/01 12:39
mietekI sort of assumed everybody sees it23/01 12:39
mietekbecause it happens every time…23/01 12:39
Saizanalso, i'm not aware of the environment being handled differently intentionally, the expanded lambdas might just be a side-effect of typechecking, do you have small example showing this?23/01 12:40
mietekhm23/01 12:40
mieteklet’s see if I can make one23/01 12:41
Saizanalso, parentheses inserted around lambdas seem fine to me, but i'm using master, not sure about 2.5.323/01 12:43
comietekSaizan: before I do that, here’s my actual problem case right now https://usercontent.irccloud-cdn.com/file/MqykXOBg/Screen%20Shot%202018-01-23%20at%2012.43.15.png23/01 12:43
mietekthis happens to definitions such as `Δ ⊢ Ξ allvalid[ Γ ] = All (\ A → Δ ⊢ A valid[ Γ ]) Ξ`23/01 12:44
mietekI introduced the definition for a reason23/01 12:47
mietekI would prefer not to see it expanded all the time23/01 12:47
Saizanyeah, that looks like the type of \psi got reduced for some reason, what happens if you ask for C-c C-d mvar ?23/01 12:47
mietekI get something horrible23/01 12:48
mietek_Δ_6428 ξ η i ψ ∋ ⟪ _Ψ_6427 ξ η i ψ ⊫ _A_6426 ξ η i ψ ⟫ → _Δ_6428 ξ η i ψ ⊢ _Ψ_6427 ξ η i ψ allvalid[ _Γ_6429 ξ η i ψ ] → _Δ_6428 ξ η i ψ ⊢ _A_6426 ξ η i ψ valid[ _Γ_6429 ξ η i ψ ]23/01 12:48
Saizanyeah, lots of metas23/01 12:48
Saizanbut the type is not reduced there23/01 12:48
mietekok. so a small example will be useful?23/01 12:49
Saizanyeah, i think something is happening while the patterns are typechecked23/01 12:49
apostolisAgda tells me that a record of mine is recursive, but I cannot find the recursion. Is there a way to get more accurate information than this error?23/01 17:14
apostolisNo field contains the type of the defined record.23/01 17:16
pgiarrussoapostolis: unless somebody answers first, a minimal example might help23/01 17:48
Saizanapostolis: can you show us the record declaration? i don't think there's any command to ask more about it23/01 17:49
apostolisDid you see the email?23/01 17:50
apostolishttps://github.com/xekoukou/AgdaScript/blob/master/AgdaScript2.agda#L4223/01 17:50
apostolisThe problem appears in field with name "asf".23/01 17:51
Saizani guess it's due to the mutual recursion?23/01 17:51
Saizani.e. the record is indirectly recursive23/01 17:52
Saizanmaybe?23/01 17:52
Saizanalso, what is the error exactly? does it not allow this definition?23/01 17:52
apostolisProbably, I do not know. If I make the record inductive, everything is ok.23/01 17:53
apostolis"Recursive record ASFunF needs to be declared as either inductive or coinductive"23/01 17:55
Saizanah, fair enough23/01 17:55
Saizanwould be nice if it explained how it is recursive, other errors do that, but i guess chosing inductive will get you what you expect anyway23/01 17:56
apostolisYes, I was thinking that it was a bug, so maybe I need to report it, but the code is difficult to understand even for me at the moment.23/01 17:57
Saizani think it's just that the error message could be improved23/01 18:03
apostolisSaizan : Ok.23/01 18:06
mietekthis happens when you mutually define a record together with a datatype that takes values of the record type in constructors23/01 18:21
mietekadding the keyword “inductive” allowed me to progress beyond this error every time23/01 18:22
mietekI don’t know when would “coinductive” be needed23/01 18:22
mietekah.23/01 18:22
mietekhttps://github.com/mietek/abel-chapman-extended/blob/master/AbelChapmanExtended/Delay.agda#L1723/01 18:22
mietekhere.23/01 18:23
mietekSaizan: why don’t we have a `codata` keyword?23/01 18:23
mietekI think {AS} was asking about a Pientka paper today, too23/01 18:23
mietek{AS}: which one was it?23/01 18:24
{AS}mietek: http://www.cs.mcgill.ca/~bpientka/papers/indexed-codata.pdf23/01 18:24
mietekSaizan: ^^23/01 18:24
mietek{AS}: do you have a year for that?23/01 18:25
{AS}It's fairly recent23/01 18:25
{AS}I can check out the date23/01 18:25
{AS}201623/01 18:25
mieteknice. I guess I haven’t seen it before23/01 18:25
apostolismietek : it is possible that this is the case here but I didn't know about this rule.23/01 18:26
{AS}mietek: there is a video https://www.youtube.com/watch?v=0Idla8oYaKM23/01 18:27
mietekapostolis: well, it’s not really a rule I understand; it’s rather something I’ve observed 23/01 18:27
mietekapostolis: the empirical approach to programming in unfamiliar languages…23/01 18:27
mietekapostolis: I’d definitely say it’s a deficiency23/01 18:28
apostolislol , yea I use this approach too.23/01 18:28
mietekI am really annoyed when I have to 23/01 18:28
mietekI wish it wasn’t necessary to work this way23/01 18:29
mietekbut if the alternative is, read and understand the entirety of Agda source code23/01 18:29
apostolismietek : Agda has very few such cases. That is why I like it and that is why I was going to report this as a bug.23/01 18:29
mietekagreed23/01 18:30
mietekI suppose this one is simple to report23/01 18:30
{AS}mietek: In any case, I would think Saizan knows it23/01 18:32
{AS}I was just wondering why Agda did not have it23/01 18:32
mietek{AS}: I’m also wondering what exactly Agda supports in the way of codata23/01 18:32
mietekI know we have copatterns23/01 18:32
mietekand this question about records reminded me that this is the only way I know how to define a codatatype23/01 18:33
mietekthat is, define a record marked as `coinductive`23/01 18:33
mietekbut there is no `codata` keyword23/01 18:33
apostolisUsing a record with "coinductive" is the canocical way to do it.23/01 18:35
mietekbut that means we cannot have anonymous tupels23/01 18:35
mietektuples*23/01 18:35
mietekor co-sum types?23/01 18:35
mietekI don’t know what’s the proper nomenclature here23/01 18:36
apostolisI got to go but have a look at my definition here : The inductive parts are defined in a data type and the rest in a coinductive record.23/01 18:37
{AS}mietek: co-sum types = product types I believe :)23/01 18:37
mietek{AS}: uh…23/01 18:37
apostolishttps://github.com/xekoukou/sparrow/blob/master/agda/LinLogic.agda#L2823/01 18:37
apostolisI copied this pattern from Andreas Abel paper on the delay monad.23/01 18:38
mietekapostolis: I know; so did I23/01 18:38
apostolis:)23/01 18:38
{AS}mietek: a sum type is one which satisfies the following A <- A + B -> B, and for each A <- C -> B we have a unique morphism C -> A + B23/01 18:39
{AS}right?23/01 18:39
mietekI’m searching for my go-to example23/01 18:39
mietekbear with me23/01 18:39
{AS}OK23/01 18:39
{AS}sorry, I would guess it is A + B -> C23/01 18:39
{AS}Yeah, I flipped all the arrows23/01 18:40
{AS}nevermind :|23/01 18:40
{AS}So, just fixing this: A -> A + B <- B, A -> C <- B, and unique morphism from A + B -> C23/01 18:40
mietekI have no idea what you’re saying now23/01 18:41
mietekcan you try sentences? :)23/01 18:41
{AS}mietek: I am trying to draw a categorical diagram23/01 18:41
mietekhaha23/01 18:41
{AS}anyway, a co-sum would be like where the arrows are flipped23/01 18:42
{AS}so a product type :)23/01 18:42
mietek{AS}: https://gist.github.com/mietek/068092bae201e42e65ff51791bbd8a3623/01 18:42
mietekthis is pseudocode23/01 18:42
{AS}mietek: Interesting23/01 18:42
mietekI would like to be able to write like this23/01 18:43
{AS}mietek: So I think that codata types must have coeliminators, right?23/01 18:43
mietekwhatever you call them23/01 18:43
mietekwe define an inductive datatype by giving its constructors23/01 18:43
mietekand we define a coinductive codatatype by giving its eliminators23/01 18:43
{AS}mietek: there is work on guarded recursion 23/01 18:43
mietekI don’t think that should be necessary here23/01 18:44
{AS}I think this solves a lot of issues for coinductive types23/01 18:44
mietekthis much has been done in 199323/01 18:44
mietekhttps://github.com/mietek/et-language/blob/master/doc/pdf/splawski-1993.pdf23/01 18:44
{AS}I see23/01 18:44
mietekif you look on page 523/01 18:46
mietekthe user types into the system one line23/01 18:46
mietek`codatatype STREAM ‘a = Shd to ‘a & Stl to STREAM ‘a;`23/01 18:46
mietekthis is represented in my gist as the `codata` declaration23/01 18:46
mietekand the ET/IPL system accepts the definition, responding with automatically-derived iterator, recursor, and computation rules23/01 18:47
mietekapostolis: you should also look at the Splawski note23/01 18:49
mietekapostolis: there’s codatatypes for linear logic later23/01 18:49
apostolismietek : Ok. I would rather start from the problem you are having and see if I can solve it myself.23/01 20:24
mietekhm?23/01 20:24
apostolisTo understand the theory, I need to understand the problem it is solving.23/01 20:26
mietekI’m not sure what to say23/01 20:27
mietekI guess my problem is that I would like a language in which I can define codatatypes and work with their elimination rules explicitly23/01 20:28
mietekor via copatterns23/01 20:28
mietekbeing able to only declare coinductive records in Agda seems weird and limiting23/01 20:28
mietekand I think the work necessary to have such a language has been done23/01 20:29
mietekI’ve collected materials; https://github.com/mietek/et-language/23/01 20:29
mietekincluding implementations23/01 20:29
mietekbut this particular language is an extension of System F; it’s not dependently typed23/01 20:29
mietekand it’s not really alive in any sense23/01 20:29
mietekI’m slowly working my way up the ladder and maybe this year I’ll understand some of it23/01 20:30
apostolisok.23/01 20:31
mietekor, enough of it to write my own formalisation23/01 20:31
mietekand then see what happens next23/01 20:31
tomjackwhy are coinductive records weird and limiting? they seem sensible and not limiting given the "codata is defined by eliminators" intuition. e.g. your codata Stream makes no sense to me unless I think about it like a record...23/01 20:43
mietekhm23/01 20:54
mietekcome to think of it, the ET/ILP notation does use `&` as a separator 23/01 20:55
mieteksorry, I don’t have a clear argument23/01 20:56

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