[01:04:00] *** Quits: doppioslash (sid76291@gateway/web/irccloud.com/x-ekdrccsfgdrbwoqd) (Ping timeout: 252 seconds) [01:04:01] *** Quits: MasX (~masx@2001:41d0:a:2340::1) (Ping timeout: 252 seconds) [01:04:09] *** Joins: MasX (~masx@2001:41d0:a:2340::1) [01:09:24] *** Joins: doppioslash (sid76291@gateway/web/irccloud.com/x-ymwoxtcclqsjdwwu) [03:05:49] *** Quits: koo7 (~kook@236.152.broadband3.iol.cz) (Quit: Ragequit) [03:08:04] *** Joins: koo7 (~kook@236.152.broadband3.iol.cz) [05:27:45] *** Quits: Gurkenglas (Gurkenglas@dslb-094-223-143-032.094.223.pools.vodafone-ip.de) (Ping timeout: 246 seconds) [05:59:20] *** Quits: koo7 (~kook@236.152.broadband3.iol.cz) (Quit: Ragequit) [05:59:33] *** Joins: koo7 (~kook@236.152.broadband3.iol.cz) [06:00:10] *** Quits: koo7 (~kook@236.152.broadband3.iol.cz) (Remote host closed the connection) [06:00:19] *** Joins: koo7 (~kook@236.152.broadband3.iol.cz) [12:30:55] *** Joins: Gurkenglas (Gurkenglas@dslb-094-223-143-032.094.223.pools.vodafone-ip.de) [17:00:16] cat Value (class : Class) ; [17:00:27] what does (class : Class) do? [17:01:12] ive been skimming the tutorial and whatnot and couldnt find this part of the syntax explained [17:37:55] *** Quits: koo7 (~kook@236.152.broadband3.iol.cz) (Remote host closed the connection) [17:45:49] *** Joins: koo7 (~kook@236.152.broadband3.iol.cz) [21:18:37] it's the same as just writing cat Value Class ; [21:19:12] you might have seen earlier e.g. some opers that go like irregVerb : (x1,_,_,_,x5 : String) -> String [21:19:31] and that's the same as to write irregVerb : String -> String -> String -> String -> String -> String ; [21:19:56] in those cases, naming the arguments is for making it shorter [21:20:50] with dependent types, it can be used to show that whatever value you are giving it as an argument (like e.g. the fourth String to the irregVerb), it will show up later in the type signature as the argument to some dependent type [21:21:03] let me find an example [21:21:38] so like in this one [21:21:39] http://www.grammaticalframework.org/doc/tutorial/gf-tutorial.html#toc118 [21:21:48] how many forms do finnish nouns have? [21:21:56] you've got cats City and Flight City City [21:22:00] and then this one cat City ; Flight City City ; [21:22:03] aaghs rory [21:22:06] imagine writing irregNoun : String -> String -> String -> .................. [21:22:06] sorry * [21:22:12] cat IsPossible (x,y,z : City)(Flight x y)(Flight y z) ; [21:23:15] so that's *not* identical to cat IsPossible City City City (Flight City City) (Flight City City) ; [21:23:35] because now you require that the first city and the second city have a flight, and the second and third too [21:23:44] so you name the arguments and then you can refer to them later [21:23:47] vin-ivar: hahah [21:24:00] the worst-case constructor needs 10 stem forms ^_^ [21:24:13] but it's 14 cases in 2 numbers, so it's not that bad! [21:25:40] spectre and i found this thing for marathi that included postpositions in forms of the word [21:25:50] imagine doing a worst-case constructor for that [21:25:57] D: [23:00:10] *** Quits: spectre (~fran@115.114.202.84.customer.cdi.no) (Ping timeout: 260 seconds) [23:02:07] *** Joins: spectre (~fran@115.114.202.84.customer.cdi.no)