Last active
November 8, 2021 19:23
-
-
Save danidiaz/a945ff36ddccac0851fea2a4485df350 to your computer and use it in GitHub Desktop.
Repurposing the "getter dot" of RecordDotSyntax for performing record updates.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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) | |
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
But what benefit
gives over say
optics
:(where
OverloadedLabels
resolve to field lens)