Strongly-Typed Multi-View Stack-Based Computations
summary
A DSL embedded in a strongly typed functional host uses heterogeneous lists to statically ensure required stack arguments are present and that untouched tail of the stack is preserved, eliminating runtime stack-errors. It uses universally quantified type variables to allow functions with different stack layouts so mutually recursive functions of arbitrary arities typecheck. The implementation provides evaluation and pretty-printing views plus code generation that emits stack-machine code, generates fresh names for printed definitions, and is shown to work for examples though call-by-name control is left for future work.
AI-written summary · about
chapters (25)
- 0:00Introduction
- 0:41Goals of strongly-typed DSL
- 3:32Naive stack language limits
- 5:00Type system prevents stack errors
- 7:26Instruction composition without failures
- 9:20Adding functions
- 10:46Type system challenges with args
- 12:20Quantitative type system solution
- 13:23Recursive functions
- 15:11Implementing Z combinator
- 16:10Multi-view computations
- 17:55Multi-view design overview
- 18:56Evaluation view implementation
- 20:01Pretty-printing view
- 22:13Mutual recursion in views
- 23:30Printing class support
- 24:15Code generation
- 25:42Conclusion
- 27:13Extending control flow
- 28:31Call-by-name vs call-by-value
- 30:10Push instruction challenges
- 31:15Type system and memory tracking
- 32:56Comparison with typed assembly
- 33:38DSL design philosophy
- 34:01Future control flow work
related talks
41mConcatenative programming and stack-based languages
36mDependently Typed Multi-Stage Programming, Revisited
17mNotions of Stack-manipulating Computation and Relative Monads
24mScoped and Typed Staging by Evaluation
18mSuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT(…)
16mAn Intrinsically Typed Compiler for Algebraic Effect Handlers
14mMulti-stage Programming in the Large with Staged Classes
41mThe Dialectics of Type-Level Programming