Changes between Version 8 and Version 9 of ExtensibleRecords


Ignore:
Timestamp:
Nov 12, 2007 1:45:30 PM (8 years ago)
Author:
guest
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • ExtensibleRecords

    v8 v9  
    2525 * `r - L` the record `r` with field `L` deleted
    2626 * `t ::- L` the record type `t` with field `L` deleted
    27  * `r + s` record `r` extended by adding all the fields of `s`. Many systems restrict to the case where `s` is constant.
    28  * `t ::+ u` record type `t` extended by adding all the fields of type `u`. Many systems restrict to the case where `u` is constant.
     27 * `r + s` record `r` extended by adding all the fields of `s`. Many systems restrict to the case where `s` has constant shape.
     28 * `t ::+ u` record type `t` extended by adding all the fields of type `u`. Many systems restrict to the case where `u` has constant shape.
     29 * `r <- s` record `r` updated by replacing the all fields of `s`. Many type systems restrict to the case where `s` has constant shape.
     30
     31By '''constant shape''' we mean that the field names of a record are given literally, though the values and types of the fields could be variables.
     32
     33= Type Systems =
     34
     35The most important difference between the various record proposals seems to be the expressive power of their type systems. Most systems depend on special predicates in the type context. As usual there is a trade-off between power and simplicity.
     36
     37 No predicates:: You can get away without any predicates if you are prepared to allow records to have multiple fields with the same label. In the '''scoped labels''' system, the syntactic form of the type matches that of the record, so you can type the operators by
     38 * `(. L) :: a ::+ {L :: b} -> b`
     39 * `(- L) :: a ::+ {L :: b} -> a`
     40 * `(+ {L = v}) :: a -> a ::+ {L :: b}`
     41 * `(<- {L = v}) :: a ::+ {L :: b} -> a ::+ {L :: b}`
     42
     43 Positive predicates:: If you allow only positive information about records in the context, you can only type some of the operators. In '''A proposal for records in Haskell''' the condition `a <: {L1::t1, L2 :: t2, ...}` means that `a` is a record type with at least the fields `L1, L2, ...` of types `t1, t2, ...` respectively. You can type the following operators:
     44 * `(. L) :: a <: {L :: b} => a -> b`
     45 * `(<- {L = v}) :: a <: {L :: b} => a -> a`
     46
     47 Lacks predicates:: In order to type the other operators, we need negative information about records. In the Hugs '''Trex''' system the condition `a \ L` means that `a` is a record type without a field `L`. You can type all the operators if you restrict the right-hand sides to constant shape records:
     48 * `(. L) :: a \ L => a ::+ {L :: b} -> b`
     49 * `(- L) :: a \ L => a ::+ {L :: b} -> a`
     50 * `(+ {L = v}) :: a \ L => a -> a ::+ {L :: b}`
     51 * `(<- {L = v}) :: a \ L => a ::+ {L :: b} -> a ::+ {L :: b}`
     52
     53 General predicates, using type families:: The '''Type Families''' system uses three predicates: {{{ a `Contains` L }}} means that `a` is a record type with a field labelled `L`; {{{ a `Disjoint` b }}} means that `a` and `b` are record types with no fields in common; and {{{ a `Subrecord` b }}} means that `a` and `b` are record types, and every field of `a` also occurs in `b` (with the same type). You can type all the operators:
     54 * {{{ (. L) :: a `Contains` L => a -> a ::. L }}}
     55 * {{{ (- L) :: a `Contains` L => a -> a ::- L }}}
     56 * {{{ (+) :: a `Disjoint` b => a -> b -> a ::+ b }}}
     57 * {{{ (<-) :: a `Subrecord` b => b -> a -> b }}}
     58
     59 General predicates, using functional dependencies:: The '''Heterogeneous Collections''' and '''Poor Man's Records''' systems achieve the same as the '''Type Families''' system, using the relational style of functional dependencies. In '''Poor Man's Records''', `Select L a b` means that `a` is a record type with a field labelled `L`, and `b = a ::. L`; `Remove L a b` means that `a` is a record type with a field labelled `L`, and `b = a ::- L`; and `Concat a b c` means that `a` and `b` are record types with no fields in common, and `c = a ::+ b`. You can type the operators:
     60 * {{{ (. L) :: Select L a b => a -> b }}}
     61 * {{{ (- L) :: Remove L a b => a -> b }}}
     62 * {{{ (+) :: Concat a b c => a -> b -> c }}}
     63The `Subrecord` predicate and `<-` operator could easily be added. The difference between '''Heterogeneous Collections''' and '''Poor Man's Records''' is that '''Poor Man's Records''' makes no attempt to sort labels or remove duplicates, so for example `{x = 3, y = 4}` and `{y = 4, x = 3}` have different types, so are certainly not equal.
    2964
    3065