/home/laney/.irssi/irclogs/Freenode/#agda.log-20170302

--- Day changed Wed Mar 01 2017
dgprattI01/03 01:35
dgprattI hate it when I mean to <shift> and instead <enter>01/03 01:35
dgprattI'm trying to understand "typing judgements" and getting hung up on a basic thing: given something like Γ,x:τ1 ⊢ e:τ2 how do I interpret the comma? what is its precedence, so to speak?01/03 01:37
jonsterlingdgpratt: good question :) The bracketing is "(G, (x:t1)) !- (e:t2)"01/03 02:51
jonsterlingThe comma is adding another variable to the context01/03 02:51
Saizanjonsterling: seems like it would be easy to add a printing primitive for debugging though, ask Ulf :)01/03 08:36
jonsterlingSaizan: sweet. I'll ask him if it makes sense to send a PR w/ the feature or something.01/03 12:46
quchenHow can I use ∀ in data definitions? ∀ α is shorthand for { α : _ }, right?01/03 13:11
quchenThis works,   record Semigroup {α : _} {A : Set α} (_⋆_ : A → A → A) : Set α where01/03 13:11
quchenBut this does not,   record Semigroup ∀ α {A : Set α} (_⋆_ : A → A → A) : Set α where 01/03 13:11
quchenAdding parentheses didn’t help either01/03 13:11
dgprattthanks jonsterling01/03 13:16
dgprattdo you think it makes sense, at least in certain contexts, to think of it like pattern matching, a la "x:xs"? I ask because I see that in context "G" by itself is referenced in the conclusion01/03 13:19
rntzquchen: "\forall a" is shorthand for (a : _), not {a : _}. In data definitions, you can omit the \forall if you're on the left-hand-side of the ":"01/03 13:22
quchenHuh, ∀ does not introduce an implicit parameter?01/03 13:22
rntz"forall a" makes an explicit one01/03 13:23
rntz"forall {a}" makes an implicit one01/03 13:23
quchenOooooh!01/03 13:23
quchenI thought the {} were only necessary for multiple arguments01/03 13:23
rntznah, {} means implicit. forall just lets you leave off the type of the parameter.01/03 13:24
rntzand in a data declaration you can do that anyway, so "Transactional memory is most often mentioned in the context of multi-threaded programming, where the reason the system tracks memory access is to prevent corruption. Another kind of transactional memory is the database, SQL or otherwise; one of the main reasons they exist is to provide transactions over data. Transactions are useful in many contexts where 01/03 13:24
rntznot commonly reached for; transactional collections offer a nice compromise between primitive collections and databases, and the world would be a better place if more undo facilities tracked change sets rather than individual changes.01/03 13:24
rntzargleblarg, sorry! I pasted the wrong thing01/03 13:24
quchenThought so ;-)01/03 13:25
rntzso "record Semigroup {a} {A : Set a} (_*_ : A -> A -> A) : Set a where" should work01/03 13:25
quchenAh, I see.01/03 13:25
quchenI thought level polymorphism was a bit tedious to write at first.01/03 13:25
quchenThere’s a lot of sugar and autocompletion going on in Agda it seems.01/03 13:27
quchenrntz: Is there something to be said about »∀ {A B}« in terms of how A and B have to match somehow, e.g. have the same type or at least unify?01/03 13:28
rntzhm. I don't think they do, actually?01/03 13:28
rntzI think forall {A B} is the same as forall {A}{B}01/03 13:28
quchenOh, I can even add multiple parameters to a single forall, such as {A} B {C}? Neat.01/03 13:29
rntzyup01/03 13:29
quchenThanks, that was really helpful :-)01/03 13:29
rntz:)01/03 13:29
quchenCan I somehow shorten this even more?  symm-≡ : ∀ {α} {A : Set α} {x y : A} → x ≡ y → y ≡ x01/03 13:32
quchen{A : Set _} doesn’t seem to work, unfortunately.01/03 13:33
simonnnsomeone should update the topic: https://github.com/agda/agda/issues/2480 ;)01/03 15:21
akrbummer01/03 16:22
akrhttps://gist.github.com/copumpkin/5945905#file-topology-agda-L3401/03 16:22
akrthat doesn't seem quite right?01/03 16:22
akr"Closed set is a set for which there exists a disjoin open set"?01/03 16:23
-!- Irssi: Topic: -: Agda safety: we last proved false on May 2nd 2015.01/03 21:35
-!- ChanServ changed the topic of #agda to: Agda: is it a dependently-typed programming language? Is it a proof-assistant based on intuitionistic type theory? ¯\(°_0)/¯ Dunno, lol. | Wiki: http://bit.ly/7pSJE | Logs: http://agda.orangesquash.org.uk/ | http://news.gmane.org/gmane.comp.lang.agda | Please comment your Agda | Lib: http://bit.ly/RivPPG01/03 21:35

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