--- Day changed Fri Aug 04 2017
rntz... argh, I think I've actually run into a case where I want Set \omega04/08 01:46
rntzI guess I can pass an argument04/08 01:47
rntzon the plus side, I can get agda to chain together casts/conversions now: https://gist.github.com/rntz/e280c8810bd2ffc812988515c526529404/08 02:04
rntzdoes anyone have advice on encoding typeclass hierarchies with multiple inheritance into agda?04/08 02:23
gallaisrntz: Ulf is the one doing major work with typeclasses https://github.com/UlfNorell/agda-prelude04/08 07:42
gallaisI guess using "overlap" is important to cut down on time (otherwise the instances found are compared for equality IIRC): https://github.com/UlfNorell/agda-prelude/blob/master/src/Container/Traversable.agda04/08 07:43
gallais02:42 < rntz> ... argh, I think I've actually run into a case where I want Set \omega04/08 08:16
gallaisMe too just now! The level at which an IO computation lives has to be constant: https://agda.github.io/agda-stdlib/IO.html#IO04/08 08:16
gallaisthat's annoying04/08 08:16
gallaisyou need a lot of Level.Lift wrapping :(04/08 08:17
Saizan_overlap is also important in case two typeclasses have the same superclass and you are abstracting over an instance of both04/08 10:14
Saizan_because in that case they will be projections from distinct variables, so actually different04/08 10:14
rntzI guess my actual problem comes down to: I have a diamond inheritance pattern (D descends from B and C, which each descend from A)04/08 13:04
rntzand I want to write some code that takes an instance of type D, and which *requires* that its two contained instances of A be equal04/08 13:05
rntzI guess I could explicitly take an argument of propositional equality type04/08 13:05
rntzthe other option is to regard B, C, and D not as typeclasses descending from A but as structures on it04/08 13:06
rntzso the types B, C, and D would be parameterized over a value of type A04/08 13:06
rntzI tried that, and it made instance resolution for various things become annoyingly ambiguous04/08 13:06
rntz(concretely, my "typeclasses" are A = category, B = cartesian closed category, C = cocartesian category, D = bicartesian closed category)04/08 13:08
rntzgallais: related to Level.Lift, is there some that in agda  (Set n) isn't just cumulative?04/08 13:10
rntzthat is, if (M : Set i) then (M : Set (suc i))04/08 13:10
rntzit seems like it would reduce the need for lifts a lot04/08 13:11
rntzin fact, eliminate it04/08 13:11
rntzand you'd have to quantify over fewer level variables04/08 13:11
rntzhm, I guess my problem is basically equivalent to Saizan, except I want to *enforce* the condition Saizan mentions04/08 13:12
rntz*equivalent to Saizan's04/08 13:12
Saizan_rntz: yeah, the propositional equality argument is probably the best bet04/08 13:19
rntzI'm beginning to think Agda could really benefit from an ML-like module system04/08 18:51
rntzinstead of using records to emulate modules04/08 18:51
rntz(or perhaps that records should just be more like ML modules)04/08 18:51
rntzI guess that complicates everything by adding subtyping, though04/08 18:52
mietekeh?04/08 18:57
mietekwhat do you miss about ML modules?04/08 18:57
mietekare you still trying to do subtyping?04/08 18:57
rntztrying to do subtyping?04/08 19:12
rntzmy situation is described above, where I talk about diamond inheritance04/08 19:13
rntzin particular the bit about category, cartesian closed category, cocartesian category, and bicartesian closed category04/08 19:13
rntzgenerally, ML modules seem to handle inheritance nicely; a module satisfying a signature B that is an extension of signature A automatically satisfies signature A as well04/08 19:17
rntzIn Agda I have to choose between:04/08 19:20
rntz1. (record B where field {{super}} : A; ...), which has problems with diamond inheritance, means I have to explicitly convert from Bs to As sometimes, and makes defining a B involve defining a nested A rather than being flat04/08 19:20
rntzor 2. duplicating fields between A & B and writing a coercion function B -> A04/08 19:21
rntzor 3. (record B (super : A) where ...), which doesn't seem to play nicely with instance resolution in my experience04/08 19:21
rntzfor me, (3) seems most *natural* for the category/cartesian category/cocartesian category stuff, since cartesian-ness is a property of a category; so I'd do (record Cartesian (C : Cat) where ...)04/08 19:21
rntzOTOH, the ML approach would be pretty natural too.04/08 19:22
rntzunrelatedly, I filed this issue, but I'm no longer sure it's really a bug: https://github.com/agda/agda/issues/267504/08 19:29
rntzcan someone look at that and tell me whether it's a bug, or whether I've misunderstood agda in some way?04/08 19:29
mietekrntz: about inheritance: have you seen npo’s https://nicolaspouillard.fr/publis/nameless-painless.pdf ?04/08 20:04
mietekrntz: take a look how he uses Kits04/08 20:04
mietekrntz: also interesting is https://people.cs.kuleuven.be/~dominique.devriese/agda-instance-arguments/icfp001-Devriese.pdf04/08 20:04
mietekmodule DataTm {`} (kit : DataKit {`}) where04/08 20:05
mietek  open DataKit kit04/08 20:05
mietekI remember liking this approach a lot when I redid that development04/08 20:05
mietekI’m not sure if it’ll solve your problem04/08 20:05
mietekI should revisit it04/08 20:05

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