I'm working on a type system with extensible records, similar to ones explained in "A Polymorphic Type System for Extensible Records and Variants - Benedict R. Gaster and Mark P. Jones" and "Extensible records with scoped labels - Daan Leijen",
I already have a working implementation but I followed a completely different path for implementation(for example, I didn't use kinds, instead I used different variables with different types, this also helped me add arbitrary properties to variables, like absent label list). Now I want to implement it like explained in this two papers,
And the problem is, I can't see how can fields and rows with "absent" specifiers can be implemented. Both papers using a simple type constant for record update operations, but types or kinds are not allowing specifying field labels, or absent field names in row variables.
So can anyone help me understand how can field labels and absent fields can be specified in simple kind/type system explained in these two papers?
Thanks in advance.
EDIT: To clarify things,
Here's a language of kinds and types described in papers mentioned above: (in haskell syntax)
data Kind = KStar | KRow | KFun Kind Kind
data Type = TCon Typeconstant
| TVar Typevar
| TAp Type Type -- type application
What I meant to say was I couldn't see a way to encode row types with this language. ie. there is no way to encode type of this function:
row_extend r = r.a = 10
Because there is now way to tell in types that this function adds or updates 'a field with label a
'.
I can't give types to record operations in this language(given as Haskell code above).
{ a = 10 | r }
, and the type of the extension operator is given in Section 3.1 asFor-all r, alpha, (alpha -> {r}) -> {label::alpha | r}
. And in your example the label and alpha are both already bound, right? (I don't recall my Haskell syntax particularly well.) So wouldn't the type would beFor-all r, {r} -> {a::Int | r}
? Then he says (Section 3.1) "we explicitly quantify all types in this paper, but practical systems can normally use implicit quantification." $\endgroup$