rntz rntz --- Day changed Fri Aug 04 2017 ... argh, I think I've actually run into a case where I want Set \omega 04/08 01:46 I guess I can pass an argument 04/08 01:47 on the plus side, I can get agda to chain together casts/conversions now: https://gist.github.com/rntz/e280c8810bd2ffc812988515c5265294 04/08 02:04 does anyone have advice on encoding typeclass hierarchies with multiple inheritance into agda? 04/08 02:23 rntz: Ulf is the one doing major work with typeclasses https://github.com/UlfNorell/agda-prelude 04/08 07:42 I 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.agda 04/08 07:43 02:42 < rntz> ... argh, I think I've actually run into a case where I want Set \omega 04/08 08:16 Me too just now! The level at which an IO computation lives has to be constant: https://agda.github.io/agda-stdlib/IO.html#IO 04/08 08:16 that's annoying 04/08 08:16 you need a lot of Level.Lift wrapping :( 04/08 08:17 overlap is also important in case two typeclasses have the same superclass and you are abstracting over an instance of both 04/08 10:14 because in that case they will be projections from distinct variables, so actually different 04/08 10:14 I 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 and I want to write some code that takes an instance of type D, and which *requires* that its two contained instances of A be equal 04/08 13:05 I guess I could explicitly take an argument of propositional equality type 04/08 13:05 the other option is to regard B, C, and D not as typeclasses descending from A but as structures on it 04/08 13:06 so the types B, C, and D would be parameterized over a value of type A 04/08 13:06 I tried that, and it made instance resolution for various things become annoyingly ambiguous 04/08 13:06 (concretely, my "typeclasses" are A = category, B = cartesian closed category, C = cocartesian category, D = bicartesian closed category) 04/08 13:08 gallais: related to Level.Lift, is there some that in agda  (Set n) isn't just cumulative? 04/08 13:10 that is, if (M : Set i) then (M : Set (suc i)) 04/08 13:10 it seems like it would reduce the need for lifts a lot 04/08 13:11 in fact, eliminate it 04/08 13:11 and you'd have to quantify over fewer level variables 04/08 13:11 hm, I guess my problem is basically equivalent to Saizan, except I want to *enforce* the condition Saizan mentions 04/08 13:12 *equivalent to Saizan's 04/08 13:12 rntz: yeah, the propositional equality argument is probably the best bet 04/08 13:19 I'm beginning to think Agda could really benefit from an ML-like module system 04/08 18:51 instead of using records to emulate modules 04/08 18:51 (or perhaps that records should just be more like ML modules) 04/08 18:51 I guess that complicates everything by adding subtyping, though 04/08 18:52 eh? 04/08 18:57 what do you miss about ML modules? 04/08 18:57 are you still trying to do subtyping? 04/08 18:57 trying to do subtyping? 04/08 19:12 my situation is described above, where I talk about diamond inheritance 04/08 19:13 in particular the bit about category, cartesian closed category, cocartesian category, and bicartesian closed category 04/08 19:13 generally, 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 well 04/08 19:17 In Agda I have to choose between: 04/08 19:20 1. (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 flat 04/08 19:20 or 2. duplicating fields between A & B and writing a coercion function B -> A 04/08 19:21 or 3. (record B (super : A) where ...), which doesn't seem to play nicely with instance resolution in my experience 04/08 19:21 for 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 OTOH, the ML approach would be pretty natural too. 04/08 19:22 unrelatedly, I filed this issue, but I'm no longer sure it's really a bug: https://github.com/agda/agda/issues/2675 04/08 19:29 can 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 rntz: about inheritance: have you seen npo’s https://nicolaspouillard.fr/publis/nameless-painless.pdf ? 04/08 20:04 rntz: take a look how he uses Kits 04/08 20:04 rntz: also interesting is https://people.cs.kuleuven.be/~dominique.devriese/agda-instance-arguments/icfp001-Devriese.pdf 04/08 20:04 module DataTm {} (kit : DataKit {}) where 04/08 20:05 open DataKit kit 04/08 20:05 I remember liking this approach a lot when I redid that development 04/08 20:05 I’m not sure if it’ll solve your problem 04/08 20:05 I should revisit it 04/08 20:05