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
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
Do you think there could be a point in terms of the constraint solving if the type inference were done that way?
1
I dunno, even using Prolog I think I'd want to implement the algorithm myself, so maybe not? Maybe you could reuse the infrastructure they have for “Attributed variables” for implementing unification:
Quote Tweet
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
Show this thread
1
1
Yeah I was wondering the extent to which you could defer unification or instance resolution
1
1
I haven't seen any way to use native logic programming features to do best practice elab with dep types. For simple types it looks more realistic
2
1
I keep forgetting, but Elpi is a lambda-prolog implementation used for Coq metaprogramming, up to Hierarchy Builder.
But it might be the exact opposite: logic programming built onto the logic monad of the proof assistant.
2
4
I was also thinking of Twelf and Makam (the other lambda Prolog).
lix.polytechnique.fr/~dale/lProlog/
2
3
Makam is coool, have been meaning to try Twelf too at some stage! It seems pretty neat.