[03:17:12] *** Joins: drbean (~drbean@TC210-63-209-208.static.apol.com.tw)
[03:25:50] *** Quits: drbean (~drbean@TC210-63-209-208.static.apol.com.tw) (Ping timeout: 256 seconds)
[08:15:57] *** Quits: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se) (Ping timeout: 256 seconds)
[11:12:55] *** Joins: wmacmil (~wmacmil@c83-252-138-144.bredband.comhem.se)
[11:40:33] <wmacmil> how do you generate a random ast for a dependent type
[11:40:50] <wmacmil> *dependently typed category
[11:42:01] <wmacmil> Harper> gr -cat=Exp
[11:42:01] <wmacmil> Category Exp should have 1 argument(s), but has been given 0
[11:42:01] <wmacmil> In the type: Exp
[11:42:08] <wmacmil> as an example of the error i'm referencing
[11:42:27] <wmacmil> where the cat is defined
[11:42:28] <wmacmil> cat
[11:42:30] <wmacmil>   Exp Typ ;
[11:42:54] <wmacmil> because whitespace doesn't work
[13:51:04] <inariksit> hmm, does it work to put it in quotes?
[13:51:31] <inariksit> if Exp Typ is an argument to some other function, you can cheat and write a hole of that type in some other tree
[13:51:41] <inariksit> say you have some fun f : Exp Typ -> Foo
[13:51:51] <inariksit> > gr f ?
[15:51:20] <wmacmil> yeah that was my ad hoc solution
[15:52:03] <inariksit> I wouldn't be surprised if there's no way for it, dependent types are not all that well supported in GF :-P
[15:52:09] <wmacmil> but it works in quotes :)
[15:52:14] <inariksit> okay, cool!
[15:52:19] <wmacmil> i just didnt see that specified anywhere
[15:52:31] <inariksit> yeah I don't think I've seen it either, just guessing
[15:52:39] <wmacmil> are you familiar with HOAS in gf?
[15:53:09] <inariksit> familiar in the sense "have read tutorial about it", but never needed in any of my actual projects
[15:55:14] <inariksit> this bug which was reported in 2016 https://groups.google.com/g/gf-dev/c/fatik3-_AG8/m/anor-hI9CQAJ was fixed in 2020, https://github.com/GrammaticalFramework/gf-core/issues/76 with a comment: "Since practically no one uses HOAS it was left unnoticed for a long time."
[15:57:08] <wmacmil> i think it might actually be useful for writing grammars with instrinsically typed expressions
[15:59:37] <inariksit> I'm not sure what that means :-D but I guess you'll tell us in 2 weeks
[16:00:03] <wmacmil> but i'm a bit confused about the linearization phase though
[16:00:07] <inariksit> I think my slides won't be done before tomorrow, now I have a meeting
[16:00:13] <wmacmil> ok
[16:00:35] <wmacmil> no pressure, you can also do live coding or anything
[16:00:42] <wmacmil> do you still wanna talk?
[16:01:20] <inariksit> haha sorry, I said wrong, I think they will be done tomorrow, but not in advance!
[16:01:33] <wmacmil> oh ok
[16:01:38] <wmacmil> :)
[16:01:59] <wmacmil> no worries, looking forward
[16:03:08] <inariksit> the HOAS linearisation is complete magic, all I know about is from this http://www.grammaticalframework.org/doc/tutorial/gf-tutorial.html#toc119
[16:07:03] <wmacmil> i'm going to send off an email tomorrow morning to the mailing list, so even if your slides aren't ready an abstract would be nice!  like i said, no pressure if that's not possible
[16:08:26] <inariksit> okay, I'll prioritise writing something short tonight, and finish my slides tomorrow during the day
[17:59:56] <wmacmil> so i'm toying around with hoas and i'm not sure how it does it's variable magic
[18:00:32] <wmacmil> for instance, piping a linearized tree into a parse should always yield the original tree
[18:00:45] <wmacmil> but this isn't working because the variable names get assigned automatically
[18:00:56] <wmacmil> Harper> l (MkS Nat (Plus (NatExp 3) (NatExp 4))) | p
[18:00:56] <wmacmil> MkS Nat (Plus (NatExp 3) (NatExp 4))
[18:00:56] <wmacmil> 1 msec
[18:00:56] <wmacmil> Harper> l All (\x -> Eq x x) | p
[18:00:56] <wmacmil> The parser failed at token 2: "forall"
[18:00:57] <wmacmil> 0 msec
[18:01:01] <wmacmil> is an example
[18:01:39] <wmacmil> but the linearizations work
[18:01:40] <wmacmil> Harper> l (MkS Nat (Plus (NatExp 3) (NatExp 4))) | p
[18:01:40] <wmacmil> MkS Nat (Plus (NatExp 3) (NatExp 4))
[18:01:40] <wmacmil> 1 msec
[18:01:40] <wmacmil> Harper> l All (\x -> Eq x x) | p
[18:01:40] <wmacmil> The parser failed at token 2: "forall"
[18:01:42] <wmacmil> 0 msec
[18:01:52] <wmacmil> Harper> l All (\x -> Eq x x)
[18:01:52] <wmacmil> ( forall x ) x = x
[18:01:52] <wmacmil> 0 msec
[18:01:52] <wmacmil> Harper> l (MkS Nat (Plus (NatExp 3) (NatExp 4)))
[18:01:52] <wmacmil> 3 + 4
[18:01:54] <wmacmil> 0 msec
[18:01:56] <wmacmil> Harper>
[18:02:27] <wmacmil> sorry this is so ugly, i can create a github gist if anyone wants to look at the source code, it's really simple
[18:05:39] <inariksit> yeah, show your code
[18:05:59] <inariksit> I assume you have the latest GF, because you're not getting that same error form 2016 :-D
[18:07:00] <inariksit> in case you're doing something weird with whitespace, this is a known thing https://groups.google.com/g/gf-dev/c/c4WNtExo2F4/m/RHHT6HQWAgAJ
[18:12:36] <wmacmil> https://gist.github.com/wmacmil/d73133d7b8b7f409b2938ba2823fbae2
[18:13:02] <wmacmil> the only place I'm using HOAS is in the All and Eq functions
[18:13:18] <wmacmil> and they're verbatim copied from the book
[18:14:12] <wmacmil> but I'd ideally like to be able to have expressions with variables, incorporating the rest of the code present, i.e. be able to say things like
[18:14:23] <wmacmil> ( forall x ) x + 3 = 3 + x
[18:15:02] <wmacmil> ( forall x ) c ++ at ++ x = cat ++ x
[18:15:39] <wmacmil> its just a toy expression language from Robert Harper's practical foundations for programming
[18:17:00] <wmacmil> and I'm trying to see if I can get GF to implement the functionality of the typechecking rules via GF's dependent types and HOAS
[18:17:26] <wmacmil> where all the variable scope for let expressions is dealt with HOAS
[18:18:03] <wmacmil> methinks that one should be to use GF as, not just a parser, but typechecker for this language
[18:18:46] <inariksit> does this smaller example work for you? in the first message of the thread from 2016 https://groups.google.com/g/gf-dev/c/fatik3-_AG8/m/XzeF8wtbBwAJ
[18:25:31] <inariksit> wmacmil: oh, it works if you just specify a lincat!
[18:25:32] <inariksit> Harper> l All (\x -> Eq x x) | p -cat=Prop
[18:25:32] <inariksit> All (\x -> Eq x x)
[18:26:27] <inariksit> you can write this in the beginning of the abstract
[18:26:33] <inariksit> flags startcat=Prop ;
[18:55:52] <wmacmil> sorry i'm gonna have to try tomorrow, i'm going to dinner now.  thank you so much, and lookin forward to your talk
[19:27:47] <inariksit> smaklig måltid!