Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Alias type for List and ADT types #2063

Open
b-scholz opened this issue Sep 8, 2021 · 3 comments
Open

Alias type for List and ADT types #2063

b-scholz opened this issue Sep 8, 2021 · 3 comments

Comments

@b-scholz
Copy link
Member

b-scholz commented Sep 8, 2021

The current version of Souffle prohibits alias types for lists and ADTs. For example,

.type myList = [l:myList, n:number]
.type myEqList = myList

and

.type myADT = b {l:myList, n:number}
.type myEqADT = myADT

will fail.

It is a simple change in the type system. We need a special case. In method TypeDeclarationChecker::checkUnionType the case,

 } else if (!isA<ast::UnionType>(subtype) && !isA<ast::SubsetType>(subtype)) {
            report.addError(tfm::format("Union type %s contains the non-primitive type %s",
                                    type.getQualifiedName(), sub),
                    type.getSrcLoc());
        }

can be extended to

 } else if (!isA<ast::UnionType>(subtype) && !isA<ast::SubsetType>(subtype) && types.getTypes() > 1) {
            report.addError(tfm::format("Union type %s contains the non-primitive type %s",
                                    type.getQualifiedName(), sub),
                    type.getSrcLoc());
        }

for this purpose. Also, I would like to remark that it might be better to introduce an equivalence type class rather than using the union-type class.

However, the I/O system needs fixing as well. I.e., the root type must be passed on (i.e. the actual List / ADT) so that the I/O system can handle the complex type.

@hide-kawabata
Copy link
Contributor

hide-kawabata commented Sep 13, 2021

I found a bug that may be related to the discussion here.

.type TPositive = number
.decl N(a1:number)
.decl Positive(x:TPositive)
.decl Divisible(x:number, y:number)
N(-2).
N(i+1) :- N(i), i < 5.
Positive(as(x, TPositive)) :- N(x), x > 0.
Divisible(x, y) :- N(x), Positive(y), x % y = 0.
.output Positive
.output Divisible

In the above, the last clause defining Divisible causes errors. When you remove the line (and corresponding .output), you will not get an error.

@b-scholz b-scholz changed the title Type Equivalence for List and ADTs Alias Type for List and ADTs Sep 13, 2021
@b-scholz
Copy link
Member Author

Also, the following example is not working:

.type L=[a:L,  b:number]
.type A=L

.decl R(x:A)
R(nil).
R([nil,1]).

.output R

@b-scholz
Copy link
Member Author

We have similar issues with ADTs:

.type L= next {a:L,  b:number} | end {}
.type A=L

.decl R(x:A)
R($end()).
R($next($end(),1)).

.output R

@b-scholz b-scholz changed the title Alias Type for List and ADTs Alias type for List and ADT types Sep 13, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants