{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Data.Record.Generic.Transform (
Interpreted
, Interpret(..)
, liftInterpreted
, liftInterpretedA2
, HasNormalForm
, InterpretTo
, IfEqual
, normalize
, denormalize
, Uninterpreted
, DefaultInterpretation
, normalize1
, denormalize1
, StandardInterpretation(..)
, toStandardInterpretation
, fromStandardInterpretation
) where
import Data.Coerce
import Data.Kind
import Data.Proxy
import Data.SOP.BasicFunctors
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)
import Data.Record.Generic
type family Interpreted (d :: dom) (x :: Type) :: Type
newtype Interpret d x = Interpret (Interpreted d x)
liftInterpreted ::
(Interpreted dx x -> Interpreted dy y)
-> (Interpret dx x -> Interpret dy y)
liftInterpreted :: (Interpreted dx x -> Interpreted dy y)
-> Interpret dx x -> Interpret dy y
liftInterpreted Interpreted dx x -> Interpreted dy y
f (Interpret Interpreted dx x
x) = Interpreted dy y -> Interpret dy y
forall dom (d :: dom) x. Interpreted d x -> Interpret d x
Interpret (Interpreted dx x -> Interpreted dy y
f Interpreted dx x
x)
liftInterpretedA2 ::
Applicative m
=> (Interpreted dx x -> Interpreted dy y -> m (Interpreted dz z))
-> (Interpret dx x -> Interpret dy y -> m (Interpret dz z))
liftInterpretedA2 :: (Interpreted dx x -> Interpreted dy y -> m (Interpreted dz z))
-> Interpret dx x -> Interpret dy y -> m (Interpret dz z)
liftInterpretedA2 Interpreted dx x -> Interpreted dy y -> m (Interpreted dz z)
f (Interpret Interpreted dx x
x) (Interpret Interpreted dy y
y) = Interpreted dz z -> Interpret dz z
forall dom (d :: dom) x. Interpreted d x -> Interpret d x
Interpret (Interpreted dz z -> Interpret dz z)
-> m (Interpreted dz z) -> m (Interpret dz z)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Interpreted dx x -> Interpreted dy y -> m (Interpreted dz z)
f Interpreted dx x
x Interpreted dy y
y
type HasNormalForm d x y = InterpretTo d (MetadataOf x) (MetadataOf y)
type family InterpretTo d xs ys :: Constraint where
InterpretTo _ '[] '[] = ()
InterpretTo d ('(f, x) ': xs) ('(f, y) ': ys) = IfEqual x (Interpreted d y)
(InterpretTo d xs ys)
type family IfEqual x y (r :: k) :: k where
IfEqual actual actual k = k
IfEqual expected actual k = TypeError (
'Text "Expected "
':<>: 'ShowType expected
':<>: 'Text " but got "
':<>: 'ShowType actual
)
normalize ::
HasNormalForm d x y
=> Proxy d
-> Proxy y
-> Rep I x -> Rep (Interpret d) y
normalize :: Proxy d -> Proxy y -> Rep I x -> Rep (Interpret d) y
normalize Proxy d
_ Proxy y
_ = Rep I x -> Rep (Interpret d) y
forall a b. a -> b
unsafeCoerce
denormalize ::
HasNormalForm d x y
=> Proxy d
-> Proxy y
-> Rep (Interpret d) y -> Rep I x
denormalize :: Proxy d -> Proxy y -> Rep (Interpret d) y -> Rep I x
denormalize Proxy d
_ Proxy y
_ = Rep (Interpret d) y -> Rep I x
forall a b. a -> b
unsafeCoerce
data Uninterpreted x
data DefaultInterpretation (f :: Type -> Type)
type instance Interpreted (DefaultInterpretation f) (Uninterpreted x) = f x
normalize1 :: forall d f x.
HasNormalForm (d f) (x f) (x Uninterpreted)
=> Proxy d
-> Rep I (x f) -> Rep (Interpret (d f)) (x Uninterpreted)
normalize1 :: Proxy d -> Rep I (x f) -> Rep (Interpret (d f)) (x Uninterpreted)
normalize1 Proxy d
_ = Proxy (d f)
-> Proxy (x Uninterpreted)
-> Rep I (x f)
-> Rep (Interpret (d f)) (x Uninterpreted)
forall dom (d :: dom) x y.
HasNormalForm d x y =>
Proxy d -> Proxy y -> Rep I x -> Rep (Interpret d) y
normalize (Proxy (d f)
forall k (t :: k). Proxy t
Proxy @(d f)) (Proxy (x Uninterpreted)
forall k (t :: k). Proxy t
Proxy @(x Uninterpreted))
denormalize1 :: forall d f x.
HasNormalForm (d f) (x f) (x Uninterpreted)
=> Proxy d
-> Rep (Interpret (d f)) (x Uninterpreted) -> Rep I (x f)
denormalize1 :: Proxy d -> Rep (Interpret (d f)) (x Uninterpreted) -> Rep I (x f)
denormalize1 Proxy d
_ = Proxy (d f)
-> Proxy (x Uninterpreted)
-> Rep (Interpret (d f)) (x Uninterpreted)
-> Rep I (x f)
forall dom (d :: dom) x y.
HasNormalForm d x y =>
Proxy d -> Proxy y -> Rep (Interpret d) y -> Rep I x
denormalize (Proxy (d f)
forall k (t :: k). Proxy t
Proxy @(d f)) (Proxy (x Uninterpreted)
forall k (t :: k). Proxy t
Proxy @(x Uninterpreted))
class StandardInterpretation d f where
standardInterpretation ::
Proxy d
-> ( Interpreted (d f) (Uninterpreted x) -> f x
, f x -> Interpreted (d f) (Uninterpreted x)
)
default standardInterpretation ::
Coercible (Interpreted (d f) (Uninterpreted x)) (f x)
=> Proxy d
-> ( Interpreted (d f) (Uninterpreted x) -> f x
, f x -> Interpreted (d f) (Uninterpreted x)
)
standardInterpretation Proxy d
_ = (Interpreted (d f) (Uninterpreted x) -> f x
coerce, f x -> Interpreted (d f) (Uninterpreted x)
coerce)
instance StandardInterpretation DefaultInterpretation f
toStandardInterpretation :: forall d f x.
StandardInterpretation d f
=> Proxy d
-> f x -> Interpret (d f) (Uninterpreted x)
toStandardInterpretation :: Proxy d -> f x -> Interpret (d f) (Uninterpreted x)
toStandardInterpretation Proxy d
d f x
fx = Interpreted (d f) (Uninterpreted x)
-> Interpret (d f) (Uninterpreted x)
forall dom (d :: dom) x. Interpreted d x -> Interpret d x
Interpret (Interpreted (d f) (Uninterpreted x)
-> Interpret (d f) (Uninterpreted x))
-> Interpreted (d f) (Uninterpreted x)
-> Interpret (d f) (Uninterpreted x)
forall a b. (a -> b) -> a -> b
$
(Interpreted (d f) (Uninterpreted x) -> f x,
f x -> Interpreted (d f) (Uninterpreted x))
-> f x -> Interpreted (d f) (Uninterpreted x)
forall a b. (a, b) -> b
snd (Proxy d
-> (Interpreted (d f) (Uninterpreted x) -> f x,
f x -> Interpreted (d f) (Uninterpreted x))
forall k dom (d :: (k -> *) -> dom) (f :: k -> *) (x :: k).
StandardInterpretation d f =>
Proxy d
-> (Interpreted (d f) (Uninterpreted x) -> f x,
f x -> Interpreted (d f) (Uninterpreted x))
standardInterpretation Proxy d
d) f x
fx
fromStandardInterpretation :: forall d f x.
StandardInterpretation d f
=> Proxy d
-> Interpret (d f) (Uninterpreted x) -> f x
fromStandardInterpretation :: Proxy d -> Interpret (d f) (Uninterpreted x) -> f x
fromStandardInterpretation Proxy d
d (Interpret Interpreted (d f) (Uninterpreted x)
fx) =
(Interpreted (d f) (Uninterpreted x) -> f x,
f x -> Interpreted (d f) (Uninterpreted x))
-> Interpreted (d f) (Uninterpreted x) -> f x
forall a b. (a, b) -> a
fst (Proxy d
-> (Interpreted (d f) (Uninterpreted x) -> f x,
f x -> Interpreted (d f) (Uninterpreted x))
forall k dom (d :: (k -> *) -> dom) (f :: k -> *) (x :: k).
StandardInterpretation d f =>
Proxy d
-> (Interpreted (d f) (Uninterpreted x) -> f x,
f x -> Interpreted (d f) (Uninterpreted x))
standardInterpretation Proxy d
d) Interpreted (d f) (Uninterpreted x)
fx