{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternSynonyms #-}
module Generics.Simplistic.Util
(
(&&&) , (***) , (:->) , (<.>)
, (:*:)(..) , Delta , curry' , uncurry' , delta , deltaMap
, Sum(..) , either' , either''
, Implies , Trivial
, EqHO(..) , ShowHO(..)
, Exists(..) , exMap , exMapM , exElim
, Elem , NotElem , HasElem(..) , ElemPrf(..) , IsElem, sameTy
, All , Witness(..) , witness , witnessPrf
, weq , wshow
) where
import Data.Kind (Constraint)
import Data.Proxy (Proxy(..))
import Data.Functor.Sum
import Data.Functor.Const
import Data.Type.Equality
import Control.Arrow ((***) , (&&&))
import GHC.Generics ((:*:)(..), V1 , U1(..))
curry' :: ((f :*: g) x -> a) -> f x -> g x -> a
curry' :: ((:*:) f g x -> a) -> f x -> g x -> a
curry' f :: (:*:) f g x -> a
f fx :: f x
fx gx :: g x
gx = (:*:) f g x -> a
f (f x
fx f x -> g x -> (:*:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g x
gx)
uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a
uncurry' :: (f x -> g x -> a) -> (:*:) f g x -> a
uncurry' f :: f x -> g x -> a
f (fx :: f x
fx :*: gx :: g x
gx) = f x -> g x -> a
f f x
fx g x
gx
type f :-> g = forall n . f n -> g n
type Delta f = f :*: f
delta :: f :-> Delta f
delta :: f n -> Delta f n
delta fx :: f n
fx = f n
fx f n -> f n -> Delta f n
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: f n
fx
deltaMap :: (f :-> g) -> Delta f :-> Delta g
deltaMap :: (f :-> g) -> Delta f :-> Delta g
deltaMap f :: f :-> g
f (x :: f n
x :*: y :: f n
y) = f n -> g n
f :-> g
f f n
x g n -> g n -> (:*:) g g n
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: f n -> g n
f :-> g
f f n
y
either' :: (f :-> r) -> (g :-> r) -> Sum f g :-> r
either' :: (f :-> r) -> (g :-> r) -> Sum f g :-> r
either' f :: f :-> r
f _ (InL x :: f n
x) = f n -> r n
f :-> r
f f n
x
either' _ g :: g :-> r
g (InR x :: g n
x) = g n -> r n
g :-> r
g g n
x
either'' :: (forall x . f x -> a) -> (forall y . g y -> a) -> Sum f g r -> a
either'' :: (forall (x :: k). f x -> a)
-> (forall (y :: k). g y -> a) -> Sum f g r -> a
either'' f :: forall (x :: k). f x -> a
f g :: forall (y :: k). g y -> a
g = Const a r -> a
forall a k (b :: k). Const a b -> a
getConst (Const a r -> a) -> (Sum f g r -> Const a r) -> Sum f g r -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f :-> Const a) -> (g :-> Const a) -> Sum f g :-> Const a
forall k (f :: k -> *) (r :: k -> *) (g :: k -> *).
(f :-> r) -> (g :-> r) -> Sum f g :-> r
either' (a -> Const a n
forall k a (b :: k). a -> Const a b
Const (a -> Const a n) -> (f n -> a) -> f n -> Const a n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f n -> a
forall (x :: k). f x -> a
f) (a -> Const a n
forall k a (b :: k). a -> Const a b
Const (a -> Const a n) -> (g n -> a) -> g n -> Const a n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g n -> a
forall (y :: k). g y -> a
g)
infixr 8 <.>
(<.>) :: (Monad m) => (b -> m c) -> (a -> m b) -> a -> m c
f :: b -> m c
f <.> :: (b -> m c) -> (a -> m b) -> a -> m c
<.> g :: a -> m b
g = (m b -> (b -> m c) -> m c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> m c
f) (m b -> m c) -> (a -> m b) -> a -> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m b
g
class (c => d) => Implies c d
instance (c => d) => Implies c d
class Trivial c
instance Trivial c
class EqHO (f :: ki -> *) where
eqHO :: forall k . f k -> f k -> Bool
instance Eq a => EqHO (Const a) where
eqHO :: Const a k -> Const a k -> Bool
eqHO (Const a :: a
a) (Const b :: a
b) = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
instance (EqHO f, EqHO g) => EqHO (f :*: g) where
eqHO :: (:*:) f g k -> (:*:) f g k -> Bool
eqHO (fx :: f k
fx :*: gx :: g k
gx) (fy :: f k
fy :*: gy :: g k
gy) = f k -> f k -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO f k
fx f k
fy Bool -> Bool -> Bool
&& g k -> g k -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO g k
gx g k
gy
instance (EqHO f, EqHO g) => EqHO (Sum f g) where
eqHO :: Sum f g k -> Sum f g k -> Bool
eqHO (InL fx :: f k
fx) (InL fy :: f k
fy) = f k -> f k -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO f k
fx f k
fy
eqHO (InR gx :: g k
gx) (InR gy :: g k
gy) = g k -> g k -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO g k
gx g k
gy
eqHO _ _ = Bool
False
instance EqHO V1 where
eqHO :: V1 k -> V1 k -> Bool
eqHO _ _ = Bool
True
instance EqHO U1 where
eqHO :: U1 k -> U1 k -> Bool
eqHO _ _ = Bool
True
class ShowHO (f :: ki -> *) where
showHO :: forall k . f k -> String
showsPrecHO :: forall k . Int -> f k -> ShowS
{-# MINIMAL showHO | showsPrecHO #-}
showHO fx :: f k
fx = Int -> f k -> ShowS
forall ki (f :: ki -> *) (k :: ki). ShowHO f => Int -> f k -> ShowS
showsPrecHO 0 f k
fx ""
showsPrecHO _ fx :: f k
fx s :: String
s = f k -> String
forall ki (f :: ki -> *) (k :: ki). ShowHO f => f k -> String
showHO f k
fx String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
instance Show a => ShowHO (Const a) where
showsPrecHO :: Int -> Const a k -> ShowS
showsPrecHO d :: Int
d (Const a :: a
a) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString "Const " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) a
a
where app_prec :: Int
app_prec = 10
instance (ShowHO f , ShowHO g) => ShowHO (f :*: g) where
showsPrecHO :: Int -> (:*:) f g k -> ShowS
showsPrecHO d :: Int
d (x :: f k
x :*: y :: g k
y) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
Int -> f k -> ShowS
forall ki (f :: ki -> *) (k :: ki). ShowHO f => Int -> f k -> ShowS
showsPrecHO (Int
app_precInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) f k
x
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " :*: "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> g k -> ShowS
forall ki (f :: ki -> *) (k :: ki). ShowHO f => Int -> f k -> ShowS
showsPrecHO (Int
app_precInt -> Int -> Int
forall a. Num a => a -> a -> a
+1) g k
y
where app_prec :: Int
app_prec = 10
instance (ShowHO f , ShowHO g) => ShowHO (Sum f g) where
showsPrecHO :: Int -> Sum f g k -> ShowS
showsPrecHO d :: Int
d (InL fx :: f k
fx) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString "InL " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f k -> ShowS
forall ki (f :: ki -> *) (k :: ki). ShowHO f => Int -> f k -> ShowS
showsPrecHO (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) f k
fx
where app_prec :: Int
app_prec = 10
showsPrecHO d :: Int
d (InR gx :: g k
gx) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString "InR " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> g k -> ShowS
forall ki (f :: ki -> *) (k :: ki). ShowHO f => Int -> f k -> ShowS
showsPrecHO (Int
app_prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) g k
gx
where app_prec :: Int
app_prec = 10
data Exists (f :: k -> *) :: * where
Exists :: f x -> Exists f
exMap :: (forall x . f x -> g x) -> Exists f -> Exists g
exMap :: (forall (x :: k). f x -> g x) -> Exists f -> Exists g
exMap f :: forall (x :: k). f x -> g x
f (Exists x :: f x
x) = g x -> Exists g
forall k (f :: k -> *) (x :: k). f x -> Exists f
Exists (f x -> g x
forall (x :: k). f x -> g x
f f x
x)
exMapM :: (Monad m) => (forall x . f x -> m (g x)) -> Exists f -> m (Exists g)
exMapM :: (forall (x :: k). f x -> m (g x)) -> Exists f -> m (Exists g)
exMapM f :: forall (x :: k). f x -> m (g x)
f (Exists x :: f x
x) = g x -> Exists g
forall k (f :: k -> *) (x :: k). f x -> Exists f
Exists (g x -> Exists g) -> m (g x) -> m (Exists g)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> m (g x)
forall (x :: k). f x -> m (g x)
f f x
x
exElim :: (forall x . f x -> a) -> Exists f -> a
exElim :: (forall (x :: k). f x -> a) -> Exists f -> a
exElim f :: forall (x :: k). f x -> a
f (Exists x :: f x
x) = f x -> a
forall (x :: k). f x -> a
f f x
x
instance ShowHO f => Show (Exists f) where
show :: Exists f -> String
show = (forall (x :: k). f x -> String) -> Exists f -> String
forall k (f :: k -> *) a.
(forall (x :: k). f x -> a) -> Exists f -> a
exElim forall (x :: k). f x -> String
forall ki (f :: ki -> *) (k :: ki). ShowHO f => f k -> String
showHO
type family IsElem (a :: k) (as :: [ k ]) :: Bool where
IsElem a (a ': as) = 'True
IsElem a (b ': as) = IsElem a as
IsElem a '[] = 'False
data ElemPrf a as where
Here :: ElemPrf a (a ': as)
There :: ElemPrf a as -> ElemPrf a (b ': as)
class HasElem a as where
hasElem :: ElemPrf a as
instance {-# OVERLAPPING #-} HasElem a (a ': as) where
hasElem :: ElemPrf a (a : as)
hasElem = ElemPrf a (a : as)
forall a (a :: a) (as :: [a]). ElemPrf a (a : as)
Here
instance {-# OVERLAPPABLE #-}
(HasElem a as) => HasElem a (b ': as) where
hasElem :: ElemPrf a (b : as)
hasElem = ElemPrf a as -> ElemPrf a (b : as)
forall a (a :: a) (as :: [a]) (b :: a).
ElemPrf a as -> ElemPrf a (b : as)
There ElemPrf a as
forall k (a :: k) (as :: [k]). HasElem a as => ElemPrf a as
hasElem
type Elem a as = (IsElem a as ~ 'True , HasElem a as)
type NotElem a as = IsElem a as ~ 'False
sameTy :: forall fam x y . (Elem x fam , Elem y fam)
=> Proxy fam -> Proxy x -> Proxy y -> Maybe (x :~: y)
sameTy :: Proxy fam -> Proxy x -> Proxy y -> Maybe (x :~: y)
sameTy _ _ _ = ElemPrf x fam -> ElemPrf y fam -> Maybe (x :~: y)
forall (fam' :: [k]) (b :: k).
ElemPrf x fam' -> ElemPrf b fam' -> Maybe (x :~: b)
go (ElemPrf x fam
forall k (a :: k) (as :: [k]). HasElem a as => ElemPrf a as
hasElem :: ElemPrf x fam) (ElemPrf y fam
forall k (a :: k) (as :: [k]). HasElem a as => ElemPrf a as
hasElem :: ElemPrf y fam)
where
go :: ElemPrf x fam' -> ElemPrf b fam' -> Maybe (x :~: b)
go :: ElemPrf x fam' -> ElemPrf b fam' -> Maybe (x :~: b)
go Here Here = (x :~: x) -> Maybe (x :~: x)
forall a. a -> Maybe a
Just x :~: x
forall k (a :: k). a :~: a
Refl
go (There rr :: ElemPrf x as
rr) (There y :: ElemPrf b as
y) = ElemPrf x as -> ElemPrf b as -> Maybe (x :~: b)
forall (fam' :: [k]) (b :: k).
ElemPrf x fam' -> ElemPrf b fam' -> Maybe (x :~: b)
go ElemPrf x as
rr ElemPrf b as
ElemPrf b as
y
go _ _ = Maybe (x :~: b)
forall a. Maybe a
Nothing
type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where
All c '[] = ()
All c (x ': xs) = (c x , All c xs)
data Witness c x where
Witness :: (c x) => Witness c x
witness :: forall x xs c
. (HasElem x xs , All c xs)
=> Proxy xs -> Witness c x
witness :: Proxy xs -> Witness c x
witness _ = ElemPrf x xs -> Witness c x
forall k (c :: k -> Constraint) (xs :: [k]) (x :: k).
All c xs =>
ElemPrf x xs -> Witness c x
witnessPrf (ElemPrf x xs
forall k (a :: k) (as :: [k]). HasElem a as => ElemPrf a as
hasElem :: ElemPrf x xs)
weq :: forall x xs
. (All Eq xs , Elem x xs)
=> Proxy xs -> x -> x -> Bool
weq :: Proxy xs -> x -> x -> Bool
weq p :: Proxy xs
p = case Proxy xs -> Witness Eq x
forall k (x :: k) (xs :: [k]) (c :: k -> Constraint).
(HasElem x xs, All c xs) =>
Proxy xs -> Witness c x
witness Proxy xs
p :: Witness Eq x of
Witness -> x -> x -> Bool
forall a. Eq a => a -> a -> Bool
(==)
wshow :: forall x xs
. (All Show xs , Elem x xs)
=> Proxy xs -> x -> String
wshow :: Proxy xs -> x -> String
wshow p :: Proxy xs
p = case Proxy xs -> Witness Show x
forall k (x :: k) (xs :: [k]) (c :: k -> Constraint).
(HasElem x xs, All c xs) =>
Proxy xs -> Witness c x
witness Proxy xs
p :: Witness Show x of
Witness -> x -> String
forall a. Show a => a -> String
show
witnessPrf :: (All c xs) => ElemPrf x xs -> Witness c x
witnessPrf :: ElemPrf x xs -> Witness c x
witnessPrf Here = Witness c x
forall k (c :: k -> Constraint) (x :: k). c x => Witness c x
Witness
witnessPrf (There p :: ElemPrf x as
p) = ElemPrf x as -> Witness c x
forall k (c :: k -> Constraint) (xs :: [k]) (x :: k).
All c xs =>
ElemPrf x xs -> Witness c x
witnessPrf ElemPrf x as
p