Editing CTRex (section)

= What the hell are extensible records? =

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

== Row polymorphism ==

Some extensible record systems, such as CTRex, support '''row polymorphism'''. This concept is best explained by an example, consider the following function (in CTRex):

<haskell> 
f ::    Rec ("x" ::= Double .| "y" ::= Double .| Empty) 
     -> Rec ("x" ::= Double .| "y" ::= Double .| "dist" ::= Double .| Empty)
f r = norm := dist ((r.!x * r.!x) + (r.!y * r.!y)) .| r
</haskell>

Where <hask>(.!)</hask> is the function to get a value from a record. This function takes a record with row <hask>{ x = Double, y = Double }</hask> and add returns the same record with a label <hask>dist</hask> added, which carries the distance of the point <hask>(x,y)</hask> from <hask>(0,0)</hask>. 


Now suppose we want to call this function with record <hask>{ name = "PointA", x = 10, y = 10  }</hask>. This is not possible, because the row <hask>{ name = String, x = Double, y = Double  }</hask> and  <hask>{ x = Double, y = Double  }</hask> are not the same.


For this we need row polymorphism: we want to make the function <hask>f</hask> '''polymorphic''' in the rest of the row as follows: 
<haskell> 
f :: ((r :! "x") ~ Double, (r :! "y") ~ Double) =>
     Rec r -> Rec ("norm" ::= Double :| r)
f r = norm := dist ((r.!x * r.!x) + (r.!y * r.!y)) .| r
</haskell>
Now the type <hask> f </hask> reads as follows: Given some record with row <hask>r</hask>where x and y have type Double, return a record in which x,y and dist have type Double and there are also some other fields described by row <hask>r</hask>. The type that GHC infers is even more general :

<haskell>
f :: (Floating t, (r :! "y") ~ t, (r :! "x") ~ t) =>
     Rec r -> Rec (Extend "norm" (r :! "x") r)
</haskell>

== Difference between Heterogenous maps and extensible records ==

A question that may arise after the previous section is: What is the difference between extensible records and heterogenous maps? A hetrogenous map is a map that can store values of different types, see for example the [http://hackage.haskell.org/package/HMap HMap package] (blatant plug, my package ).

In heterogenous maps the type associated with a key is present '''in the type of the key'''. For example, in [http://hackage.haskell.org/package/HMap HMap] a key has type <hask>Key x a</hask> where a is the type of the things we can store at this key, for example <hask>Int</hask>. 


In extensible records, the type associated with a key (now called label) is stored '''in the type of the record''', i.e. in its row. The row states, for example, that <hask>x</hask> is associated with <hask>Int</hask>, The label itself does not hold any information on the associated type. In fact, the associated type may differ between records. 



This means that if a record has <hask>x ::= Int </hask> in its row, then we are '''sure''' that this record has a value of type <hask>Int</hask> for <hask>x</hask>. In a hetrogenous map, we can never be sure if a key is present in a map, i.e. <hask>lookup x m</hask> may return <hask>Maybe</hask>.