Type Checking Program Code using SHACL (Extended Version)

TL;DR

This paper introduces TyCuS, a formal method for type checking RDF data processing code using SHACL shapes, ensuring type safety and preventing runtime errors in flexible graph data formats.

Contribution

It presents a novel approach that derives SHACL shapes from queries and integrates them into a lambda calculus framework with formal proofs of type safety.

Findings

Formalization of type checking using SHACL shapes.

Proof of type safety for the proposed method.

Enabling type-checked RDF data processing to reduce runtime errors.

Abstract

It is a strength of graph-based data formats, like RDF, that they are very flexible with representing data. To avoid run-time errors, program code that processes highly-flexible data representations exhibits the difficulty that it must always include the most general case, in which attributes might be set-valued or possibly not available. The Shapes Constraint Language (SHACL) has been devised to enforce constraints on otherwise random data structures. We present our approach, Type checking using SHACL (TyCuS), for type checking code that queries RDF data graphs validated by a SHACL shape graph. To this end, we derive SHACL shapes from queries and integrate data shapes and query shapes as types into a $\lambda$-calculus. We provide the formal underpinnings and a proof of type safety for TyCuS. A programmer can use our method in order to process RDF data with simplified, type checked code that will not encounter run-time errors (with usual exceptions as type checking cannot prevent accessing empty lists).