--- Day changed Fri Dec 29 2017
svercerHas there been any recent change to the status of universe-polymorphic typeclasses, beyond what I can find on Google (i.e., nothing)? Would Set\omega data/record types actually be inconsistent? It seems like the (implicit) rule "the type of a universe-polymorphic function can only be found on the RHS of :" could be relaxed to "the type of the type of a universe-polymorphic function (viz. Set\omega) can only 29/12 05:30
svercerbe found on the RHS of :", which would enable universe-polymorphic functions in typeclasses...29/12 05:30
Eduard_Munteanusvercer, I remember instance search could fill out level implicits, either that or I tried working on it a long time ago.29/12 12:37
comieteksvercer: you may be thinking about Coq29/12 13:51
comietekhttps://www.irif.fr/~sozeau/research/publications/drafts/Cumulative_Inductive_Types_in_Coq.pdf29/12 13:52
comieteknew in 8.729/12 13:52
pgiarrussosvercer: I think there was ages ago somewhere on the Agda mailing list a discussion about transfinite levels29/12 14:37
pgiarrussobut I'm not sure how consistent they'd be; maybe that reduces to stronger large cardinals axioms, but it's a hard thing to speculate about29/12 14:38
pgiarrussoEduard_Munteanu: any chance you mean that *implicit* search can fill levels? because it usually can29/12 14:39
pgiarrussoI've NEVER seen levels as instance params, only implicit params29/12 14:40
pgiarrussosvercer: also, without cumulativity set\omega is empty because it has no predecessor, and with cumulativity you can just work in, say, Set 42, and put in it universe-polymorphic functions that work for universes up to 41 29/12 14:44
pgiarrussoor sth. like that29/12 14:44
pgiarrusso*up to 42 probably29/12 14:44
pgiarrussoand hopefully use another level parameter rather than 4229/12 14:44
mietekpgiarrusso, Eduard_Munteanu: agreed; you should be able to write _ instead of explicit levels in most cases29/12 14:45
pgiarrussoequivalently, make your levels implicit29/12 14:46
mietekyes, but sometimes you still need to write Set _29/12 14:47
pgiarrussothe main annoyance is when declaring types you need to bind and use levels carefully29/12 14:47
pgiarrussoah yes29/12 14:47
Eduard_Munteanupgiarrusso, I mean instance search may find 'method' where method : {l} -> ...29/12 16:15
Eduard_MunteanuI mean where there's a 'method : {l} -> F l' in scope and you're looking for {{method : F l}}29/12 16:16
pgiarrussoAaah, OK, yes29/12 16:16
pgiarrussoBut still29/12 16:17
pgiarrussoF l can’t contain polymorphic functions29/12 16:18
pgiarrussoSo you indeed can’t have polymorphic methods within typeclass instances29/12 16:18
pgiarrussoI agree splitting those instances into separate methods might be a workaround, I’m not sure it’s always applicable though29/12 16:19

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