[04:17:17] *** Quits: proteus-guy (~proteus-l@cm-58-10-208-180.revip7.asianet.co.th) (Remote host closed the connection) [08:09:57] *** Joins: proteus-guy (~proteus-l@184.82.235.0) [08:10:18] *** Joins: proteus-dude (~proteus-l@node-19dm.pool-125-24.dynamic.totinternet.net) [12:01:10] *** Quits: proteus-dude (~proteus-l@node-19dm.pool-125-24.dynamic.totinternet.net) (Ping timeout: 256 seconds) [12:13:28] *** Joins: proteus-dude (~proteus-l@184.82.235.0) [12:25:27] *** Quits: proteus-guy (~proteus-l@184.82.235.0) (Read error: Connection reset by peer) [12:25:27] *** Quits: proteus-dude (~proteus-l@184.82.235.0) (Remote host closed the connection) [14:13:05] *** Joins: proteus-guy (~proteus-l@cm-58-10-208-180.revip7.asianet.co.th) [14:13:27] *** Joins: proteus-dude (~proteus-l@cm-58-10-208-180.revip7.asianet.co.th) [14:15:58] *** Quits: proteus-dude (~proteus-l@cm-58-10-208-180.revip7.asianet.co.th) (Client Quit) [17:11:22] hi! [17:13:05] i would like to have type level Nat:s but parse and linearise as ordinary numerals [17:13:56] i am thinking that there is no real way of doing that in gf - but that i might have to do that in e.g. haskell. [17:14:30] is that correct? [17:26:29] good question, I haven't found out the answer myself either! if you do, consider posting the answer here https://stackoverflow.com/questions/55883172/grammatical-framework-linearization-type-field-cannot-be-int-how-to-write-a [17:31:04] or do you mean that the costructors Zero and Succ would be types themselves, not funs? [17:31:23] in that question, there's cat Nat ; fun Zero ; Succ ; [17:41:51] inariksit: thanks [17:42:27] it is also reading chapter 6 of the gf book that got me wondering. [17:42:58] but i think i am happy enough with Zero and Succ being types rather than funs. [17:47:16] but that might just make my goal more unlikely. i'm a bit confused. [18:00:29] esg: i used Nums in my own way here: https://github.com/daherb/mulle-spatial/blob/master/grammar/Spatial.gf [18:02:01] but I didn't really manage to linearize them as ordinary numbers, so I linearaize them to 0+1+1+... and let css do the actual summing here: https://github.com/daherb/mulle-spatial/blob/master/grammar/SpatialHTML.gf [18:21:32] daherb: nice! [19:01:43] esg: i am not sure if it makes sense stand alone, but in january i gave a presentation about some experiments i did with dependent types in gf (and what is not working properly). the material is available here: https://github.com/daherb/GF-Dependent-Types [19:02:13] it also was my first attempt to use the GF core for jupyter notebooks [21:42:28] daherb: thanks! i'll have a look at that.