[05:37:01] I see 4/6 posts about GrammaticalFramework with the [gf] tag on stackoverflow. [07:42:04] *** Quits: proteusguy (~proteusgu@cm-58-10-154-216.revip7.asianet.co.th) (Ping timeout: 246 seconds) [11:08:59] *** Joins: proteusguy (~proteusgu@58-97-48-85.static.asianet.co.th) [14:04:01] *** Quits: proteusguy (~proteusgu@58-97-48-85.static.asianet.co.th) (Ping timeout: 258 seconds) [16:56:32] *** Joins: proteusguy (~proteusgu@cm-58-10-154-216.revip7.asianet.co.th) [17:05:17] drbean: yeah, that's way more than I expected! [17:18:34] *** Quits: proteusguy (~proteusgu@cm-58-10-154-216.revip7.asianet.co.th) (Ping timeout: 250 seconds) [17:32:32] *** Joins: proteusguy (~proteusgu@cm-58-10-154-216.revip7.asianet.co.th) [19:37:27] turns out I actually had a legit question! https://stackoverflow.com/questions/55883172/grammatical-framework-linearization-type-field-cannot-be-int-how-to-write-a [19:43:32] i guess the solution is not to use int but to only use peano numbers [19:44:11] yeah, that's another option [19:44:20] in the GF book, there's another chapter with Nats [19:44:30] or even simpler for each nat to remember if it is even or odd [19:44:50] oh yeah I didn't even consider making the function Even truthful [19:44:55] zero = { isEven = True }; [19:45:39] succ n = { isEven case n.isEven of { True => False ; False => True } } ; [19:45:46] yeah [19:46:05] I was just thinking about the representation of the numbers [19:46:18] so this is what it says on page 149 [19:46:20] A simple example of the use of proof objects is the definition of well-formed time spans: a time span is expected to be from an earlier to a later time: [19:46:20] from 3 to 8 [19:46:20] is thus well-formed, whereas [19:46:20] from 8 to 3 [19:46:20] is not. The following rules for spans impose this condition by using the Less predicate: [19:46:21] cat Span ; fun FromTo : (m,n : Nat) -> Less m n -> Span [19:46:55] [19:47:14] that makes it look like I could expect output like "3" and "8" from the GF Nats [19:47:51] but maybe it was just a shorthand for "nah just kidding, use haskell to get the nice output, we can do proof objects in GF" [19:48:45] you can have a look at what i did with numbers here: https://github.com/daherb/mulle-spatial/tree/master/grammar [19:49:16] but i didn't find a good way to deal with them either [19:49:35] haha that's promising [19:49:55] it produces (s (s ... zero)) and the linearizes to 1+...+1 in html/css [19:52:44] oh yeah that could be another option, create an arithmetic expression in GF that is meant to be evaluated in another program :-D [19:53:54] or you can probably hardcode some numbers e.g. all between 0 and 12 [19:55:31] maybe you can find a way that (s (s z)) is mapped to the fun two which again is linearized as "2" [19:57:02] i just remembered that i did that but i don't remeber if that worked [20:00:36] hahah [20:00:46] well, we'll see! I can ask aarne on monday [20:00:51] and then I can answer myself ^_^ [21:30:00] ooh I'm getting a TypeError in python [21:33:49] I wonder if this is a standard python error message, "TypeError: the arguments must be expressions", because I was trying out this embedding GF grammars in python, and giving a string as an argument to a GF constructor [21:33:57] whereas it expects an expression [22:52:21] inariksit: maybe i should take the python for nlp class at esslli to finally learn some python [22:53:00] *** Quits: inariksit (~inari@ksit.fixme.fi) (Ping timeout: 246 seconds)