[01:16:50] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Ping timeout: 256 seconds) [04:09:59] *** Joins: drbean (~drbean@TC210-63-209-76.static.apol.com.tw) [08:51:16] *** Quits: drbean (~drbean@TC210-63-209-76.static.apol.com.tw) (Ping timeout: 240 seconds) [08:51:39] *** Joins: drbean (~drbean@TC210-63-209-15.static.apol.com.tw) [09:24:42] *** Quits: drbean (~drbean@TC210-63-209-15.static.apol.com.tw) (Ping timeout: 260 seconds) [10:37:01] *** Joins: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) [10:44:56] hey i'm wondering about extreme overgeneration with the use of variables [10:46:30] in order to "support this hypothetical typechecking I mentioned i Have to create functions for placeholders for variables [10:47:14] these being a dependently typed over the input type of the type of the variable in an expression [10:47:27] MkVarB : String -> Var Bool ; [10:47:27] MkVarN : String -> Var Nat ; [10:47:27] MkVarS : String -> Var Strng ; [10:48:04] but this is having the problem that when I try to parse an expression in this programming language, i get extreme overgeneration [10:48:21] Harper> p "apply let y = lambda z : Natural Number . x + 2 in y to 999 + 999" [10:48:21] MkS Nat (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (NatExp 2)))) (Plus (NatExp 999) (NatExp 999))) [10:48:21] MkS Nat (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (NatExp 2)))) (Plus (NatExp 999) (VarExpB Nat (MkVarN "999")))) [10:48:21] MkS Nat (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (NatExp 2)))) (Plus (VarExpB Nat (MkVarN "999")) (NatExp 999))) [10:48:23] MkS Nat (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (NatExp 2)))) (Plus (VarExpB Nat (MkVarN "999")) (VarExpB Nat (MkVarN "999")))) [10:48:26] MkS Nat (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (VarExpB Nat (MkVarN "2"))))) (Plus (NatExp 999) (NatExp 999))) [10:48:29] MkS Nat (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (VarExpB Nat (MkVarN "2"))))) (Plus (NatExp 999) (VarExpB Nat (MkVarN "999")))) [10:48:32] MkS Nat (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (VarExpB Nat (MkVarN "2"))))) (Plus (VarExpB Nat (MkVarN "999")) (NatExp 999))) [10:48:37] MkS Nat (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (VarExpB Nat (MkVarN "2"))))) (Plus (VarExpB Nat (MkVarN "999")) (VarExpB Nat (MkVarN "999")))) [10:48:41] MkS Nat (Plus (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (NatExp 2)))) (NatExp 999)) (NatExp 999)) [10:48:44] MkS Nat (Plus (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (NatExp 2)))) (NatExp 999)) (VarExpB Nat (MkVarN "999"))) [10:48:47] MkS Nat (Plus (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (NatExp 2)))) (VarExpB Nat (MkVarN "999"))) (NatExp 999)) [10:48:50] MkS Nat (Plus (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (NatExp 2)))) (VarExpB Nat (MkVarN "999"))) (VarExpB Nat (MkVarN "999"))) [10:48:53] MkS Nat (Plus (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (VarExpB Nat (MkVarN "2"))))) (NatExp 999)) (NatExp 999)) [10:48:56] MkS Nat (Plus (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (VarExpB Nat (MkVarN "2"))))) (NatExp 999)) (VarExpB Nat (MkVarN "999"))) [10:48:59] MkS Nat (Plus (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (VarExpB Nat (MkVarN "2"))))) (VarExpB Nat (MkVarN "999"))) (NatExp 999)) [10:49:02] MkS Nat (Plus (App Nat Nat (Let (Arr Nat Nat) (Arr Nat Nat) (\y -> VarExpB (Arr Nat Nat) y) (Lam Nat Nat (\z -> Plus (VarExpB Nat (MkVarN "x")) (VarExpB Nat (MkVarN "2"))))) (VarExpB Nat (MkVarN "999"))) (VarExpB Nat (MkVarN "999"))) [10:49:30] when it should be unambiguous [10:49:49] also, is there a way to pretty print a syntax tree so that I can just see it's structure? [10:50:10] you can use tt [10:50:59] e.g. gr | tt [10:51:11] p "apply let y = lambda z : Natural Number . x + 2 in y to 999 + 999" | tt [10:51:46] ah amazing [10:52:19] makes me wanna cry, they should include this in the title of AArne's book [10:52:50] haha yes [10:53:50] but so if i'm working with numerals and variables [10:55:34] is there anyway to flag to gf to tell it : autamatically flag a numeral, (or more generally, a regex of some specified sort) to be given a specified leaf in the tree corresponding to a given fuction [10:56:05] like, fun NatExp : Int -> Exp Nat; [10:56:22] instead of MkVarNat [10:57:05] there is so much undocumented behaviour in GF, I honestly don't know [10:57:54] ok, i can just work with local dummy variables by convention, its just a lot of bookkeeping [10:58:03] i'll ask aarne and see what he suggests [10:58:54] yeah, do that, and let us know! [10:59:30] if you remove mkVarN and just hardcode x, y and z, does all of the ambiguity go away? [11:00:45] exactly what i meant [11:00:50] the only time I dabbled in HOAS in GF, I based it on an example in categorial grammar, and I intended the trees to be like this [11:00:51] MkPhr (AndV2 (\x,y -> Prove x y) (\x,y -> Conjecture x y) Marcel Completeness) [11:01:14] yes, I just wondered if that was all of the ambiguity, or if there was some other lambda weirdness too [11:01:45] but since i want to extend the language I might have to start using metaprogramming techniques to generate gf code [11:02:18] then i'll really be getting into the dirty corners quick :) [11:02:31] (continuing my story) but then I noticed that it also generates all kinds of nonsense, like AndVP (\_1 -> AndVP (\_1 -> AndV2 (\_1, _2 -> Prove _1 Marcel) (\_1, _2 -> Prove Marcel _2) Completeness Marcel) (\_1 -> AndVP (\_1 -> Conjecture Completeness _1) (\_1 -> Conjecture Completeness Marcel) _1) Marcel) (\_1 -> Prove Completeness Completeness) Completeness [11:04:02] yeah i get a lot of that kinda stuff with gr too ^^ [11:07:07] yeah I can imagine [11:07:39] I like how it looks to encode all verbs as functions, I think this is a pretty AST [11:07:40] > l -bind Prove Marcel Completeness [11:07:41] Marcel:NP proved:(S\NP)/NP completeness:NP [11:08:20] the lambdas in my first example are redundant, you can just do this [11:08:22] > l -bind (AndV2 Prove Conjecture) Marcel Completeness [11:08:22] Marcel:NP ( proved:(S\NP)/NP and:(X\X)/X conjectured:(S\NP)/NP ):(S\NP)/NP completeness:NP [11:09:21] but then when you gr, it allows all kinds of (\x, y -> Prove x (\z, z' -> Small x)) [11:09:56] I wrote this manually so it's probably not well-formed, point was just that it puts totally random variables and nests stuff [11:10:46] I know you know all this, you've worked much more on HOAS in gf :-D [12:23:20] what were the categorial grammar peoples critiques [12:23:28] if you remember [12:24:49] yeah it was 4 years ago, I don't really remember :-P [14:01:12] *** Joins: drbean (~drbean@TC210-63-209-212.static.apol.com.tw) [14:02:57] *** Joins: drbean_ (~drbean@TC210-63-209-150.static.apol.com.tw) [14:06:18] *** Quits: drbean (~drbean@TC210-63-209-212.static.apol.com.tw) (Ping timeout: 256 seconds) [14:39:36] *** Quits: drbean_ (~drbean@TC210-63-209-150.static.apol.com.tw) (Ping timeout: 240 seconds) [14:40:27] *** Joins: drbean (~drbean@TC210-63-209-157.static.apol.com.tw) [14:45:29] *** Quits: drbean (~drbean@TC210-63-209-157.static.apol.com.tw) (Ping timeout: 265 seconds) [14:47:20] whats the kill command [14:47:24] in emacas mode [14:47:45] i ran gt and now its already through 170 M of memory [14:58:25] it crashed my spacemacs session [14:59:21] guess I broke gf :) [16:18:33] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Remote host closed the connection) [16:19:02] *** Joins: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se)