--- Day changed Sat Jul 29 2017
lapinothi29/07 19:05
Nik05`Hi29/07 19:05
lapinoti was thinking about module systems and traits (type classes), this is still a research topic today but agda seems to have done it. Have there been difficulties? or notable advances on the theoretical part?29/07 19:06
lapinotsome ocaml people are working on "modular implicits" which i think are somewhat the same idea, is there any reason why it would be more difficult to do in ocaml vs agda?29/07 19:08
Nik05`Agda had typeclasses?29/07 19:09
Nik05`Has*29/07 19:09
lapinotyeah, i mean, it has "instance arguments" and records29/07 19:09
lapinotbut since it's dependantly typed, ml modules would simply be agda records so maybe it's not really the same...29/07 19:10
lapinotmaybe the whole thing is simpler to do in agda because it's dependantly typed, but for the particular part of instance resolution, i don't see how it's not applicable to other languages29/07 19:12
Nik05`I don't know much about the language itself, well nothing really29/07 19:13
akrIs this the current way to implement a main in agda? https://agda.readthedocs.io/en/v2.5.2/tools/compilers.html#example29/07 20:31
akrhmm, this looks nicer http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual2.Compilation29/07 20:32

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