Ende-readme
Ende-readme copied to clipboard
AndyShiue
Ende is a hypothetical programming language.
unsafe
There are three kinds of unsafely arranged with the strength, `unsafe(dyn)` >= `unsafe(const)` >= `unsafe(in type)`. There's also another series of unsafely meaning implementing a trait is unsafe.
Two things: 1. Make the compile-time and run-time representation of a data type different. 2. Let users control the `const` system more specifically.
- [ ] memory layout - [ ] data type flattening - [ ] strict positivity - [x] induction-recursion - [x] induction-induction
See if the current system can be used to model class inheritance.
The paper about rig by Conor McBride seems to be the right way to implement it.
Make inlining functions and data types possible. Inlining a function has the usual meaning; inlining data types measn that the union type should not have a tag, having no runtime...
aka extensible effects, which could freely arrange the underlying monads. I still haven't fully understand the implementation, but I think it would be a great idea to write functional code.