6
$\begingroup$

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).

$\endgroup$
5
  • $\begingroup$ Can you give us real citations? Who are the authors of the papers, where and when were the papers published? And also links to the papers. $\endgroup$ Apr 27, 2013 at 22:04
  • $\begingroup$ @WanderingLogic links anda author names added. $\endgroup$
    – sinan
    Apr 28, 2013 at 7:31
  • $\begingroup$ I'm not sure what you mean by "can be implemented". Are you talking about implementing the types? Or the records? $\endgroup$ Apr 28, 2013 at 10:08
  • $\begingroup$ @DaveClarke I made an edit. $\endgroup$
    – sinan
    Apr 28, 2013 at 10:46
  • $\begingroup$ @sinan: In Leijen's paper, Section 2, the extension operator is given using syntax { a = 10 | r }, and the type of the extension operator is given in Section 3.1 as For-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 be For-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$ Apr 28, 2013 at 13:14

1 Answer 1

2
$\begingroup$

In the Gaster and Jones paper, rows are encoded using type application of a few type constants, most notably row extension. Your implementation needs to have the following constructors in Typeconstant:

data Typeconstant = Arrow | EmptyRow | Rec | Var | RowExtension Label

Absence of labels is handled using predicates in qualified types:

data QualifiedType = QualifiedType [(Type {- where kind is Row -}, Label)] Type
data TypeSchema = TypeSchema [(Typevar,Kind)] QualifiedType

Assuming row extension creates a copy of the object, then the type of row_extend in your example is

forall rec:row. (rec\a) => Rec rec -> Rec {a:int|rec}

which would be encoded as

rowExtendType = typeSchema where
  typeSchema = TypeSchema [("rec",KRow)] qualifiedType
  qualifiedType = QualifiedType [(TVar "rec", Label "a")] func
  func = TAp (TAp (TCon Arrow) input) output
  input = TAp (TCon Rec) (TVar "rec")
  output = TAp (TCon Rec) (TAp (TAp (RowExtension (Label "a")) (TCon IntType)) (TVar "rec"))
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.