xcmw xcmw --- Day changed Tue Jan 23 2018 Does agda have something similar to idris's auto implicit? 23/01 00:39 i want to run the agda auto solver on an implicit argument automatically 23/01 00:54 xcmw: http://agda.readthedocs.io/en/latest/language/implicit-arguments.html 23/01 01:06 xcmw: err… http://agda.readthedocs.io/en/latest/language/instance-arguments.html 23/01 01:06 I don’t know if that’s what you mean 23/01 01:06 if by “auto solver” you mean, you want Agda to run Agsy automatically 23/01 01:06 then I’m afraid we don’t have that 23/01 01:06 the only proof-searchy thing we do have is instance arguments 23/01 01:07 http://agda.readthedocs.io/en/latest/tools/auto.html 23/01 01:07 right, I see Agsy is also called Auto 23/01 01:07 I believe better proof search may be the subject of the upcoming Agda implementors meeting next week 23/01 01:08 wish I were there 23/01 01:08 :( 23/01 01:08 mietek: No instance of type 2 ≤ 2 was found in scope. 23/01 01:10 well, do you have one? 23/01 01:11 Well I was hoping agda could figure it out for me. Idris can do it. 23/01 01:11 are you using https://agda.github.io/agda-stdlib/Data.Nat.Base.html#802 ? 23/01 01:11 for _≤_ 23/01 01:11 I am using Data.Nat 23/01 01:11 unfortunately the stdlib is not quite helpful here 23/01 01:12 the constructors need to be declared instance 23/01 01:12 before you go all in, try just copying the definition 23/01 01:13 > 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 :1:44: error: parse error on input ‘,’ 23/01 12:25 lambdabot: quiet 23/01 12:25 does anyone know why the DISPLAY pragma is limited as above? 23/01 12:26 in particular, the lambda limitation is really annoying 23/01 12:26 because one of the annoying things that Agda does is, it expands lambdas in the environment display 23/01 12:27 BUT NOT IN THE GOAL DISPLAY 23/01 12:27 argh 23/01 12:27 that is, when you do C-C C-, in a hole, the format of the Goal is different from the format of the available lemmas 23/01 12:28 you have to do C-u C-u C-c C-, to get the same expanded format 23/01 12:28 but I would prefer to see the lemmas in contracted format, like the goal… 23/01 12:29 it could be fixable using the DISPLAY pragma, but unfortunately in the most annoying cases, it can’t be, because of the lambda limitation 23/01 12:29 mietek: Thanks it worked 23/01 12:33 xcmw: cool! 23/01 12:33 mietek: 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 Saizan: would it be simpler to fix the goal vs environment display difference? 23/01 12:35 I’m planning to learn emacs properly and start fixing agda-mode 23/01 12:36 because it’s driving me insane 23/01 12:36 then, maybe, 10 years later, I’ll graduate on to fixing Agda itself 23/01 12:37 in the 2.5.3 release, agda-mode stopped inserting parentheses correctly around lambdas 23/01 12:38 now, if you fill a hole with a lambda, you get no parentheses, even when the resulting file doesn’t typecheck 23/01 12:38 but if you explicitly fill a hole with a lambda in parentheses, you get *double parentheses* 23/01 12:38 have you reported these as issues? 23/01 12:38 sorry, not this one yet 23/01 12:39 I sort of assumed everybody sees it 23/01 12:39 because it happens every time… 23/01 12:39 also, 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 hm 23/01 12:40 let’s see if I can make one 23/01 12:41 also, parentheses inserted around lambdas seem fine to me, but i'm using master, not sure about 2.5.3 23/01 12:43 Saizan: 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.png 23/01 12:43 this happens to definitions such as Δ ⊢ Ξ allvalid[ Γ ] = All (\ A → Δ ⊢ A valid[ Γ ]) Ξ 23/01 12:44 I introduced the definition for a reason 23/01 12:47 I would prefer not to see it expanded all the time 23/01 12:47 yeah, 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 I get something horrible 23/01 12:48 _Δ_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 yeah, lots of metas 23/01 12:48 but the type is not reduced there 23/01 12:48 ok. so a small example will be useful? 23/01 12:49 yeah, i think something is happening while the patterns are typechecked 23/01 12:49 Agda 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 No field contains the type of the defined record. 23/01 17:16 apostolis: unless somebody answers first, a minimal example might help 23/01 17:48 apostolis: can you show us the record declaration? i don't think there's any command to ask more about it 23/01 17:49 Did you see the email? 23/01 17:50 https://github.com/xekoukou/AgdaScript/blob/master/AgdaScript2.agda#L42 23/01 17:50 The problem appears in field with name "asf". 23/01 17:51 i guess it's due to the mutual recursion? 23/01 17:51 i.e. the record is indirectly recursive 23/01 17:52 maybe? 23/01 17:52 also, what is the error exactly? does it not allow this definition? 23/01 17:52 Probably, I do not know. If I make the record inductive, everything is ok. 23/01 17:53 "Recursive record ASFunF needs to be declared as either inductive or coinductive" 23/01 17:55 ah, fair enough 23/01 17:55 would be nice if it explained how it is recursive, other errors do that, but i guess chosing inductive will get you what you expect anyway 23/01 17:56 Yes, 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 i think it's just that the error message could be improved 23/01 18:03 Saizan : Ok. 23/01 18:06 this happens when you mutually define a record together with a datatype that takes values of the record type in constructors 23/01 18:21 adding the keyword “inductive” allowed me to progress beyond this error every time 23/01 18:22 I don’t know when would “coinductive” be needed 23/01 18:22 ah. 23/01 18:22 https://github.com/mietek/abel-chapman-extended/blob/master/AbelChapmanExtended/Delay.agda#L17 23/01 18:22 here. 23/01 18:23 Saizan: why don’t we have a codata keyword? 23/01 18:23 I think {AS} was asking about a Pientka paper today, too 23/01 18:23 {AS}: which one was it? 23/01 18:24 mietek: http://www.cs.mcgill.ca/~bpientka/papers/indexed-codata.pdf 23/01 18:24 Saizan: ^^ 23/01 18:24 {AS}: do you have a year for that? 23/01 18:25 It's fairly recent 23/01 18:25 I can check out the date 23/01 18:25 2016 23/01 18:25 nice. I guess I haven’t seen it before 23/01 18:25 mietek : it is possible that this is the case here but I didn't know about this rule. 23/01 18:26 mietek: there is a video https://www.youtube.com/watch?v=0Idla8oYaKM 23/01 18:27 apostolis: well, it’s not really a rule I understand; it’s rather something I’ve observed 23/01 18:27 apostolis: the empirical approach to programming in unfamiliar languages… 23/01 18:27 apostolis: I’d definitely say it’s a deficiency 23/01 18:28 lol , yea I use this approach too. 23/01 18:28 I am really annoyed when I have to 23/01 18:28 I wish it wasn’t necessary to work this way 23/01 18:29 but if the alternative is, read and understand the entirety of Agda source code 23/01 18:29 mietek : 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 agreed 23/01 18:30 I suppose this one is simple to report 23/01 18:30 mietek: In any case, I would think Saizan knows it 23/01 18:32 I was just wondering why Agda did not have it 23/01 18:32 {AS}: I’m also wondering what exactly Agda supports in the way of codata 23/01 18:32 I know we have copatterns 23/01 18:32 and this question about records reminded me that this is the only way I know how to define a codatatype 23/01 18:33 that is, define a record marked as coinductive 23/01 18:33 but there is no codata keyword 23/01 18:33 Using a record with "coinductive" is the canocical way to do it. 23/01 18:35 but that means we cannot have anonymous tupels 23/01 18:35 tuples* 23/01 18:35 or co-sum types? 23/01 18:35 I don’t know what’s the proper nomenclature here 23/01 18:36 I 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 mietek: co-sum types = product types I believe :) 23/01 18:37 {AS}: uh… 23/01 18:37 https://github.com/xekoukou/sparrow/blob/master/agda/LinLogic.agda#L28 23/01 18:37 I copied this pattern from Andreas Abel paper on the delay monad. 23/01 18:38 apostolis: I know; so did I 23/01 18:38 :) 23/01 18:38 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 + B 23/01 18:39 right? 23/01 18:39 I’m searching for my go-to example 23/01 18:39 bear with me 23/01 18:39 OK 23/01 18:39 sorry, I would guess it is A + B -> C 23/01 18:39 Yeah, I flipped all the arrows 23/01 18:40 nevermind :| 23/01 18:40 So, just fixing this: A -> A + B <- B, A -> C <- B, and unique morphism from A + B -> C 23/01 18:40 I have no idea what you’re saying now 23/01 18:41 can you try sentences? :) 23/01 18:41 mietek: I am trying to draw a categorical diagram 23/01 18:41 haha 23/01 18:41 anyway, a co-sum would be like where the arrows are flipped 23/01 18:42 so a product type :) 23/01 18:42 {AS}: https://gist.github.com/mietek/068092bae201e42e65ff51791bbd8a36 23/01 18:42 this is pseudocode 23/01 18:42 mietek: Interesting 23/01 18:42 I would like to be able to write like this 23/01 18:43 mietek: So I think that codata types must have coeliminators, right? 23/01 18:43 whatever you call them 23/01 18:43 we define an inductive datatype by giving its constructors 23/01 18:43 and we define a coinductive codatatype by giving its eliminators 23/01 18:43 mietek: there is work on guarded recursion 23/01 18:43 I don’t think that should be necessary here 23/01 18:44 I think this solves a lot of issues for coinductive types 23/01 18:44 this much has been done in 1993 23/01 18:44 https://github.com/mietek/et-language/blob/master/doc/pdf/splawski-1993.pdf 23/01 18:44 I see 23/01 18:44 if you look on page 5 23/01 18:46 the user types into the system one line 23/01 18:46 codatatype STREAM ‘a = Shd to ‘a & Stl to STREAM ‘a; 23/01 18:46 this is represented in my gist as the codata declaration 23/01 18:46 and the ET/IPL system accepts the definition, responding with automatically-derived iterator, recursor, and computation rules 23/01 18:47 apostolis: you should also look at the Splawski note 23/01 18:49 apostolis: there’s codatatypes for linear logic later 23/01 18:49 mietek : Ok. I would rather start from the problem you are having and see if I can solve it myself. 23/01 20:24 hm? 23/01 20:24 To understand the theory, I need to understand the problem it is solving. 23/01 20:26 I’m not sure what to say 23/01 20:27 I guess my problem is that I would like a language in which I can define codatatypes and work with their elimination rules explicitly 23/01 20:28 or via copatterns 23/01 20:28 being able to only declare coinductive records in Agda seems weird and limiting 23/01 20:28 and I think the work necessary to have such a language has been done 23/01 20:29 I’ve collected materials; https://github.com/mietek/et-language/ 23/01 20:29 including implementations 23/01 20:29 but this particular language is an extension of System F; it’s not dependently typed 23/01 20:29 and it’s not really alive in any sense 23/01 20:29 I’m slowly working my way up the ladder and maybe this year I’ll understand some of it 23/01 20:30 ok. 23/01 20:31 or, enough of it to write my own formalisation 23/01 20:31 and then see what happens next 23/01 20:31 why 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 hm 23/01 20:54 come to think of it, the ET/ILP notation does use & as a separator 23/01 20:55 sorry, I don’t have a clear argument 23/01 20:56