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
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
Show replies