Problem with list types
Problem
(This discussion uses terms and types from rOTTR and syntax of stOTTR)
The way lists, blank nodes and IRIs are typed currently introduces some issues. First of all, the way lists are typed in mOTTR does not make sense:
[...] and the type of nonempty lists is NonEmptyList<LUB
> where P is the subtype-least type such that each element's type is subtype of P
This means e.g. that the type of the list (1, 2, _:a)
is NonEmptyList<LUB<rdfs:Resource>>
, so the following is well-typed:
SubClassOfList[owl:Class ?sub, NEList<owl:Class> ?supers] .
SubClassOfList(:c, (1, 2, _:a)) .
In the implementation Lutra, lists are typed according to a similar statement, but without the LUB
, so e.g. (1, 2, _:a)
has type NonEmptyList<rdfs:Resource>
. This makes the above example invalid, as expected. However, this type system also makes the following instance (assuming the same signature as above) invalid:
SubClassOfList(:c1, (:c2, _:a))
as the list (:c2, _:a)
has type NEList<rdfs:Resource>
which is not compatible with NEList<owl:Class>
.
The problem really stems from the fact that _:a
can be anything, thus it is difficult to determine the type of a list containing _:a
.