This idea of a higher-order Prolog is very interesting! But it's not clear to me how it can be truly extensional without further limiting the language. For there is another reason why Prolog is not extensional: non-termination. As a simple example, consider this program:
q(X) :- q(X).
It looks like extensional higher-order prolog should have the same problem. The article doesn't address it, so I'll go read the papers.
EDIT: The relevant research papers on Higher-Order Prolog, if anybody is interested: http://arxiv.org/abs/1106.3457 "Extensional Higher-Order Logic Programming"; http://arxiv.org/abs/1405.3792 in which they extend it to negation; https://github.com/acharal/hopes the implementation's github repo
I have a question for you: have you considered what a homoiconic datafun might look like?