16 May 2021 |

brendanzab | * what made this particular paper easier? | 08:12:19 |

Labbekak | 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 |

brendanzab | Oh that sounds *very* handy | 08:18:08 |

Labbekak | It really made things "click" for me | 08:18:08 |

brendanzab | I love the simply typed -> dependently typed approach to explaining things | 08:18:36 |

Labbekak | And regarding the flaw Boarders ...I don't know ðŸ˜… | 08:18:49 |

Labbekak | 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 |

Labbekak | 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 |

brendanzab | yeah, I remember that now - ie. avoiding the type usages counting towards term usages by multiplying by 0 | 08:25:36 |

brendanzab | is it true to say that GrTT is a generalisation of QTT? | 08:26:27 |

Labbekak | They are definitely similar, but the structure of contexts is different | 08:34:27 |

Labbekak | The contexts of GrTT are way more complicated, I'm still trying to understand it | 08:34:52 |

Labbekak | But if you squint you can definitely see that the rules are similar | 08:35:44 |

Labbekak | I wonder if GrTT has strong sigmas | 08:35:52 |

Labbekak | 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 |

brendanzab | Is this a related question? https://twitter.com/goobamine/status/1392959410192875522 | 10:09:04 |

Labbekak | Here is a presentation of the GraD paper btw: https://www.youtube.com/watch?v=yrwtXrey7mE | 11:58:50 |

17 May 2021 |

Boarders | 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 |

Boarders | That is probably just specific to how I am implementing it though | 02:18:18 |

Labbekak | 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 |

Boarders | 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 |

Boarders | The natural bidirectiional algorithm pushes usages it sees at binders into the context and then pulls from the context at vars. | 13:38:15 |

Labbekak | but how do you check linear usages like `\f x. f x x : (Bool -> Bool -> Bool) -> (1 x : Bool) -> Bool` | 13:53:51 |

Labbekak | * but how do you check linear usages like `\f x. f x x : (Bool -> Bool -> Bool) -> (1 x : Bool) -> Bool` | 13:54:04 |

Boarders | so at the binder for x I am adding to the context that x can be used once | 13:59:22 |

Boarders | 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 |

Boarders | I'm not completely sure this works but it is possible to implement it | 14:00:27 |

Labbekak | Aah okay I see, so your algorithm also returns usages but the *remaining* usages, and not all the usages | 14:01:03 |

Labbekak | Sounds reasonable | 14:01:08 |

Boarders | yeah, that is my strategy. I think Pnenning does something similar when he explains how to implement a linear type theory. | 14:01:33 |