Allow for recursive types

[FrancoisLaferriere]

No description provided.

[rkaminsk]

Here is an example that fails because the join of Nat and Pos is not computed correctly.

%*?
type Nat := s(Nat)|null.
type Pos := s(Nat).
pred p(Nat,Pos).
*%
p(X,X) :- X=s(s(null)).

[FrancoisLaferriere]

Do you agree that writing type A := A. or type A := f(A). should result in a wrong type definition error?

[rkaminsk]

Do you agree that writing type A := A. or type A := f(A). should result in a wrong type definition error?

Yes, those are not helpful in practice. Checking this is a bit more involved though because we have to make sure some "terminal" is reachable. This sounds possible to check. The structure reminds me a bit of a context free grammar.

[rkaminsk]

I also noticed that typclingo is quite lax. It accepts the following:

%*?
type Nat := s(Nat)|null.
type Pos := s(Nat).
pred p(Pos).
pred q(Nat).
*%
p(X) :- q(X).

This is currently by design as typclingo just looks for empty joins. Here we are sneaking in a zero into predicate p. Maybe it should be made a bit more strict though. Ideally, we would check that the head is a super type of what is inferred by the body.

[rkaminsk]

@namcsi Maybe you can have a look and see if this is enough to type your meta encodings?

[FrancoisLaferriere]

@namcsi I tried to implement the traffic light examples from you metaasp-temporal paper. They are in the examples folder.

[namcsi]

Hey! Thanks for letting me know, I will play around with this branch a bit and go through the examples you mentioned @FrancoisLaferriere next week when I have a bit more time:)

[rkaminsk]

@FrancoisLaferriere, I went over the meet definition and trying to only put the recursion checks where actually necessary. I still don't fully thought things through. What do you think about the last commit?

[FrancoisLaferriere]

@rkaminsk, I believe it is correct, we only need the check when unfolding type constants.