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