Created
July 12, 2023 12:56
-
-
Save Lev135/48077d95b6973dc9d272690f1afa8776 to your computer and use it in GitHub Desktop.
Abstraction over profunctor optics' kinds
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 TypeFamilies #-} | |
{-# LANGUAGE AllowAmbiguousTypes #-} | |
{-# LANGUAGE TypeApplications #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE InstanceSigs #-} | |
import Data.Data | |
class OpticKind k where | |
-- This definition would give us injectivity with respect to s, t, a, b | |
-- but it doesn't allow to write @Base OKGetter s t a b = s -> a@, since | |
-- there is no lambdas on type level and type synonyms can't be partially | |
-- applied: | |
-- | |
-- type Base k :: Type -> Type -> Type -> Type -> Type | |
-- | |
-- This definition would also be better (though not so clear), but also is | |
-- impossible now: | |
-- | |
-- type Base k s t a b = r | (k, r) -> s, (k, r) -> t, (k, r) -> a, (k, r) -> b | |
type Base k s t a b | |
trivOptic :: Base k a b a b | |
newtype OpticP k a b s t = OpticP { runOpticP :: Base k s t a b } | |
type AnOptic k s t a b = OpticP k a b a b -> OpticP k a b s t | |
runOptic :: forall k s t a b. OpticKind k => AnOptic k s t a b -> Base k s t a b | |
runOptic = runOpticP . ($ OpticP (trivOptic @k @a @b)) | |
class OpticKind k => OpticC k p where | |
opticOp :: Base k s t a b -> p a b -> p s t | |
type Optic k s t a b = forall p. OpticC k p => p a b -> p s t | |
optic :: forall k s t a b. OpticKind k => Base k s t a b -> Optic k s t a b | |
optic = opticOp @k | |
class (OpticKind k1, OpticKind k2) => Is k1 k2 where | |
comp :: Proxy (k1, k2, s, t, a, b, u, v) | |
-> Base k1 s t a b -> Base k2 a b u v -> Base k2 s t u v | |
-- This looks awful since we don't know that "Base k1" is a normal type => | |
-- is injective. See also comment to "Base" definition | |
instance forall k1 k2 u v. (Is k1 k2) => OpticC k1 (OpticP k2 u v) where | |
opticOp :: forall s t a b. Base k1 s t a b -> OpticP k2 u v a b -> OpticP k2 u v s t | |
opticOp b1 p2 = OpticP $ | |
comp (Proxy @(k1, k2, s, t, a, b, u, v)) b1 (runOpticP p2) | |
store :: (Is k k) => Optic k s t a b -> AnOptic k s t a b | |
store = id | |
clone :: forall k s t a b. AnOptic k s t a b -> Optic k s t a b | |
clone = optic @k . runOptic | |
-- Getter | |
data OKGetter | |
instance OpticKind OKGetter where | |
type Base OKGetter s t a b = s -> a | |
trivOptic = id | |
instance Is OKGetter OKGetter where | |
comp _ sa au = au . sa | |
type AGetter s t a b = AnOptic OKGetter s t a b | |
view :: AGetter s t a b -> s -> a | |
view = runOptic | |
type Getter s t a b = Optic OKGetter s t a b | |
getter :: (s -> a) -> Getter s t a b | |
getter = optic @OKGetter | |
storeGetter :: Getter s t a b -> AGetter s t a b | |
storeGetter = store | |
cloneGetter :: AGetter s t a b -> Getter s t a b | |
cloneGetter = clone | |
-- Lens | |
data OKLens | |
instance OpticKind OKLens where | |
type Base OKLens s t a b = (s -> a, s -> b -> t) | |
trivOptic = (id, const id) | |
instance Is OKLens OKLens where | |
comp _ (sa, sbt) (au, avb) = (au . sa, \s v -> sbt s $ avb (sa s) v) | |
instance Is OKLens OKGetter where | |
comp _ (sa, sbt) au = au . sa | |
type ALens s t a b = AnOptic OKLens s t a b | |
viewAndSet :: ALens s t a b -> (s -> a, s -> b -> t) | |
viewAndSet = runOptic @OKLens | |
type Lens s t a b = Optic OKLens s t a b | |
lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b | |
lens = curry (optic @OKLens) | |
storeLens :: Lens s t a b -> ALens s t a b | |
storeLens = store | |
cloneLens :: ALens s t a b -> Lens s t a b | |
cloneLens = clone | |
-- Here I use primitive combinators instead of synonyms 'Lens', 'lens' etc. | |
-- to make it more clear how it works | |
_1 :: Optic OKLens (a, a') (b, a') a b | |
_1 = optic @OKLens (fst, \(_, a') b -> (b, a')) | |
-- >>> runOptic @OKGetter _1 (True, 'x') | |
-- True | |
{- | |
runOptic @OKGetter _1 (True, 'x') | |
≡ runOpticP (_1 $ OpticP (trivOptic @OKGetter)) (True, 'x') | |
≡ runOpticP (optic @OKLens (fst, \(_, a') b -> (b, a')) | |
$ OpticP (trivOptic @OKGetter) | |
) (True, 'x') | |
≡ runOpticP (OpticP $ | |
comp | |
Proxy | |
(fst, \(_, a') b -> (b, a')) | |
(trivOptic @OKGetter) | |
) (True, 'x') | |
≡ runOpticP (OpticP $ | |
comp | |
_ | |
(fst, \(_, a') b -> (b, a')) | |
id | |
) (True, 'x') | |
≡ runOpticP (OpticP $ | |
id . fst | |
) (True, 'x') | |
≡ (id . fst) (True, 'x') | |
≡ True | |
-} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment