Title: An Executable Specification of Typing Rules for Extensible Records based on Row Polymorphism,
Abstract: Type inference is an application domain that is a natural fit for logic
programming (LP). LP systems natively support unification, which serves as a
basic building block of typical type inference algorithms. In particular,
polymorphic type inference in the Hindley--Milner type system (HM) can be
succinctly specified and executed in Prolog. In our previous work, we have
demonstrated that more advanced features of parametric polymorphism beyond HM,
such as type-constructor polymorphism and kind polymorphism, can be similarly
specified in Prolog. Here, we demonstrate a specification for records, which is
one of the most widely supported compound data structures in real-world
programming languages, and discuss the advantages and limitations of Prolog as
a specification language for type systems. Record types are specified as
order-irrelevant collections of named fields mapped to their corresponding
types. In addition, an open-ended collection is used to support row
polymorphism for record types to be extensible.