Let's consider the task to match something that has a type. We could use the extended matcher and :<, :, :>, as a default. If we don't like it it is possible to redefine it. So what to expect. We genereally constrain types to be of a certain type.

f(X :< number, Y :> number, Z : var) :- Y is X + 1.2.
g(X < a(Z : var), Y > b(Z)) :- ...

Generally an out variable or a result of an expression is of the kind :> and arguments to functions is :< e.g. if an argumnet to a fuction demands a rational number it is ok to supply an integer. But if the result of a sum is typed as number then anything higher like complex is allowed, but not integer so we see that :< is for arguments and :> is for result. : is identical to.

We would actually like to deduce isA relationships, e.g. construct a directed graph with non cycles. this can be done via type

:- type(integer => rational => real => complex => number)

...

The result of this should be a partial order on all entitis that shuld be predicates. Now we can also use type to force a variable to be of a type inside a predicate:

g1 :-
  type(X : integer),
  type(Y : integer),
  f(X,Y).

The unification of a type is as follows:

(X :< A) = (Y :> B) => X=Y, X : ((< A),(> B))
(X :< A) = (Y :< B) => X=Y, X : min(A,B)
(X :> A) = (Y :> B) => X=Y, X : max(A,B)
(X :  A) = (Y xx B) => X=Y, A=B

Now min(A,B) and max(A,B) results in the minimum or maximum acording to the directed graph's partial order or if they are not related, the expression fails. ((< A),(> B)) is an extension of the system and we need to see if it is closed, it works like this.

(X : ((< A),(> B))) = (Y :< C) => X=Y,  X : ((< min(A,C)),(> B))
(X : ((< A),(> B))) = (Y :> C) => X=Y,  X : ((< A),(> max(B,C)))
(X : ((< A),(> B))) = (Y : ((< C),(> D)))) => ...

The last one works by using the distributive law and the other rules. We also add the identity (= A) to this. So with this we see that we can represent all solutions according to this recipy and we do not need more operators and that the , operator is natural here.

It turns out that we given a dependency graph one can compute datastructures for the indexing that is quite effective in shelving out which representation is the most effective one. Not only this. We can allow for alternative via a ; as well.

Now for types of the form f(X : a,Y : B) we interpret as a kind of record and we use the deductions modeled ontop of the following,

X :< f(A : a) = Y :< g(B : b) => X=Y, A=B, X :< min(g,f)(A : min(a,b))

Note that an extension of a record form one form to another can be modeled according to

:-type(f < g),
X :< g(A : a|_) = Y :< f(A2 : a, B : b) => A=A2, X :< f(A : a, B : b | _)

And multiple inheritance can be modeled using ∘

:-type(t < g, f < h)
X :< f((A : a ∘ B : b), C : c) = Y < g(A2 : a)
   => X=Y, A=A2, X < f((A : a ∘ B : b), C : c)

X :< f((A : a ∘ B : b), C : c) = Y < h(B2 : b)
   => X=Y, B=B2, X :< f((A : a ∘ B : b), C : c)

The indexer can knows about this type and match against A : a types or B : b types as well as [[A : a],[B : b]] which is what the ∘ translated to in code.

Last we introduce the or type e.g. ; with this we can do:

X < (number ; var)

To deduce a type that is either an integer or variable. Actually some of the simple predicates can be used by the indexer not var but integer on an atom works quite well.

It is important that the atoms used in types act as a predicate as well. A typed variable is modeled as an attribute, the translation is

X : f(|L) = A. (transforms-to =>) X=A, f(A|L).

if X is a not a variable or attributed variable.

Here is examples for g,h,fabove:

g([X],X : a).
h([X],X : b).   
f([X,Y],[[X : a], [Y : b]]).      
a(1).
a(2).
b(2).
b(3).

Now the accessor logic needs to be designed according to your class implementation it can be used as

get_g_x([X,_] : f(|_),X : a).
get_g_x([X]   : g(|_),X : a).

get_h_x([_,X] : f(|_),X : b).
get_h_x([X]   : h(|_),X : b).

There is alot of things that can be said about an efficient compilation of the inheritance structure. But that is for another time.

Happy Hacking.