Pikelet Theory

39 Members
+pikelet:matrix.org - github.com/pikelet-lang - Theory chat about things possibly related to the Pikelet programming language (eg. dependent types, modal logic, category theory). Let's get confused together!3 Servers

Load older messages

16 May 2021
@_discord_280132690059984897:t2bot.iobrendanzab * what made this particular paper easier? 08:12:19
@_discord_84011264606502912:t2bot.ioLabbekak It starts with a simply-typed system before moving to a dependently-typed system. And the paper also gives some hints on how to implement it 08:17:21
@_discord_280132690059984897:t2bot.iobrendanzab Oh that sounds very handy 08:18:08
@_discord_84011264606502912:t2bot.ioLabbekak It really made things "click" for me 08:18:08
@_discord_280132690059984897:t2bot.iobrendanzab I love the simply typed -> dependently typed approach to explaining things 08:18:36
@_discord_84011264606502912:t2bot.ioLabbekak And regarding the flaw Boarders ...I don't know 😅 08:18:49
@_discord_84011264606502912:t2bot.ioLabbekak Also in that paper usage checking is not turned off in types (like it is in QTT), that makes it a little simpler 08:22:49
@_discord_84011264606502912:t2bot.ioLabbekak It's easy to extend it to be equivalent to QTT though, just store a 0 or 1 in the context and multiply usages with it. Then in types you store a 0 and in relevant positions you store a 1. 08:23:22
@_discord_280132690059984897:t2bot.iobrendanzab yeah, I remember that now - ie. avoiding the type usages counting towards term usages by multiplying by 0 08:25:36
@_discord_280132690059984897:t2bot.iobrendanzab is it true to say that GrTT is a generalisation of QTT? 08:26:27
@_discord_84011264606502912:t2bot.ioLabbekak They are definitely similar, but the structure of contexts is different 08:34:27
@_discord_84011264606502912:t2bot.ioLabbekak The contexts of GrTT are way more complicated, I'm still trying to understand it 08:34:52
@_discord_84011264606502912:t2bot.ioLabbekak But if you squint you can definitely see that the rules are similar 08:35:44
@_discord_84011264606502912:t2bot.ioLabbekak I wonder if GrTT has strong sigmas 08:35:52
@_discord_84011264606502912:t2bot.ioLabbekak In GraD (https://arxiv.org/abs/2011.04070), (0 Nat : Type) ** (Z : Nat) ** (S : Nat -> Nat) ** () is not so usable because you cannot project out the (0 Nat : Type) even in types. In QTT usage checking is disabled in types so it allows you to do that. I have a feeling that in GrTT it's also not allowed. 08:37:52
@_discord_280132690059984897:t2bot.iobrendanzab Is this a related question? https://twitter.com/goobamine/status/1392959410192875522 10:09:04
@_discord_84011264606502912:t2bot.ioLabbekak Here is a presentation of the GraD paper btw: https://www.youtube.com/watch?v=yrwtXrey7mE 11:58:50
17 May 2021
@_discord_535117309732323328:t2bot.ioBoarders One interesting thing I have found in my implementation experiments so far is that in QTT it makes most sense to have a ordered semiring with a monus operator. The reason is when you implement the Var rule you want to do something like check how much of the resource you have available and then monus the amount you are asking for (though in that case you can only be asking for zero or one) 02:18:08
@_discord_535117309732323328:t2bot.ioBoarders That is probably just specific to how I am implementing it though 02:18:18
@_discord_84011264606502912:t2bot.ioLabbekak I'm using the GraD rules. There usages are checked at binders. So the Var rule doesn't check anything but returns the type of the Var and a usage list of 0s with a 1 at the position of the Var (debruijn index). 05:40:18
@_discord_535117309732323328:t2bot.ioBoarders Yeah, I'm not sure how you go about turning those rules into an algorithm though I read they use a SAT solver to do it which sounds particularly complicated. 13:37:13
@_discord_535117309732323328:t2bot.ioBoarders The natural bidirectiional algorithm pushes usages it sees at binders into the context and then pulls from the context at vars. 13:38:15
@_discord_84011264606502912:t2bot.ioLabbekak but how do you check linear usages like \f x. f x x : (Bool -> Bool -> Bool) -> (1 x : Bool) -> Bool 13:53:51
@_discord_84011264606502912:t2bot.ioLabbekak * but how do you check linear usages like \f x. f x x : (Bool -> Bool -> Bool) -> (1 x : Bool) -> Bool 13:54:04
@_discord_535117309732323328:t2bot.ioBoarders so at the binder for x I am adding to the context that x can be used once 13:59:22
@_discord_535117309732323328:t2bot.ioBoarders then in the application I infer after f x that there are no more usages of x (so my bidirectional algorithm gives back the usages remaining) and so then when you ask to use x again it will so there is zero usages remaining (because 1 monus 1 = 0) 14:00:16
@_discord_535117309732323328:t2bot.ioBoarders I'm not completely sure this works but it is possible to implement it 14:00:27
@_discord_84011264606502912:t2bot.ioLabbekak Aah okay I see, so your algorithm also returns usages but the remaining usages, and not all the usages 14:01:03
@_discord_84011264606502912:t2bot.ioLabbekak Sounds reasonable 14:01:08
@_discord_535117309732323328:t2bot.ioBoarders yeah, that is my strategy. I think Pnenning does something similar when he explains how to implement a linear type theory. 14:01:33

There are no newer messages yet.

Back to Room List