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

--- Day changed Fri May 19 2017
lapinotmietek: :) i'm not sure so, but it's interesting! beforehand i was thinking that using unicode and new infix operators everywhere was unmaintainable (because you almost have to learn a new DSL when you look at a new library) (things like if_then_else_ made me think "oh nice :(, that's just objective-C")... But actually here it's justified because of the math symbols which are just convenient (and anyway it's19/05 00:02
lapinotnot a general purpose language)19/05 00:02
mieteklapinot: the have-to-learn-a-new-DSL problem occurs in many different contexts19/05 00:04
mietekI’d say it’s orthogonal to the use of Unicode symbols, but certainly, you could make it more difficult by choosing hostile notation19/05 00:04
mietekI like being able to stick close to the notation used in papers19/05 00:05
mietekso, Agda19/05 00:05
mietekalso, I’ve ran into more annoying issues with Idris than with Agda19/05 00:05
mietekalthough this may be a dated view now, since I’ve basically stopped using Idris a year+ ago19/05 00:06
lapinotyeah, and the notation problem can appear in papers too, so the most important part is actually to establish some conventions (that's why i'm gonna try to stay open-minded with that and see how it goes)19/05 00:06
mietekone nice thing about Idris is universe, uh…19/05 00:07
mietekcumulativity19/05 00:08
lapinotis there some Set_omega?19/05 00:08
mietekhttp://docs.idris-lang.org/en/latest/faq/faq.html#does-idris-have-universe-polymorphism-what-is-the-type-of-type19/05 00:08
mietekThere is Set_omega in Agda19/05 00:08
mietekalso http://docs.idris-lang.org/en/latest/faq/faq.html#what-are-the-differences-between-agda-and-idris19/05 00:08
mietekanother nice thing is that the main author of Idris recently finished writing a book about it19/05 00:09
mietekthere is a book about Agda, but not by one of the authors19/05 00:09
mietekhttps://www.manning.com/books/type-driven-development-with-idris19/05 00:10
mietekhttp://dl.acm.org/citation.cfm?id=284131619/05 00:10
lapinotcool, i'm gonna take a look at the book (probably interesting to get into any dependantly typed language)19/05 00:11
mietekyes, I would expect the lessons to carry over both ways19/05 00:11
mietekCoq books could also be somewhat relevant19/05 00:12
lapinot(actually, when i ran into a problem wanting to have Set_omega, pestering about the heaviness of dealing with levels, i fant out i was not taking the right approach, so anyway issues were you really need that may be uncommon)19/05 00:14
mietekindeed19/05 00:14
mietekhaving to deal with universe levels explicitly does introduce a fair amount of noise, sometimes19/05 00:15
lapinotsomething that was a big shock, coming from "normal" functional languages, is that polymorphism is just an implicit type argument, 'forall' has no real meaning19/05 00:16
mietekwell, forall is actually fundamental to the language19/05 00:16
mietekBTW, if you’re undecided, you may want to check out ##dependent19/05 00:17
lapinotnice, currently i'm seduced by agda but i'm genna hang out there19/05 00:18
lapinotin what way for 'forall'? i'm curious19/05 00:18
mietekhttp://www.cs.bham.ac.uk/~mhe/AgdaTutorial/html/AgdaTutorial.html19/05 00:19
mietekthis is an excellent and succinct Agda tutorial19/05 00:19
mietekscroll down to "-- * The BHKCH intepretation of universal quantification:"19/05 00:20
comietekhttps://www.irccloud.com/pastebin/pUFcfKGd/19/05 00:21
lapinotyep, just saw it, actually to precise what i wanted to say: 'forall' is equivalent to a function definition (so in that way it is central, but not in the way classical languages have it)19/05 00:24
mietek*dependent* function19/05 00:24
mietekor, \Pi type19/05 00:24
lapinothmm indeed, that precision makes sense now19/05 00:25
lapinotisn't there a typo? "[..] is empty if x and y are equal"19/05 00:27
mietek I don’t know; this is "Howard’s idea"19/05 00:30
lapinotsure, but it contradicts the next sentence19/05 00:31
lapinotgoing back to agda vs idris, something that i found neat is a clear and central use of modules (versus type classes), i would say that i'm more on the ML side than the haskell side for this part (ML sucks because there is no implicit argument support but type-classes suck deeply because they enforce things to have only one instance)19/05 00:34
mietekI’m with you here19/05 00:35
mietekalthough one can emulate typeclasses in Agda by using instance arguments19/05 00:35
mietekhttp://agda.readthedocs.io/en/v2.5.2/language/instance-arguments.html19/05 00:36
lapinotyeah, but i don't get the point of using an instance argument versus a normal implicit argument19/05 00:38
mietekit gets handy in hairier code19/05 00:38
lapinoteven when considering parametrized modules as an option?19/05 00:39
mietekI use instance arguments to talk about models; https://mietek.github.io/imla2017/html/CompleteSemantics.html#119/05 00:40
mieteka canonical model then simply becomes an instance19/05 00:40
mietekalso, hello Unicode19/05 00:40
lapinothaha why is everyone doing nbe? .. that is exactely my current excuse to doing dependantly typed programming!19/05 00:43
mietekwell, because it makes sense :)19/05 00:45
mietekwhat logic?19/05 00:45
lapinothm i'm just a undergraduate cs student so it does no go very far, i was hoping to add shift/reset (delimited continuations) to a simply typed lambda calculus (using some papers that gave some typing system for that)19/05 00:46
mieteka Materzok paper?19/05 00:47
mietekjust curious19/05 00:47
mietekor maybe Ilik?19/05 00:48
mietekhttp://www.speleologic.net/publications.html19/05 00:48
mietek"Type Directed Partial Evaluation for Level-1 Shift and Reset"19/05 00:48
lapinotno, that was Polymorphic Delimited Continuations from Kenichi Asai and Y.Kameyam (they did OchaCaml), i read a lot from Filinski and Danvy but actually they don't talk that precisely about type systems if i recall well19/05 00:49
mietekindeed they don’t 19/05 00:49
mietekyou should check out Ilik19/05 00:49
lapinotcool, i'll note that down19/05 00:49
mietekmy work strongly benefits from his "Continuation-passing style models complete for intuitionistic logic"19/05 00:49
mietekwhich is a simplification of shift/reset19/05 00:49
lapinotsounds like i have a lot of nice papers to read :) i checked out your github and it might provide me some inspiration19/05 00:55
lapinotcould i bother you a bit with some more personal (actually professional) question? you seem to have a strong academic background but work not in public and do open-source, that's something that i would go into but it's not so common in academics19/05 00:57
mieteklapinot: that’s better tackled in ##dependent19/05 00:58
mietekany Agda formalisations of real numbers?19/05 23:27

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