<bollu> Is there some way to think of typeclasses as sections of some bundle? Roughly speaking, when we declare instances of (say) Ring, we're declaring a canonical choice of ring structure for each type.
7:40 PM <nf> for each type? how so?
7:40 PM <nf> wouldn't you define a Ring instance for a particular type?
7:42 PM <bollu> well, I guess it's some kind of "partial sections". I'm imagining it like this: when you create a typeclass Ring, you're declaring some bundle over Type. Then, as we declare instances (or infer them), we're somehow building a section of this bundle piecemeal. So a declaration of `instance Ring Int` defines the value of this section over `Int`, and so forth
7:47 PM <nf> ah i see
7:59 PM → econo joined  ⇐ rgrinberg, bollu, Volgaar and search_s1cial quit
Tuesday, December 7th, 2021
12:02 AM <joel135> Ring -> Set
12:04 AM <joel135> (Ring a, Ring b) => Ring (a, b)
12:09 AM <joel135> (Ring x Ring -> Set x Set -> Set); (Ring x Ring -> Ring -> Set)
12:12 AM <joel135> Apparently a commuting square like this can encapsulate an instance inference rule.
12:55 AM → search_social and rgrinberg joined  ⇐ hololeap quit  ↔ [itchyjunk] popped in  ↔ ChaiTRex and leah2 nipped out
8:00 AM <taeaad> joel135: Instance inference in what sense? Instance of a class?
8:01 AM <taeaad> The termininology seems to allude to computer science.
8:25 AM → bollu and Volgaar joined  ⇐ econo and rgrinberg quit
11:29 AM <joel135> yes i was thinking like in haskell