[01:21:33] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Ping timeout: 260 seconds) [04:13:47] *** Joins: drbean (~drbean@TC210-63-209-213.static.apol.com.tw) [06:46:04] *** Quits: proteusguy (~proteusgu@cm-58-10-154-202.revip7.asianet.co.th) (Remote host closed the connection) [06:47:59] *** Joins: proteusguy (~proteusgu@cm-58-10-154-202.revip7.asianet.co.th) [07:02:42] *** Joins: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) [08:10:12] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Ping timeout: 264 seconds) [08:14:53] *** Joins: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) [09:46:40] morning didnt see that yesterday [10:04:45] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Ping timeout: 240 seconds) [10:49:12] *** Quits: drbean (~drbean@TC210-63-209-213.static.apol.com.tw) (Ping timeout: 264 seconds) [10:50:33] *** Joins: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) [11:53:43] i think i' [11:53:50] ve halfway figured it out [11:54:04] after 10 hours of banging my head against a keyboard [11:54:18] l ConsBranch (OBranch Zero (Split (ConsBranch (OBranch Zero (Var True)) (BaseBranch (OBranch M (Var False)))))) (BaseBranch (OBranch N (Split (ConsBranch (OBranch Zero (Var False)) (BaseBranch (OBranch M (App (App (Var EqualNat) (Var M)) (Var N)))))))) [11:54:18] zero zero = true m = false @@ zero m n zero = false m = equalNat m n @@ zero m [11:54:26] this is as close as ive come [11:54:39] but i guess i'm having a few problems [11:54:51] and this is maybe just some venting about GF, but so it goes [11:55:07] like, normally when i write a functional program, in say, haskell [11:55:14] i can test each party of my code seperately [11:55:28] and then put them together [11:55:39] and assuming the types are correct, it tends to work [11:55:50] but i don't really see a way of doing this in gf [11:56:13] because the linearization is *too declarative* it gives you no way of kind of breaking it apart [11:56:23] or to see partial evaluation results or anything [11:56:30] so it ends up feeling a lot more imperative [11:57:39] perhaps we can discuss this next meeting, but the main point is, I feel like GF doesn't have either the right tooling for properly testing pieces of a grammar, or perhaps its just not documented because I certainly haven't found any good resources other than your blog posts [11:58:23] like i think aarne's book is good in the sense of it giving you a kind of theoretical understanding of GF. but when it comes to practical examples, debugging, etc, it seems completely absent [12:00:43] like i think a GF Koans would be a really useful tool, because the theory and practical use of GF seems so widely spaced apart [12:02:09] [end of rant]. would love to contribute to some of these ideas (either write my own blog posts, make a KOANs etc) , i just need and time and money to do so :p [13:15:58] @inari, here's a gist of my keyboard headbaning :/ [13:15:59] https://gist.github.com/wmacmil/e20075acd59373d36caa4370bbb7de08 [13:23:40] *** Joins: drbean (~drbean@TC210-63-209-203.static.apol.com.tw) [14:46:47] *** Quits: drbean (~drbean@TC210-63-209-203.static.apol.com.tw) (Ping timeout: 264 seconds) [17:04:28] for @anyone_else interested, the gist is an attempt to get gf to do agda-like pattern matching [23:04:05] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Quit: Leaving)