--- Day changed Tue Jan 09 2018
lfishhello, what does the `Agda2 Highlight Catchall Clause Face` signal in the emacs mode?09/01 18:24
lfishhttp://lpaste.net/361506 I'm getting it here09/01 18:31
m0rphismHi, is there a way to specify the fixity of record parameters? Consider e.g. `data Group (G : Set) (_*_ : G -> G -> G) ...`. Is there a way to specify the fixity of _*_ inside the scope of the `data` definition?09/01 18:35
m0rphismInserting `infixl 5 _*_` above or inside the `data` definition, seems to be not allowed.09/01 18:38
m0rphism(because of scoping issues)09/01 18:38
trikl[m]I was wondering about that too09/01 19:01
pgiarrussolfish: it’s described as “white smoke” highlight, and you can often ignore it. It highlights equations that are not used as reduction rules when normalizing terms09/01 19:06
pgiarrussom0rphism: what about moving params into an anonymous module? `module _ (G : Set) (_*_ : G -> G -> G) where\n data Group : Set where`09/01 19:08
pgiarrusso(`s/\n/new line/`)09/01 19:08
pgiarrussoafter this rewrite you might be able to write `infixl` inside the module09/01 19:08
pgiarrusso(beware my snippet omits the needed indentation for the module body)09/01 19:09
pgiarrussothe declared `Group` should be the same09/01 19:09
pgiarrussom0rphism: ^^09/01 19:09
m0rphismpgiarrusso: thanks, I've just found this github issue: https://github.com/agda/agda/issues/123509/01 19:10
pgiarrussolfish: see the “Reduction behavior” section under http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching for details — it doesn’t mention the highlight because it was added later09/01 19:10
m0rphismSo it seems to be possible that way, but it requires a slight workaround09/01 19:10
pgiarrussom0rphism: oh thanks, didn’t know09/01 19:12
m0rphismpgiarrusso: I guess in this simple case I'll avoid the boilerplate, and just add parentheses to disambiguate terms containing both _*_ and _^{-1}09/01 19:12
m0rphismbut thanks for pointing me to the module approach; good to know for other cases.09/01 19:13
pgiarrusso:-)09/01 19:13
m0rphismagda is the perfect language for procrastinating with syntax and typography :>09/01 19:14
m0rphismjust some more LaTeX support would be nice: I envision tikz diagrams as variable names ;-)09/01 19:19
m0rphismbut joking aside, I think I like Agda's syntax more than the syntax of any other programming language I have encountered yet.09/01 19:21
m0rphismI think this is especially due to mixfix operators and the choice of lexical rules, i.e. strict requirements on whitespace, but a huge alphabet for identifiers09/01 19:24
mietekm0rphism: “tikz diagrams as variable names”09/01 19:30
mietek<309/01 19:30
m0rphismmietek: <309/01 19:49
m0rphismas long as we don't arrive at youtube identifiers, we should be fine ;)09/01 19:50
m0rphismI'm having another problem: I'm trying to show that the integers from `Data.Integer` are a group, but the type `Group _+_ (Z.pos 0) -_` yields a parser error - I think because the parser is confused about whether `-_` is the postfix-operator or an operator section of `_-_`. The pastebin of the minimal example and error is here: https://pastebin.com/1ALUDQA309/01 20:10
m0rphism/s/postfix/prefix/09/01 20:13
m0rphismyep, it's definetly because of an ambiguity with `-_`, if I import `-_` renamed to `~_` it parses correctly.09/01 20:16
m0rphism...I could just rename `-_` to be a unicode `-_`...09/01 20:22
* m0rphism slaps himself on the wrist.09/01 20:22
m0rphismohh, I guess the whole was the problem, is type checking interleaved with parsing? I've started replacing the `?` with a `record` expression, and now it parses but has unresolved existentials. I guess completely filling the holes will resolve them.09/01 20:44
m0rphisms/whole/hole/09/01 20:44
pgiarrussom0rphism: I’m no expert but I think `infix` rules and maybe `mixfix` desugaring are applied *after* parsing proper and during name resolution/typechecking (not sure which) — but not sure09/01 21:26
pgiarrussom0rphism: the error in your parse mentions *scope checking*, which is the technical term Agda uses for name resolution09/01 21:27
pgiarrussoit had even figured the correct possible alternatives, and Agda’s scope-checking can be type-directed09/01 21:28
pgiarrussothat’s necessary, for instance, when you overload constructor names, so that `zero` can mean one of 10 different things, and disambiguation is done based on the expected type09/01 21:29
pgiarrusso(but somebody here has probably read the right papers, I didn’t even read the one on mixfix)09/01 21:29
pgiarrussom0rphism: TL;DR. my answer is “yes” with a “well actually”09/01 21:31
m0rphismpgiarrusso: Interesting, thanks. I guess this means even more mixfix-expressions become unambiguous as type information can be used to discard impossible parse trees.09/01 21:36
m0rphismI guess this also happened in my example, where filling the hole provided enough context for disambiguating `-_`09/01 21:40
pgiarrussom0rphism: yep, that’s what I read from the message you posted (and similar experiences)09/01 22:33

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