When I surround my datastructures with terms for better understanding then I create in a way a type. Lets say I have a list L and therefore I use the term list(L). In the subsequent computation I encounter maybe a unification or a comparison of let say list(L) with another term, lets call it numbers(1,2).
Normally this comparison or unification would fail but in my own semantics it is an error.
Is there a possibility (maybe a hook) to track all unifications and comparisons (maybe restricted to a module) to make a typecheck and to create an appropriate error?
No. The only hooks into unification are attributed variables. There is no hook for comparison. You can of course do whatever you want using program transformation.
Why would you want that to be an error, rather than the failure that it is normally? Do you have an example scenario?
By “error” do you mean an Exception as with throw/1 ?
Could you add the type as an attribute and use the attributed variable hooks?
I think this could be possible.
It could look like this:
?- typed( list_of_int( L)).
typed( list_of_int(L))
?- typed( list_of_int( L)), L=[A,2].
L=[A,2]
typed(int(A))
?- typed( list_of_int( L)), L=[A,2], A=a.
error in nth0(0,L,a)
But then I need to implement my own comparison operators which take the type attributes into account.
The use of such a type module has the advantage that automated tests can be shorter because I can leave out several type tests when I am sure that the code fails if the types don’t match.
But when I want to use tabling it can get complicated. Is there a possibility to use attributed variables in tabling?
Additionally it could be cool to have also physical unit calculations. Maybe both can be provided by the same module.
Or to avoid complications I stick to the first idea by wrapping values with types and do the parsing by myself or by term rewriting like Jan proposed.
Or I do both. The computations behind attributed variables could use the wrapped values like an intermediate language.
Or I just expand code which is already typechecked.
I aim to the same andvantages which static typed languages have at the compile time. Since my approach is for a dynamically typed language during the runtime of a program it is not as efficient as a compiler for 2 reasons: I need to get to the error in runtime which in the worst case don’t happen and it has additional runtime overhead. But it allows me to have a clearer view on the used datatypes. And in this case I would prefer an error (see help(error)) and not a throw because it signals a situation which has to be fixed.
What do you intend to happen with:
member(A, [a, 1]), typed(list_of_int(L)), L = [A, 2].
It is clearly an error. Normally you define the types before you use it but thanks to prolog you can do it anywhere.
It is like this:
?- use_module( library( clpfd)).
true.
A=a , A in 1..3.
ERROR: Type error: `integer' expected, found `a' (an atom)
ERROR: In:
ERROR: [16] throw(error(type_error(integer,a),_18862))
ERROR: [13] clpfd:clpfd_in(a,1..3) at /usr/local/lib/swipl/library/clp/clpfd.pl:1658
ERROR: [11] toplevel_call(user:user: ...) at /usr/local/lib/swipl/boot/toplevel.pl:1317
ERROR:
ERROR: Note: some frames are missing due to last-call optimization.
ERROR: Re-run your program in debug mode (:- debug.) to get more detail.
I totally agree with clpfd.
It’s both:
?- A=5, type_error(string, A).
ERROR: Type error: `string' expected, found `5' (an integer)
ERROR: In:
ERROR: [17] throw(error(type_error(string,5),_226))
Notice that throw on the last line.