Editing CTRex (section)

== Basic extensible records ==

Records are values that contain other values, which are indexed by name (label). Examples of records are structs in c. In Haskell, we can currently declare record types as follows:

<haskell> data HRec = HRec { x :: Int, y :: Bool, z :: String } </haskell>
<haskell> data HRec2 = HRec2 { p :: Bool, q :: Char } </haskell>


Extensible records are records where we can add values (with corresponding label) to existing records. Suppose we have a record <hask>r = { x = 0, y = 0 }</hask>. If we have an extensible record system we can then add a value to this record: 

<haskell> extend z "Bla" r </haskell>

Which gives <hask>{x = 0, y = 0 , z = "Bla"} </hask>

A type-level record, i.e. the mapping of labels to types, such as <hask> {x = Int, y = Bool, z = String } </hask>, is called a '''row'''. 


Such extension is not possible with the <hask>Rec</hask> type above, the fields of the record are fixed. In the non-extensible record system in Haskell currently, the records are typed '''nominally''', which means that we see if two record types are the same by checking the '''names ''' of the records. For example, to check if the type <hask>HRec</hask> is the same as <hask>HRec2</hask>, we check if their names (HRec and HRec2) are equal. n

In an extensible record system the record type are '''structural''': two records have the same type if they carry the same fields with the same types, i.e. if they have the same row. This also means we do not have to declare the type of the record before using it. For example (in CTRex):


<haskell> x := 0 .| y := False .| empty </haskell>


Constructs <hask> { x = 0, y = 0 } </hask> with type :


<haskell> Rec ("x" ::= Int :| y ::= Bool .| Empty) </haskell>


which means <hask> {x = Int, y = Bool } </hask>


This structural typing has the advantage that we can go from <hask> {x = Int, y = Bool } </hask> to  <hask> {x = Int, y = Bool, z = String } </hask> by simply adding the field, we do not have to write a specific function to convert the two types (which would have been necessary with nominal record typing).

Because the associated type for a label is in the row of the record, labels can be used in different records for different types.  This is currently not possible with standard records :

<haskell> 
data X = X { x :: Int, y :: Bool } 
data Y = Y { x :: Bool } 
</haskell>

Will give a Multiple declarations of `x' error.

To summarize, extensible records have the following advantages:

* Labels can be used in different records for different types
* Records do not have to be declared before use.
* Structural typing eliminates the need for explicit conversion functions.