Type inference

[GoogleCodeExporter]

What steps will reproduce the problem?
1. Declare a list of pairs. Each pair is an integer (identifier) and a
list. These sublists can have different types. Example:
[ [1, [1,2]], [2, [a,b]] ]
2. Implement a method that inserts an element in a sublist of a certain index.
3. Implement a method that concatenates all the sublists 
4. If I use the concatenation method before the insertion, it is not
possible to insert elements of types other than integer in index 2 of a
list like this: [ [1, [1,2]], [2, []] ]

PS: The code is attached.

What is the expected output? What do you see instead?
I would expect Teyjus to return a type error while compiling, since
concatenation has type: list A -> list A -> list A, and should not work if
the sublists are of different types. Nevertheless, it compiles OK, and it
fails in the insertion (even if the insertion is made in an empty sublist).

What version of the product are you using? On what operating system?
Teyjus version 2.0-b2
Ubuntu 9.10

Please provide any additional information below.
I am attaching 3 files. test_types.mod and test_types.sig is the
implementation of the functions described above. In test_cases.txt there
are some queries that demostrate what works and the query that fails. The
main problema is: suppose I try to insert element 'a' in the second sublist of:
[ [1, [1,2]], [2, []] ]

If I use only the insertion predicate, it returns:
[ [1, [1,2]], [2, [a]] ]

But if I use the concatenation method somewhere before, it calls the same
insertion predicate but it fails. My guess is that, because of the
concatenation, Teyjus infers that all the sublists have the same type, so I
am not able to insert elements of different types in the other sublists
anymore. As far as I know, teyjus wasn't supposed to infer types during
runtime, is that correct?

Thank you.
Giselle

Original issue reported on code.google.com by giselle....@gmail.com on 29 Apr 2010 at 3:52

Attachments:

• test_types.mod
• test_types.sig
• test_cases.txt

[GoogleCodeExporter]

Here's a slightly smaller example which illustrates the same behavior.

sig issue44.

kind pair type.

type pr           A -> B -> pair.

type match_types  pair -> o.
type fst          pair -> A -> o.
type snd          pair -> B -> o.

type test1        pair -> o.
type test2        pair -> o.
type test3        pair -> o.

module issue44.

% This just forces A and B to have the same type
match_types (pr A B) :- X = [A,B].

fst (pr A B) A.
snd (pr A B) B.

% This succeeds with P = pr 1 2 as expected
test1 P :- match_types P, fst P 1, snd P 2.

% This succeeds with P = pr 1 [2] as expected
test2 P :- fst P 1, snd P [2].

% This returns no solutions. Maybe there should be a run-time type error?
test3 P :- match_types P, fst P 1, snd P [2].

Original comment by andrew.g...@gmail.com on 30 Apr 2010 at 8:21

Attachments:

• issue44.sig
• issue44.mod

[GoogleCodeExporter]

Hi,

In my opinion, the detection of this kind of problem should be at compilation 
time. To think of it, consider this simpler example which also compiles and 
returns "no": 

.mod:
is_int (X:int). 
test :- is_int "23".

.sig:
type is_int     A -> o.
type test       o.

The problem is that the unification for types in only done with the type 
information (provided either in the .mod or in the .sig file), and not with the 
more specific types which can appear explicitly (as in my example) or 
implicitly (like that was in Andrew's example with X = [A,B]) in a clause.

To check that is_int "23" is well-typed, there should be amongst all the 
clauses defining is_int, a clause which has a type equal or greater than 
string. 
For instance, the clause is_int (X:string) could be added and that would 
compile.
I think that really should be "equal or greater than" and not "the type string 
or any unrestricted type wrt to the signature" (even if it's fine in this case) 
because for types like
A -> B -> C -> o
we can have partial restrictions.

Having a run-type error is a bad idea because that would rule out this kind of 
program (where we want to simply fails unification if the term encountered is 
not an integer or a string):
.mod:
is_int (X:int).
is_string (X:string).
test :- read X, (is_int X, print "int\n") ; (is_string X, print "string\n").

.sig:
type is_int     A -> o.
type is_string  A -> o.
type test          o.

For this example it is important to have logic variable in the types and 
restrictions in the clauses. Otherwise that does not compile.

Hoping that can help...
Fabien

Original comment by fafounet@gmail.com on 29 Jan 2013 at 3:04