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
Replying to
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`.
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
I don't see the point. No native Prolog feature can be reused sensibly, we just get a slower, untyped and more verbose transcription of Haskell/ML code.
2
Maybe it is a silly idea… I guess the Prolog feels a bit closer what I would write in a language reference, but is something I can also run. I'd also like to avoid tying a bootstrap implementation to an language that is already hard to bootstrap itself?
1
1
Show replies