Skip to content

Instantly share code, notes, and snippets.

@danidiaz
Last active November 8, 2021 19:23
Show Gist options
  • Save danidiaz/a945ff36ddccac0851fea2a4485df350 to your computer and use it in GitHub Desktop.
Save danidiaz/a945ff36ddccac0851fea2a4485df350 to your computer and use it in GitHub Desktop.
Repurposing the "getter dot" of RecordDotSyntax for performing record updates.
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
-- | This is an experiment in using the "getter dot" syntax of the upcoming
-- RecordDotSyntax extension for performing record update, without requiring
-- additional record update syntax.
--
-- https://github.com/ghc-proposals/ghc-proposals/pull/405
module Main where
import GHC.Records
import GHC.TypeLits
-- something like this should exist with RecordDotSyntax
class SetField (n :: Symbol) r v | n r -> v where
modifyField :: (v -> v) -> r -> r
--
-- some shared machinery
newtype Setter a b = Setter ((b -> b) -> a)
(.=) :: Setter a b -> b -> a
Setter f .= b = f (const b)
-- Setters in the original record turn into getters of the Setter newtype
instance SetField n b c => HasField n (Setter a b) (Setter a c) where
getField (Setter f) = Setter (f . modifyField @n)
set :: a -> Setter a a
set a = Setter (\f -> f a)
--
--
--
-- example records
data Person = Person
{ name :: String,
address :: Address
}
deriving (Show)
-- automagically derived with RecordDotSyntax
instance SetField "address" Person Address where
modifyField f r = r { address = f (address r) }
data Address = Address
{ street :: String,
number :: Int
}
deriving (Show)
-- automagically derived with RecordDotSyntax
instance SetField "number" Address Int where
modifyField f r = r { number = f (number r) }
person :: Person
person = Person "John" (Address "some street" 7)
person' :: Person
person' = getField @"number" (getField @"address" (set person)) .= 4
-- with RecordDotSyntax, this should be
-- person' = (set person).address.number .= 4
main :: IO ()
main = print $ person'
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
-- | This is an experiment in using the "getter dot" syntax of the upcoming
-- RecordDotSyntax extension for performing record update, without requiring
-- additional record update syntax.
--
-- https://github.com/ghc-proposals/ghc-proposals/pull/405
--
-- This version of the experiment tries to work with the intended final form of the
-- "HasField" typeclass. This means that it must support something like a
-- "setter setter" (!) that has some semblance of respecting the lens laws:
--
-- 1) You get back what you put in:
--
-- view l (set l v s) ≡ v
--
-- 2) Putting back what you got doesn't change anything:
--
-- set l (view l s) s ≡ s
--
-- 3) Setting twice is the same as setting once:
--
-- set l v' (set l v s) ≡ set l v' s
--
-- A "setter setter" seems pretty useless, but we must define it if we want a
-- "passthrough" HasField instance for the Setter newtype.
--
module Main where
-- import GHC.Records
import GHC.TypeLits
-- https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0158-record-set-field.rst#proposed-change-specification
class HasField x r a | x r -> a where
hasField :: r -> (a -> r, a)
--
-- some shared machinery
newtype Setter a b = Setter (b -> a, b)
(.=) :: Setter a b -> b -> a
Setter (f, _) .= b = f b
instance HasField n b c => HasField n (Setter a b) (Setter a c) where
hasField (Setter (fab, b)) =
-- Does blithely ignoring the function c -> a in the argument invalidate the lens laws?
-- I think yes, because that function might contain "a" state, which will be lost, which
-- means the first lens law "getting what you put in" won't hold.
-- We need a way to reconstruct the value only up to "b", not all the way to "a".
( \(Setter (_, c')) -> Setter (fab, fbc c'),
Setter (fab . fbc, c)
)
where
(fbc, c) = hasField @n b
set :: a -> Setter a a
set a = Setter (id, a)
--
--
--
-- example records
data Person = Person
{ name :: String,
address :: Address
}
deriving (Show)
-- automagically derived with RecordDotSyntax
instance HasField "address" Person Address where
hasField r = (\x -> r {address = x}, address r)
data Address = Address
{ street :: String,
number :: Int
}
deriving (Show)
-- automagically derived with RecordDotSyntax
--
instance HasField "number" Address Int where
hasField r = (\x -> r {number = x}, number r)
person :: Person
person = Person "John" (Address "some street" 7)
person' :: Person
person' = snd (hasField @"number" (snd (hasField @"address" (set person)))) .= 4
-- with RecordDotSyntax, this should be
-- person' = (set person).address.number .= 4
main :: IO ()
main = print $ person'
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
-- | This is an experiment in using the "getter dot" syntax of the upcoming
-- RecordDotSyntax extension for performing record update, without requiring
-- additional record update syntax.
--
-- https://github.com/ghc-proposals/ghc-proposals/pull/405
--
-- This version of the experiment tries to work with the intended final form of the
-- "HasField" typeclass. This means that it must support something like a
-- "setter setter" (!) that has some semblance of respecting the lens laws:
--
-- 1) You get back what you put in:
--
-- view l (set l v s) ≡ v
--
-- 2) Putting back what you got doesn't change anything:
--
-- set l (view l s) s ≡ s
--
-- 3) Setting twice is the same as setting once:
--
-- set l v' (set l v s) ≡ set l v' s
--
-- A "setter setter" seems pretty useless, but we must define it if we want a
-- "passthrough" HasField instance for the Focus type.
module Main where
-- import GHC.Records
import Data.Kind
import GHC.TypeLits
-- https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0158-record-set-field.rst#proposed-change-specification
class HasField x r a | x r -> a where
hasField :: r -> (a -> r, a)
--
-- some shared machinery
-- A type-level snoc list.
data SnocList a
= Lin
| Snoc (SnocList a) a
-- should be a private type
type Recon :: Type -> SnocList Type -> Type -> Type
data Recon a xs b where
ReconBase :: (b -> a) -> Recon a Lin b
ReconLink :: Recon a zs b -> (c -> b) -> Recon a (Snoc zs b) c
reconstruct :: Recon a xs b -> b -> a
reconstruct (ReconBase f) b = f b
reconstruct (ReconLink r f) b = reconstruct r (f b)
-- type should be abstract, with hidden constructors
type Focus :: Type -> SnocList Type -> Type
data Focus x xs where
FocusLin :: a -> Focus a Lin
FocusSnoc :: Recon a xs b -> b -> Focus a (Snoc xs b)
-- This should be the only way of building a Focus
focus :: a -> Focus a Lin
focus = FocusLin
-- Only a Focus with a non-empty list can be used with this function. In
-- particular, the result of 'focus' can't be directly used with this function!
-- Need to access a field first.
(|=) :: Focus a (Snoc xs b) -> b -> a
FocusSnoc recon _ |= b = reconstruct recon b
-- The setter seems to follow the lens laws, but it's kind of useles because it "overwrites" everything.
instance HasField n a b => HasField n (Focus a Lin) (Focus a (Snoc Lin b)) where
hasField (FocusLin a) =
( \(FocusSnoc (ReconBase f) b) -> FocusLin (f b),
FocusSnoc (ReconBase f) b
)
where
(f, b) = hasField @n a
-- The setter seems to follow the lens laws, but it's kind of useles because it "overwrites" everything.
instance HasField n b c => HasField n (Focus a (Snoc xs b)) (Focus a (Snoc (Snoc xs b) c)) where
hasField (FocusSnoc recon b) =
(
\(FocusSnoc (ReconLink recon' f) c) -> FocusSnoc recon' (f c),
FocusSnoc (ReconLink recon f) c
)
where
(f, c) = hasField @n b
--
-- example records
data Person = Person
{ name :: String,
address :: Address
}
deriving (Show)
-- automagically derived with RecordDotSyntax
instance HasField "address" Person Address where
hasField r = (\x -> r {address = x}, address r)
data Address = Address
{ street :: String,
number :: Int
}
deriving (Show)
-- automagically derived with RecordDotSyntax
instance HasField "number" Address Int where
hasField r = (\x -> r {number = x}, number r)
person :: Person
person = Person "John" (Address "some street" 7)
person' :: Person
person' = snd (hasField @"number" (snd (hasField @"address" (focus person)))) |= 4
-- with RecordDotSyntax, this should be
-- person' = (focus person).address.number |= 4
main :: IO ()
main = print $ person'
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
module Main where
import Data.Kind
import GHC.TypeLits
import Control.Lens hiding (Snoc)
-- https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0158-record-set-field.rst#proposed-change-specification
class HasField x r a | x r -> a where
hasField :: r -> (a -> r, a)
--
-- some shared machinery
-- A type-level snoc list.
data SnocList a
= Lin
| Snoc (SnocList a) a
-- type should be abstract, with hidden constructors
type Focus :: Type -> SnocList Type -> Type
data Focus start xs where
FocusLin :: forall a. Focus a ('Snoc 'Lin a)
FocusSnoc :: Focus a (Snoc xs b) -> ReifiedLens' b c -> Focus a (Snoc (Snoc xs b) c)
-- This should be the only way of building a Focus
the :: Focus a (Snoc Lin a)
the = FocusLin
into :: Focus a (Snoc xs b) -> Lens' a b
into FocusLin = id
into (FocusSnoc rec (Lens l)) = into rec . l
instance HasField n a b => HasField n (Focus i (Snoc xs a)) (Focus i (Snoc (Snoc xs a) b)) where
hasField foc =
( \_ -> foc, -- does this respect the lensy laws?
FocusSnoc foc (Lens (lens (snd . hasField @n) (fst . hasField @n)))
)
--
-- example records
data Person = Person
{ name :: String,
address :: Address
}
deriving (Show)
-- automagically derived with RecordDotSyntax
instance HasField "address" Person Address where
hasField r = (\x -> r {address = x}, address r)
data Address = Address
{ street :: String,
number :: Int
}
deriving (Show)
-- automagically derived with RecordDotSyntax
instance HasField "number" Address Int where
hasField r = (\x -> r {number = x}, number r)
person :: Person
person = Person "John" (Address "some street" 7)
person' :: Person
person' = person & into (snd (hasField @"number" (snd (hasField @"address" the)))) .~ 4
-- with RecordDotSyntax, this should be
-- person' = person & into the.address.number .~ 4
main :: IO ()
main = print $ person'
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Main where
import GHC.Records
import GHC.TypeLits
import Data.Kind
import Data.Function ((&))
-- I assume GHC will provide a class like this in the future.
-- Right now I define it myself.
class SetField (n :: Symbol) r v | n r -> v where
modifyField :: (v -> v) -> r -> r
--
newtype Optick a b = Optick ((b -> b) -> a -> a)
the :: Optick a a
the = Optick ($)
instance SetField n b c => HasField n (Optick a b) (Optick a c) where
getField (Optick f) = Optick (\changec -> f (modifyField @n changec))
set :: Optick a b -> b -> a -> a
set (Optick f) b = f (const b)
modify :: Optick a b -> (b -> b) -> a -> a
modify (Optick f) = f
--
--
data Person = Person
{ name :: String,
address :: Address
}
deriving (Show)
-- should be automagically derived
instance SetField "address" Person Address where
modifyField f r = r { address = f (address r) }
data Address = Address
{ street :: String,
number :: Int
}
deriving (Show)
-- should be automagically derived
instance SetField "number" Address Int where
modifyField f r = r { number = f (number r) }
person :: Person
person = Person "John" (Address "some street" 7)
--
--
main :: IO ()
main = do
print $ set the.address.number 8 person
print $ person & set the.address.number 8
print $ modify the.address.number (+1) person
print $ person & modify the.address.number (+1)
@phadej
Copy link

phadej commented Nov 8, 2021

But what benefit

print $ person & modify the.address.number (+1)

gives over say optics:

print $ person & over (#address % #number) (+1)

(where OverloadedLabels resolve to field lens)

@danidiaz
Copy link
Author

danidiaz commented Nov 8, 2021

I'm unsure myself. I think the dot syntax resembles a little more how assignment looks in imperative languages (not too much of course, because we are modifying that the and not the value itself). If we are already using OverloadedRecordDot for getting and don't need a fully-featured optics library, adopting this syntax for setting might be the path of least effort.

OverloadedRecordDot could be an alternative to OverloadedLabels within optics itself, by defining the SetField ... => HasField ... instance on an optics type.

I suspect (but haven't verified) that error messages might be a bit better with the dot syntax because, unlike happens with OverloadedLabels, it's directly tied to HasField.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment