[prologist]

Any sufficiently advanced type system is indistinguishable from Prolog.

[baq]

Note to readers: if the author’s username doesn’t make it obvious, it’s funny because is true.

If feeling adventurous, read e.g. https://lpn.swi-prolog.org/lpnpage.php?pagetype=html&pageid=...

[divs1210]

commenting for future reference.

that's a great quote.

[prologist]

Thanks. The Shen language takes this to its logical conclusion (pun intended) and implements a fully Turing complete type system. Types are specified with sequents which are essentially Prolog relations using a slightly different notation.[1]

1: https://shenlanguage.org/OSM/Recursive.html

[divs1210]

Yes! I have played with Shen before.

IIRC the type checker is literally a Prolog.