Using has_type(list(Type), X) with user created type not working as expected

Help!
1

When using has_type/2 added more types via multifile which are working fine.

Then wanted to use

has_type(list(Type), X) :-
    is_list(X), element_types(X, Type).

by calling has_type/2 from the module importing the library errors, and the code started failing.

As near as I can figure, element_types/2 (GitHub) needs to be exported.

Example 

:- module(example, []).

:- use_module(library(error)).

% :- use_module(library(error),
%     [
%         element_types/2
%     ]).

:- multifile
    error:has_type/2.

error:has_type(key_value,Key_value) :-
    key_value_validate(Key_value).

key_value_validate(Key_value) :-
    must_be(ground,Key_value),
    Key_value = kv(Key,Value),
    must_be(ground,Key),
    must_be(ground,Value).

:- begin_tests(example_bad).

test(1) :-
    has_type(list(key_value),[kv(1,a),kv(2,b)]).

:- end_tests(example_bad).

has_type_workaround(list(Type), X) :-
    is_list(X), error:element_types(X, Type).

:- begin_tests(example_workaround).

test(2) :-
    has_type_workaround(list(key_value),[kv(1,a),kv(2,b)]).

:- end_tests(example_workaround).

?- run_tests.
% PL-Unit: example_bad 
ERROR: d:/has_type_list_example.pl:28:
        test 1: received error: plunit_example_bad:'unit body'/2: Unknown procedure: plunit_example_bad:has_type/2
 done
% PL-Unit: example_workaround . done
% 1 test failed
% 1 tests passed
false.

Also tried using

:- use_module(library(error),
    [
        element_types/2
    ]).

instead of

:- use_module(library(error)).

which resulted in

?- consult('D:/has_type_list_example.pl').
Warning: d:/has_type_list_example.pl:9:
Warning:    import/1: error:element_types/2 is not exported (still imported into example)
true.

Can use_module/2 be used to import predicates from modules that did not export the predicate? This has me confused.

2

With a warning, yes. You should avoid warnings though :slight_smile: Otherwise it is not clear to me what you are trying to do. I see no reason for element_types/2 to be exported. Can you share the code you want to write?

3

Yes I can, it will be large but let me ask this first. :smiley:

I did make a complete minimal working example in the previous post, did you click on the triangle

image
to expand the section

image
…

to see the code example?

1 Like
4

Note on the example code. This clause:

can be simplified to:

key_value_validate(Key_value) :-
    must_be(ground,Key_value),
    Key_value = kv(_,_).

If Key_value is ground, then necessarily Key and Value are also ground.

1 Like
6

3 posts were split to a new topic: Types with SWI-Prolog

7

The issue seems to be

:- begin_tests(example_bad).

test(1) :-
    has_type(list(key_value),[kv(1,a),kv(2,b)]).

:- end_tests(example_bad).

error:has_type/2 is multifile, but not part of the interface of library(error). Type checking is done using must_be/2 (throws error) or is_of_type/2 (fails)

:- begin_tests(example_bad).

test(1) :-
    is_of_type(list(key_value),[kv(1,a),kv(2,b)]).

:- end_tests(example_bad).

With that change I get

101 ?- run_tests.
% PL-Unit: example_bad . done
% test passed
true.
1 Like
10

Follow up for others interested in using library errors.

I have been using library errors in creating some deterministic code (emulator) and found that there are two very different ways of using the type checking.

  1. is_of_type/2 fails and is useful with non-deterministic code.

  2. must_be/2 throws exceptions and is useful with deterministic code when the condition should not occur. I use this to stop the execution of the code immediately in test cases.

So from the answer by Jan learned that instead of using has_type/2 which is not exported, should use either is_of_type/2 or must_be/2.

Example 
:- module(example, []).

:- use_module(library(error)).

:- multifile
    error:has_type/2.

error:has_type(key_value,Key_value) :-
    key_value_validate(Key_value).

key_value_validate(Key_value) :-
    is_of_type(ground,Key_value),
    Key_value = kv(_,_).

:- begin_tests(valid_examples).

test(3) :-
    is_of_type(list(key_value),[kv(1,a),kv(2,b)]).

test(4,[fail]) :-
    is_of_type(list(key_value),[kv(1,_),kv(2,b)]).

test(5) :-
    must_be(list(key_value),[kv(1,a),kv(2,b)]).

test(6,[error(type_error(key_value,kv(1,_)),_)]) :-
    must_be(list(key_value),[kv(1,_),kv(2,b)]).

:- end_tests(valid_examples).

Running

?- run_tests.
% PL-Unit: valid_examples .... done
% All 4 tests passed
true.

And from the answer by Paulo that if you test a term for ground then all of the arguments must also be ground, so no need to test each one.

Also must note that the list of types as seen in must_be/2 is not a complete list. To see all of the types, you have to look at the source code on GitHub for has_type/2

In creating the test cases for this example to force one to return fail and one to return error found out that for any user created predicate of error:has_type/2 it should not use must_be/2 but is_of_type/2 because if the code needs to fail and calls has_type/2 with a must_be/2 it will not fail but cause an error, however when must_be/2 calls a user created predicate of error:has_type/2 and error:has_type/2 fails, then must_be/2 can return an error.

If you also read my other post, you know that I like algebraic data types and use to think they could not be done with SWI-Prolog until I found package typedef. I have not used it yet, but worth noting for others looking at using types with SWI-Prolog.

11

Doesn’t parametric types gives you in practice the same expressive power of algebraic data types? The parameters on a parametric type can be (and usually are) other types, which can also be parametric. With the basic parametric types defined by default, you can define quite complex types.

12

I should know that, but I don’t.

As such I will take some time to learn more about this and possibly add some links.

tl;dr

Parametric types makes be think of generics in other languages, and algebraic data types make me think of discriminated unions, and to me the two are different. Not saying you are wrong, but I can’t say you are right.

One of these years I will actually take the time to work through “Types and Programming Languages” by Benjamin C. Pierce (link) (WoldCat)

In just asking you made me realize that I did not mention one of the reasons I like algebraic types.

While they let you compose types from other types, during the compilation phases of type inference and checking, it can also identify where the code does not cover all of the cases of the type. I wanted to give an example, but finding examples of bad code with error messages is not easy.

In other words, when I think of algebraic data types, I think of the data as a set, and the algebraic data type definition defines what is in the set. In languages such as F# when you write a switch statement to process the data type, the compiler will warn you if the switch statement did not cover all of the items in the set. This then lets me think of the data with function compositions like this

image
image1024Ă—1231 91.5 KB

By Stephan Kulla (User:Stephan Kulla) - Own work, CC BY-SA 4.0, Link

and because of the warnings about not covering the complete set, it gets me closer to thinking of the code as a proof which means the codes is more correct.

When I program in F# (which has been a few years ago because I haven’t needed it lately) I could go for weeks without ever needing the debugger by just learning to effectively make use of the type system and fix all of the warnings. In programming Prolog, I miss the warnings about the cases not covered and only discovered during run time.

1 Like
13

You can also use attributed variables to make algebraic data types. The example given in the link is pretty close.

You can use conditional compilation to turn it on if you want it only during development.

1 Like