Is there a way to express read/write/read-write attributes of records in types?

Question

Suppose you have the following product type:

data D = D { getA :: Int, getB :: Char, getC :: [Double] }

and suppose you have a function:

f :: D -> D

which only reads the getA field, but modifies getB and getC.

Is there a convenient way to express this in the type of f?

Answer 1

This is an incomplete solution because it builds on the HasField typeclass from GHC.Records which (so far) only provides getters, not setters. We can write the following function, that explicitly lists the required fields as constraints:

{-# LANGUAGE DataKinds, TypeApplications, FlexibleContexts #-}

import GHC.Records
import GHC.TypeLits

f :: HasField "getA" r Int => r -> r
f r = let _ = getField @"getA" r 
       in undefined -- do some stuff

Using typeclasses in this way lets us avoid potential problems with clients accidentally passing the wrong lenses as parameters.

We might also want to preserve "nominal" typing: to forbid clients from mistakenly passing records that are not of type D but have—by mere chance—compatible fields. Record types like:

{-# LANGUAGE DuplicateRecordFields #-}

data Z = Z { getA :: Int, getB :: Char, getC :: [Double] } deriving Show

We need to define this auxiliary module:

{-# LANGUAGE TypeOperators, FlexibleInstances, MultiParamTypeClasses #-}
module Opaque(Opaque(..)) where

import Data.Type.Equality ((:~:)(Refl))    

newtype HiddenEq a b = HiddenEq (a :~: b)

-- fix concrete a, be polymorphic over b
class Opaque a b where
    opaque :: HiddenEq a b

-- all types have this instance!
instance Opaque a a where
    opaque = HiddenEq Refl 

Opaque a b says that a is actually equal to b, but it doesn't let you access the evidence. Now we can write a function like this:

f' :: (Opaque D r, HasField "getA" r Int) => r -> r
f' r = let _ = getField @"getA" r 
        -- _ = getField @"getB" -- we know r is D, but we can't touch the "getB" field
        in undefined

putting f and f' to use:

main :: IO ()
main = do
    print $ f (D 3 'c' [1.0]) -- compiles
    print $ f (Z 3 'c' [1.0]) -- compiles
    print $ f' (D 3 'c' [1.0]) -- compiles
    print $ f' (Z 3 'c' [1.0]) -- doesn't compile

Answer 2

The problem is that D is too specific. The more you know about a type, the more you can do with a value of it. The reverse is true as well: the less you know, the less you can do with it. The extreme example is id:

id :: a -> a

Because you know nothing about a, the only thing you can do with an input of type a is return it as-is.

Start by making D less specific:

data D' a b c = D' { getA :: a, getB :: b, getC :: c }

Now, you can define f' :: D' a Char [Double] -> D' a Char [Double], which can modify getB and getC in various ways, but can do nothing except reuse getA in the output.

You can further restrict what f' can do to the two fields by passing the functions that do the work as arguments, similar to what Jack Higgins suggested:

f' :: (b -> b) -> (c -> c) -> D' a b c -> D' a b c

Now f' has only one real implementation:

f' f g (D' x y z) = D' x (f y) (g z)

---

Taking one more step, D' is an example of a trifunctor, which is a straightforward (though not predefined or commonly used) extension of a functor.

class Trifunctor (p :: * -> * -> * -> *) where
    trimap :: (a -> b) -> (c -> d) -> (e -> f) -> p a c e -> p b d f


instance Trifunctor D' where
    trimap f g h (D' x y z) = D' (f x) (g y) (h z)

Then

f' :: (b -> b) -> (c -> c) -> D' a b c -> D' a b c
f' bf cf = trimap id bf cf

Answer 3

If you're lens-phobic like me you could get a satisfying solution using only parametricity and a rank 2 type.

{-# LANGUAGE Rank2Types #-}

import Data.Char (toLower)

-- The goal of the question: a type that expresses
-- - Reading an Int
-- - Modifying a Char
-- - Modifying a [Double]
-- Parametricity guarantees your can't do anything else with that t
type YourParticularType = forall t .
     (t -> Int)
  -> ((Char -> Char) -> t -> t)
  -> (([Double] -> [Double]) -> t -> t)
  -> (t -> t)

-- One example of something in that type.
-- No mention of D here, so the user can be sure it won't do
-- anything silly.
f_parametric :: YourParticularType
f_parametric getInt modifyChar modifyDoubles t =
    modifyDoubles (fromIntegral (getInt t) :)
  . modifyChar toLower
  $ t

data D = D
  { getA :: Int
  , getB :: Char
  , getC :: [Double]
  } deriving (Show)

modifyB :: (Char -> Char) -> D -> D
modifyB f d = d { getB = f (getB d) }

modifyC :: ([Double] -> [Double]) -> D -> D
modifyC f d = d { getC = f (getC d) }

-- Shows that D is of suitable form to match YourParticularType
run_f_at_d :: YourParticularType -> D -> D
run_f_at_d f = f getA modifyB modifyC

d1 :: D
d1 = D 42 'Z' [3.14, 1.41]

d2 :: D
d2 = run_f_at_d f_parametric d1

Answer 4

So, let's consider an example:

f :: D -> D
f d = d { getC = map (+ fromIntegral (getA d)) (getC d) }

Clearly, as soon as you have a concrete type like D -> D, all guarantees are off: this function could conceivably be doing anything with its argument.

If you want to prevent that, you need to replace the concrete D with an abstract one, like

f :: d -> d

But of course then the implementation wouldn't work anymore, because on d there's nothing you can do.

   • Couldn't match expected type ‘d’ with actual type ‘D’
      ‘d’ is a rigid type variable bound by
        the type signature for:
          f :: forall d. d -> d

To re-enable just those particular operation you want, you can pass them in as arguments. So, what is a “read-operation or modify-operation parameter”?
Enter lenses. Let's first rewrite all the original example using them:

{-# LANGUAGE TemplateHaskell #-}
import Control.Lens

data D = D { _getA :: Int, _getB :: Char, _getC :: [Double] }
makeLenses ''D

f :: D -> D
f d = d & getC %~ map (+ fromIntegral (d^.getA))

Now, this can be readily generalised / strengthified, by making d abstract but passing the necessary access operations as arguments:

type AGetter' s a = Getting a s a   -- for some reason this isn't defined
                                    -- in the `lens` library

f' :: AGetter' d Int -> ASetter' d [Double] -> d -> d
f' getInt setDbls d = d & setDbls %~ map (+ fromIntegral (d^.getInt))

Which allows you to obtain the old behaviour by passing the getA and getC lenses:

f :: D -> D
f = f' getA getC

The reasons this works is that lens uses typeclass/universal-quantification type trickery to encode a subtype relationship: getA has type Lens' D Int, but AGetter' D Int is a supertype of that with reduced capability, thus guaranteeing that you really only read the focused element, nothing else.

---

Technical detail: you've noticed I wrote ASetter' and not Setter' or ASetter. What this means:

• The AnOᴘᴛɪᴄ versions of Oᴘᴛɪᴄs are their rank-0 correspondents. So e.g. ALens can only be used as a lens, not as e.g. a getter, whereas Lens can be used as a getter or setter or traversal or fold.
  It is considered good style to restrict function arguments to the concrete AnOᴘᴛɪᴄ version, because that means the compiler doesn't actually have to juggle around with rank-2 types. (The type of a Lens itself is merely rank-1 polymorphic, but passing it as an argument would make the accepting function rank-2 polymorphic.)
• The Oᴘᴛɪᴄ' version of Oᴘᴛɪᴄs are the non-type-changing variants. In principle, an e.g. setter could also change the type of a field it focuses on – e.g. when you change the snd type of a (Bool, Char) tuple to String, that would be a Setter (Bool,Char) (Bool,String) Char String, but if you just change the second field to another Char, it's simply a Setter' (Bool,Char) Char (which is actually a synonym for a type-changing setter which happens to change to the same type).

Answer 5

There are two ways to look at this, if you just want a function that 'modifies' D the it would have a type of f :: D -> D. See here for an example:

f :: D -> D
f (D a b c) = D a (modifyB a b) (modifyC a c)
  where modifyB = undefined -- function of type Int -> Char -> Char
        modifyC = undefined -- function of type Int -> [Double] -> [Double]

Another way is to take two functions as arguments to f, one of type Int -> Char -> Char and one of type Int -> [Double] -> [Double]. Here is an example:

f :: (Int -> Char -> Char)
   -> (Int -> [Double] -> [Double])
   -> D
   -> D
f modifyB modifyC (D a b c) = D a (modifyB a b) (modifyC a c)