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

--- Day changed Sun Aug 06 2017
mietekit’s fresh06/08 00:03
dolioI guess the 'scalar multiplication' part isn't very new, because lots of modal type theories already had things like that.06/08 00:11
dolioBut recognizing that you can do linearity stuff via pointwise addition is cool.06/08 00:12
Saizan_dolio: yep06/08 07:55
Saizan_dolio: what i don't like is that the fancier pi types don't satisfy any fancier theorems, e.g. (x :0 A) -> B is not provably constant, but i guess it doesn't matter for compilation-like applications06/08 07:56
dolioSaizan_: Right.06/08 16:12
dolioI wonder if that can be added, though.06/08 16:13
dolioI didn't read all of the Atkey paper yet, but the McBride one didn't even have equality.06/08 16:14
carterdolio: there's a follow up?!?06/08 18:53
carterIn the loosely inspired sibling of that work I'm using a lattice rather than arithmetic06/08 18:53
carterSaizan_: dolio thanks for mentioning this paper. Gonna check it out after I wake up soon06/08 18:55
apostolisHas anyone else been having problems with accessing the mailing list archives?06/08 18:57
raphaelssapostolis: I wasn't able to access it yesterday (or maybe earlier today)06/08 18:59
apostolisraphaelss : strange :\06/08 19:00
gallaisapostolis: mirror for the ml: http://agda.chalmers.narkive.com/06/08 19:10
--- Log closed Sun Aug 06 20:00:19 2017
--- Log opened Sun Aug 06 20:00:27 2017
-!- Irssi: #agda: Total of 117 nicks [0 ops, 0 halfops, 0 voices, 117 normal]06/08 20:00
-!- Irssi: Join to #agda was synced in 122 secs06/08 20:02
apostolisgallais : Nice.06/08 20:07
carterSaizan_:  dolio  one issue with the type (x :_0 A) -> B its only constant if its like a type application lambda in system F 06/08 20:33
carterif its an irrelevant function, it neededn't be constant, just irrelevant06/08 20:34
dolioThe 0 means that x can only appear in non-computational places, so computationally, it is constant.06/08 20:54
dolioIt's 'parametric'.06/08 20:55
carteryeah06/08 21:28
cartertrue06/08 21:28
carterdolio:  for the core calculus def06/08 21:28
carternot sure if you have something like type classes in the mix06/08 21:28
carterbut yes, for a "core" you're absolutely right06/08 21:28
carterand thats kinda what i like about this genreal design space, gives a nice way of talking about parametricity / irrelevance06/08 21:31

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