Record update for Higher-ranked or changing type via Has/get/set [was: Records in Haskell]

AntC anthony_clayden at clear.net.nz
Tue Dec 13 11:31:06 CET 2011


>
Firstly, thank you to SPJ for putting some detailed design into 'Overloaded 
record fields' [SPJ 1].
What I'm showing here draws heavily on the techniques he demonstrates.

I wasn't happy with several parts of the design proposal;
especially not with the amount of not-yet-available type machinery it involved 
(explicit type application, anonymous types, the kind system, String types).

But then SPJ wasn't happy himself with the limitations on Record update for 
polymorphic fields:
      	"This problem seems to be a killer: if record-update syntax is
         interpreted as a call to `set', ...".

It's (too) easy to chuck rocks - the "glaring weakness" of (Haskell's record 
system) is still a swamp despite a pile of rocks (to mix my metaphors).
	

This posting (as a .lhs) is the result of exploring within the "narrow issue: 
namespacing for record field names".
I've used GHC + recent type extensions (v7.2.1). Findings in short:
- I've followed SPJ with a `Has' class, and methods `get' and `set'.
- I seem to have a way to update Higher-ranked fields,
- and change the type of the record,
- and even update Existentially-quantified fields (to a limited extent)
         - which should please the object-oriented oriented.

I'd appreciate some feedback:
- Have I misunderstood the results?
- Are there still unacceptable limitations?
         (Certainly the error messages are impenetrable when you go wrong.)
- The `Has' class, instances and type functions are ugly
         - can we be more elegant?
	(I expect the instances to be generated systematically from the data
         decl. So usually the application programmer won't have to see them.
        I like SPJ's 'Syntactic sugar for Has' to pretty-up Has constraints.)

Disclaimer:
- I'm keeping close to SPJ's objective of improving the situation w.r.t.
        name clashes for record fields. [SPJ 2]
- I'm _not_ claiming this is a design for 'first class record types'
        /extensible records/record polymorphism.
- I'm _not_ making a proposal for 'Records in Haskell'.
        (Not yet: if this is approach is deemed 'workable',
         then I have a design in mind.)
- I'm _not_ envisaging anything like 'first-class labels'.
        (I think that idea is probably not the right objective,
         but that's a debate for another day.)

The basic idea:
- Field selection uses dot notation as reverse-application,
  applying a field selector via Has/get	and resolving the instance to the
  record type and field, that is:
        r.fld ==> fld r, ==> get (undefined :: Proxy_fld) (r at DCons{fld}) = fld
       (I've used (.$) = flip ($) to fake the syntax for dot notation.)
- Record construction and pattern matching with explicit data constructors
  works as with -XDisambiguateRecordFields
- Record update uses H98 syntax, to be compiled to Has/set
  and resolving the instance to the record type and field with explicit data
  constructor:
        r {fld = val} ==> set fld val (r at DCons{..}) ==> DCons{fld = val, ..}
        -- using Puns and WildCards
        (I've used (.=) = set to fake the syntax for update: r.$(fld.=val).)
- Of course, I can't use the field name itself, because that would clash with
  the H98 selector. Instead:
        _fld = undefined :: Proxy_fld		-- for the update syntax
        fld_ = get (undefined :: Proxy_fld)	-- for the (overloadable)
                                                -- selector function

The approach uses a 'loose coupling' between the type arguments of Has/get/set,
with type functions to control the linkage.
  (Some could be Associated Types -- a matter of taste?)

The recipe needs:

> {-# OPTIONS_GHC -XDisambiguateRecordFields -XNamedFieldPuns -XRecordWildCards
                                                                        #-}
> {-# OPTIONS_GHC -XTypeFamilies					#-}
> {-# OPTIONS_GHC -XRankNTypes  -XImpredicativeTypes -XGADTs -XEmptyDataDecls
                                                                        #-}
> {-# OPTIONS_GHC -XMultiParamTypeClasses -XFlexibleInstances
                  -XUndecidableInstances                                #-}

> module HasGetSet	where

	SPJ's example of a higher-ranked data type
                     -- imported so that we have clashing declarations of `rev'

>  import HRrev
>  {- data HR	= HR {rev :: forall a.[a] -> [a]}	-}

>  data Tab a b		where	-- a different data type with a HR field `rev'
>    Ta :: {tag :: String, rev :: forall a_.([a_] -> [a_]), flda :: a }
>      -> Tab a b
>    Tb :: (Num n, Show b) => {tag :: String, fldn :: n, fldnb :: n -> b}
>       -> Tab a b
>                              -- Existential fields (GADT syntax)

	overloadable definitions for field `rev':

>  data Proxy_rev              -- phantom, same role as SPJ's String kind "rev"
>  _rev = undefined :: Proxy_rev
>  rev_ r = get (undefined :: Proxy_rev) r

build some syntax to fake the dot notation, and assignment within record update

>  (.$) = flip ($)
>  infixl 9 .$

>--  (fld .= val) r = set fld val r     -- sadly, this doesn't quite work
>  infix  9 .=                          -- so define (.=) as a method in Has

test rig for higher-rank rev, per SPJ's example, and demos

>  testrev r = (r.$rev_ $ [True, False, False], r.$rev_ $ "hello")
>                            -- dot notation would bind tighter than func apply

>  rHR0 = HR{}               -- `rev' is undefined, to show we can update it
>  rHR1 = rHR0.$(_rev.=reverse)           -- equivalent to rHR0{rev = reverse}
>                            -- testrev rHR1 ==> ([False,False,True],"olleh")
>  rHR2 = rHR1.$(_rev.=(drop 1 . reverse))
>                            -- testrev rHR2 ==> ([False,True],"lleh")

>  rTab0 = Ta{tag="tagged"}  -- `rev' is undefined, to show we can update it
>  rTab1 = rTab0.$(_rev.=reverse)
>                            -- testrev rTab1 ==> ([False,False,True],"olleh")
>  rTab2 = rTab1.$(_flda.='a').$(_rev.=(reverse . take 3))
>                            -- rTab1 :: Tab a b ; rTab2 :: Tab Char b
>                            -- testrev rTab2 ==> ([False,False,True],"leh")


here's the mechanism -- declarations for Has/get/set, and type families

>  class Has r fld t	where
>    get  :: fld -> r -> GetTy r fld t
>    set, (.=)  :: fld -> (forall a_.SetTy r fld t a_) -> r -> SetrTy r fld t
> --   (fld .= val) r = set fld val r     -- } sadly, neither of these work
> --   (.=) = set                         -- } (trying to define a default)

>  type family GetTy  r fld t     :: *  -- the type to get at `fld' in `r'
>  type family SetTy  r fld t a_  :: *  -- type to set at `fld' in updated `r'
>  type family SetrTy r fld t     :: *	-- the type to set for updated `r'

The instance for field `rev' to be a Higher-ranked type.

>  instance (t ~ ([a_]->[a_])) => Has HR Proxy_rev t	where
>                                -- the constraint needs -XUndecidableInstances
>    get _     HR{rev}	= rev
>    set _ fn  HR{..}	= HR{rev = fn, ..}
>    (_ .= fn) HR{..}	= HR{rev = fn, ..}

>  type instance GetTy  r Proxy_rev t    = t
>                        -- that is ([a_] -> [a_]) from the instance constraint
>  type instance SetTy  r Proxy_rev t a_ = ([a_] -> [a_])
>                        -- that is ([a_] -> [a_]) from `set's forall a_
>  type instance SetrTy r Proxy_rev t    = r
>                        -- updating `rev' doesn't change the type

the above type instances apply for any record with field `rev', so also type 
`Tab'

>  instance (t ~ ([a_]->[a_])) => Has (Tab a b) Proxy_rev t	where
>                                -- the constraint needs -XUndecidableInstances
>    get _     Ta{rev}	= rev
>    set _ fn  Ta{..}	= Ta{rev = fn, ..}
>    (_ .= fn) Ta{..}	= Ta{rev = fn, ..}

>  data Proxy_flda              -- `flda's type is a parameter to the data type
>  _flda = undefined :: Proxy_flda
>  flda_ r = get (undefined :: Proxy_flda) r
>  instance Has (Tab a b) Proxy_flda t	where  -- note no constraint on `t',
>                                      -- might be different to `a' for update
>    get _     Ta{flda}	= flda
>    set _ x   Ta{..}	= Ta{flda = x, ..}
>    (_ .= x)  Ta{..}	= Ta{flda = x, ..}

>  type instance GetTy  (Tab a b) Proxy_flda t    = a
>                                 -- this is where we constrain `t' for the get
>  type instance SetTy  (Tab a b) Proxy_flda t a_ = t
                                  -- type to set is whatever we're given
>  type instance SetrTy (Tab a b) Proxy_flda t    = Tab t b
                                 -- set the result type: substitute `t' for `a'

and Has/get/set for the other fields of Tab, including the Existential

>  data Proxy_tag
>  _tag = undefined :: Proxy_tag
>  tag_ r = get (undefined :: Proxy_tag) r
>  instance (t ~ String) => Has (Tab a b) Proxy_tag t	where
>                          -- constraint on `t', because tag is always a String
>    get _     Ta{tag}	= tag
>    get _     Tb{tag}	= tag
>    set _ x   Ta{..}	= Ta{tag = x, ..}
>    set _ x   Tb{..}	= Tb{tag = x, ..}
>    (_ .= x)  Ta{..}	= Ta{tag = x, ..}
>    (_ .= x)  Tb{..}	= Tb{tag = x, ..}
>  type instance GetTy  (Tab a b) Proxy_tag t    = String
>  type instance SetTy  (Tab a b) Proxy_tag t a_ = String
>  type instance SetrTy (Tab a b) Proxy_tag t    = Tab a b
>                          -- changing the tag doesn't change the record's type

>  data Proxy_fldn            -- } the Existential fields must be set together
>  data Proxy_fldnb           -- } possible approach for multiple update
>  _fldn  = undefined :: Proxy_fldn
>  _fldnb = undefined :: Proxy_fldnb
>  -- no point in a 'getter' function: the types would escape

>  instance (t ~ (tn, tn -> b'), Show b', Num tn)
>                                              -- needs -XUndecidableInstances
>           => Has (Tab a b) (Proxy_fldn, Proxy_fldnb) t	where
>                                   -- the use case is: r{fldn = n, fldnb = nb}
> -- get _     Tb{fldn, fldnb}	= (fldn, fldnb)       -- No! types would escape
>    set _ (n, nb)   Tb{..}	= Tb{fldn = n, fldnb = nb, ..}
>    (_ .= (n, nb))  Tb{..}	= Tb{fldn = n, fldnb = nb, ..}
>  type instance GetTy  (Tab a b) (Proxy_fldn, Proxy_fldnb) t    = t
>                       -- that is: (tn, tn -> b') from the instance constraint
>  type instance SetTy  (Tab a b) (Proxy_fldn, Proxy_fldnb) t a_ = t
>  type instance SetrTy (Tab a b) (Proxy_fldn, Proxy_fldnb) (tn, tn -> b')
>                                                                = Tab a b'
>                                      -- changing the fields changes the type

demo

>  nb' Tb{fldn, fldnb} = fldnb fldn           -- test rig

>  rTab3 = Tb{tag="tagged", fldn = 6 :: Double, fldnb = negate}
>                                             -- nb' rTab3 ==> -6.0 :: Double
>  rTab4 = rTab3.$((_fldn, _fldnb).=(5::Int, (6 +)))
>                                             -- rTab3{fldn = 5, fldnb = (6 +)}
>                                             -- nb' rTab4 ==> 11 :: Int


Notes/difficulties:

- Language options needs -XUndecidableInstances because the approach
  "uses a functional-dependency-like mechanism (but using equalities)" [SPJ 1]
  to 'improve' type inference for some instances.
  Since this _doesn't_ use FunDeps, can it safely exceed Paterson Conditions?

- The inability to declare (.=) = set is curious/irritating.
  (Neither as a free-standing function, nor a method of Has with a default
   implementation.
   And even declaring (.=) with a type signature identical to `set'.
   From the error messages, GHC can't match the forall'd `a_'.)

If you've managed to read this far: thank you!


Refs:
[SPJ 1] http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields
[SPJ 2] http://hackage.haskell.org/trac/ghc/wiki/Records





More information about the Glasgow-haskell-users mailing list