Is there a higher order Prolog that wouldn't need a type system?

Question

I suspect that λProlog needs a type system to make their higher
order unification sound. Otherwise through self application some
Russell type anomalies can appear.

Are there alternative higher order Prologs that don't need .sig files?
Maybe by a much simpler type system, that doesn't need that many
declarations but still has some form of higher order unification?

Can this dilemma be solved?

Answer 1

Is there a higher order Prolog that wouldn't need a type system?

These are type-free:

• HiLog

• HiOrd

From the HiOrd paper:

The framework proposed gives rise to many questions the authors hope to ad- dress in future research. In particular, a rigorous treatment must be developed for comparison with other higher-order formal systems (Hilog, Lambda-Prolog). For example, it is reasonably straightforward to conservatively translate the Higher- order Horn fragment of λProlog into Hiord by erasing types, as the resolution rules are essentially the same (assuming a type-safe higher-order unification pro- cedure).

• Ciao (includes HiOrd)