Finally, I got this to work. First, I'll go over specifications of polymorphic type systems needed for the specpification of extensible records. Then, I'll try to explain the specification of a type system supporting extensible records based on row poplymorphism. All the examples in this article are aviailible on an online IDE (follow the links on the TIPER hompage) along with the slides for the invited talk at CoALP-Ty '16.

### Review on Polymorphic Type Systems

I wrote about this in my blog article and it is also a published paper in FLOPS 2016. So, I won't go into detailed explnanations but just list the Prolog specifications of STLC, HM, and type-constructor polymorphism. We need at least the flexibility of type-constructor polymorphism in the type system to support row polymorphism because row variables need to be categorized by a separate kind other than the kind for types.

Let's start from STLC:

Then, HM:

Then, HM + Type Constructor Polymorphism:

What's going on there is that we do type and kind inference in two stages, where kinds are either o or K1 -> K2 where both K1 and K2 are kinds. Becase there are type constructor variables with different kinds, we need to make sure that all types are 'well-kinded' by satisfying the kind predicate just as we are making sure that all terms are 'well-typed' by the typed predidate. Firist, we do type inference and collect all queries (or constraints) for the kind inference as an yet uninterpreed list, which is using Definite Clause Grammars (DCGs). The type predicate is defined as a DCG. One can use phrase predicate to invoking queries of DCGs. Then, we run the kind predicates generated by the DCG query over type predicate. For example, we can use the code above as follows:

On top of this we can also easily add kind polymorphism (it is basically HM at the type level) as in our previous work (FLOPS 2016), but for row polymorphism, this is enough. Kind polymorphism is not needed for row polymorphism.

### Extensible Records based on Row Polymorphism

Here is how we extend HM + tycon poly with row polymorphism for extensible records:

The kind predicate is extended for the row kind. The row kind is inhabited by row configurations. A row configuration can either be a row variable or an extension of a row configuration with a name--type pair. In addition, we use a more advanced notion of type equality on application terms to overcome the limits of the structural unification in Prolog. The type predicate is extended for typing rules for records accordingly using some helper predicates (zip_with and type_many), which is rather straightforward.

A more subtle part of the change worth explaning further is the use of a more advanced notion of type equaity (eqty) in the clause for the application term, which is defined as follows:

The eqty predicate extends structural unification with a notion of opend-ended map unification (unify_oemap) with name--value pairs, where names are atomic terms in Prolog and values are unifiable objects modulo eqty (thus, eqty and uunify_oemap are mutually recursive definitions). Because we represent an extensible records as possibly opend-ended list by a row variable, using a Prolog standard library predicate such as perumtation, which works for finite lists, is not going to work well. In addition, we use cut in to prevent backtracking from eqty because this eqty predicate is intended to be a decision procedure that does not need backtraking. The use of eqty in application terms is in sync the with common wisdom of performing more advanced notions of type matching in applications (e.g., argument value is a subtyping of a formal argument of a function in type systems with subtyping) when developing syntax-directed rules for type systems. In terms of constraint generation and solving, we can also understand this as forcing to solve the collected constraints for records whenever the type system tries to type-infer (or type-check) the application terms. Ordinary structural unification is nativly handled by the Prolog where no manual control is needed for the constraint-generation and constraint-solving (except for delaying kind inference after type inference using DCGs). But open-ended records by membership constraints is more like handling constraints, therefore, some manual control is inevitable. What !, { eqty(A,A1) } is doing in the type predicate is that it prevents generating infinite hopless candidates for open-ended map unification (e.g., hopelessly trying to unify [x:_|_], [_,x:_|_], [_,_,x:_|_], ... with []) and decides to fail.

The predicate for open ended map unification (unify_oemap) is defined as follows:

You can run the full example code at http://ideone.com/x13a5O .