[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)