The Head Condition and Polymorphic Recursion
Abstract
In typed logic programming, the head condition states that
for each clause defining a predicate p, the arguments of
the clause head must have the declared type of p, rather than a
proper polymorphic instance.
In typed functional programming, polymorphic recursion means
that in a recursive definition of a function f, the recursive call
to f uses a type which is a proper instance of the
declared type of f.
We show that both notions are also meaningful in the respectively
other paradigm.
We observe a symmetry between the head condition and the
"monomorphic recursion condition" (meaning absence of polymorphic recursion).
We discuss arguments for and against each condition in
both paradigms.