Ah, yes. I remember this well. DCGs are lovely things that allow you to implement a toy example quickly but then the dragon appears and gobbles you up.. The scent of dragon's breath can already be seen in this example in a couple of places. In the first place, using DCGs generatively is very interesting. It implies that you can write programs that generate strings as easily as parse them. But the question of which gr…
> simple type checking becomes undecidable Where can I read more about this?
This book does it well. It can be a heavy slog:
https://mitpress.mit.edu/9780262536431/the-little-typer/
Here is a free book on how type checking can be used to do mathematical proofs: