So, I feel like #GRTT as a core calculus could be amazing. In particular, I think type-driven evaluation (with grades in the types) suddenly gives the RTS perfect information about the exact point a object on the heap becomes unused (and then RTS can then arrange for eager [for scare resources] or delayed deallocation / resource reuse).

But, proving something like that is, I feel beyond my skills right now. I have a basic GRTT evaluator, but it's not heap-based and it doesn't make use of grade information.

I need to figure out a "better" approach for dealing with context-grade-vectors. Using higher-ranked types in GHC #Haskell ...is really hard for me to concentrate on enough.

Anyone want to dispel my illusions about the superiority of GRTT? Or failing that, want to give me tips for ... bi-directional typing or heap-based abstract machines when using a context type indexed by identifiers (scope-checked / scope-correct).

What's the #typetheory tag I need? I need to know how to translate type judgements in well-formedness contraints into a bidirectional typing infer or something like that.

I "finally" got back around to trying to type check #GRTT and the first thing (I think) I need to check is that a term l in context i has Type u for any/some universe. I don't believe I can just call directly into my "check" because I don't have an exact type. (Type 42 is exact; Type u is not) Do I call infer, and then ..?

@polotek I'm full-stack and a big fan of static analysis via types, so I prefer #Purescript #Halogen for the front end and #Haskell for the backend.

Though, eventually I'd like to replace them both with a #GRTT (Graded Modal Dependent Type Theory) based language for multiple reasons.

@pebbe I prefer my errors at compile time instead of at runtime. I prefer Haskell because I learned it first and make use of higher-kinded types in my abstractions.

Though currently, I'm trying to build a "better" language using #GRTT as the core calculus.

(Sort of, I have some properties of an evaluator for a specific grade/mode that I want to prove [preferably in #Agda] and then build a language around that instance of GRTT.)