Pondering the possibility of using Prolog for bootstrapping a type theory + programming language implementation…
…though I'll probably reconsider once I start hitting all the type and mode errors. 😅
Conversation
One motivation is implementing my language in a way that is closer to the inference rules I might use for a specification.
The other is that it seems easier to implement a toy Prolog implementation (if you avoid some fancy features) than a toy version of GHC, OCaml, or Rust.
2
3
Current thoughts:
- Confused about how to use DCG to make a lexer.
- Already wishing for Extended DCG for working with multiple accumulators the same time.
- Feeling the lack of type checking/mode checking.
- Seems like you can't nest modules like: `core:semantics:eval/3`.
Replying to
Extended DCG (info.ucl.ac.be/~pvr/edcg.html) is pretty wild - has strong vibes of the stuff I was seeing in the Functional Machine Calculus, where you can push/pop from different stacks as a way of invoking and handling different effects:
2
3
Anyway, here is my silly little dependent type system implementation so far:
1
5
Wondering if I should use a DCG for threading through the state of my unification solutions in my elaborator, or should I use these nifty “Attributed variables”: swi-prolog.org/pldoc/man?sect
1
1
Replying to
Hey, happy to jump on video some time re dcg/lexer
type checking - Check out pack mavis. Static typing is, yeah....
you can nest modules. you make a 'collection' module.
make a module core that reexports all the others.
1
Ahh cheers, I'll check out mavis
1