[Martin Meyer]

Hello Thomas,

please have a look at these issues:

1)

Code: Select all

class predicates
    test : (unsigned*, unsigned*).
clauses
    test(As, Bs) :-
        if [[As, [X]]] = [[[X], Bs]] then
            stdIO::write("unifies")
        else
            stdIO::write("not unfiable")
        end if.
 
clauses
    run() :-
        test([1], [1]).

outputs "not unfiable".

2)

Code: Select all

domains
    nat{Type} =
        zero(Type);
        one(nat{Type}).
 
class predicates
    inc : (nat{Type}) -> nat{nat{Type}}.
clauses
    inc(N) = one(N).

raises error c504 : The expression has type 'main::nat{Type}', which is incompatible with the type 'main::nat{main::nat{Type}}'

[Thomas Linder Puls]

1) is noted as a bug.

But I believe 2) is correct. If N has type nat{T} then one(N) does also have type nat{T}.

[Martin Meyer]

Oh pardon, by now I see it too, 2) is correct.

However, these kinds of constructions still make me think. Please have another look at this one:

Beforehand, the following works well:

Code: Select all

domains
    nat{Type} =
        zero;
        one(nat{Type}).
 
class predicates
    matchType : (nat{Type1}, nat{nat{Type2}}).
clauses
    matchType(_, _).
 
clauses
    run() :-
        N = zero,
        SuccN = one(N),
        matchType(N, SuccN).

With an anonymous predicate Inc it is also working fine:

Code: Select all

domains
    nat{Type} =
        zero;
        one(nat{Type}).
 
class predicates
    matchType : (nat{Type1}, nat{nat{Type2}}).
clauses
    matchType(_, _).
 
clauses
    run() :-
        N = zero,
        Inc = { (X) = one(X) },
        SuccN = Inc(N),
        matchType(N, SuccN).

But it does not work with an ordinary predicate:

Code: Select all

domains
    nat{Type} =
        zero;
        one(nat{Type}).
 
class predicates
    inc : (nat{Type1}) -> nat{nat{Type2}}.
clauses
    inc(N) = one(N).
    % The expression has type 'main::nat{Type1}',
    % which is incompatible with the type 'main::nat{main::nat{Type2}}'
 
clauses
    run() :-
        N = zero,
        _SuccN = inc(N).

Since the two previous variants work, I assume this one should work as well. But I'm not sure. Thus my question: Is this error also correct or is it a bug?

Finally, while experimenting, I noticed that the compiler dumps on the following variant (which was probably meant to cause a type checking error):

Code: Select all

domains
    nat{Type} =
        zero;
        one(nat{Type}).
 
class predicates
    matchType : (nat{Type}, nat{nat{Type}}). % the compiler dumps on this line
clauses
    matchType(_, _).
 
clauses
    run() :-
        N = zero,
        SuccN = one(N),
        matchType(N, SuccN).

[Thomas Linder Puls]

Well the compiler (obviously) shouldn't dump, it should have given you an error (and I will () have to look at that problem).

Concerning the rest: Your "Peano arithmetic" domain don't need a type parameter at all.

Code: Select all

domains
    nat =
        zero;
        one(nat).

In this simplified version your inc predicate have a declaration like this:

Code: Select all

predicates
    inc : (nat) -> nat.

It is obvious that the type of the input and the output is the same. This is also consistent with the whole Peano arithmetic idea: these are the natural numbers and natural numbers all have the same type. The type of 117 is not more complex than the type of 3 (they are both "just" natural numbers).

Maybe it will ease your understanding if you notice that your natural numbers corresponds to lists. If you have a list and "erase" all the data then you basically have the "Peano number" representing the length of the list.

Now if you take all your code and use the list domain instead of the nat domain. You will also have to add some values to put into your list:

Code: Select all

predicates
    inc : (Type*, Type Dummy) -> Type*.
clauses
    inc(N, Dummy) = [Dummy | N].

In this code it should be obvious that the result type is Type* (not Type**).

[Martin Meyer]

You are of course right about the Peano arithmetic (thanks for the info!). However, my type error has a different origin, which I did not mention for the sake of simplicity. The type error originally occurred in an implementation of a double-ended queue:

Basically, the deque domain consists of a prefix and a suffix buffer of 0 to 8 elements and a middle deque of pairs of elements:

Code: Select all

domains
    deque{Type} =
        empty;
        nonEmpty(buffer{Type}, deque{tuple{Type, Type}}, buffer{Type}).

I have noticed that efficient access to the n'th element of the deque can be established if I simply add a field containing the length of the deque:

Code: Select all

domains
    raDeque{Type} =
        empty;
        nonEmpty(buffer{Type}, raDeque{tuple{Type, Type}}, buffer{Type}, positive Length).

The trouble started when I tried to create a catenable version of the random access deque by applying a "bootstrapping" pattern to domain raDeque{Type}:

Code: Select all

domains
    raCatDeque{Type} =
        singleton(Type Elem);
        nonsingle(raDeque{raCatDeque{Type}}).

The predicates of the raCatDeque class cannot be based on the predicates of raDeque, as the length field must be treated differently. In the original raDeque class, the length of an entry is always counted as 1. However, the entries are now deques, each of which has an individual length.

Trying to create a specialized version of the raDeque class that correctly calculates the length of entries led me into a nested type mess that the compiler categorically complained about.

I removed everything from my nested type construction that was not necessary to produce the error, renamed domain and functors to make it look intuitive ...that's the way I produced 2).

As you have told, the type error in 2) is correct, and so was the type error in the code of my specialized raDeque class.

By now I have found a solution that avoids overly complicated nested type constructions. I have added a length field to each buffer field. The increase in memory consumption seems justified, since the additional fields not only make length computation easier, but are also necessary to find the n'th element in O(log N) time (where N is the total number of elements).

Final question: the type layout with prefix/suffix buffer and middle deque is well known, but I have not seen a name for it anywhere. I called it "Isorecursive Pairing Deque". Do you know of a better, perhaps commonly known name?