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.
Replying to
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`.
2
1
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
This sounds a lot like the approach taken by Shen: shenlanguage.org
I've never looked at it in detail, but always thought the idea of embedding prolog to write a fancy type system sounded interesting.
1
Hmm, not sure, I think it's kind of the other way around? Ie. using prolog directly to implement a type system.
2
Show replies