{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
module Data.Registry.Lift where
import Protolude hiding (Nat)
import Data.Type.Equality
class Applicative f => ApplyVariadic f a b where
applyVariadic :: f a -> b
instance {-# OVERLAPPABLE #-} (Applicative f, b ~ f a) => ApplyVariadic f a b where
applyVariadic :: f a -> b
applyVariadic = f a -> b
f a -> f a
forall a. a -> a
identity
instance (Monad f, b ~ f a) => ApplyVariadic f (f a) b where
applyVariadic :: f (f a) -> b
applyVariadic = f (f a) -> b
f (f a) -> f a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join
instance {-# OVERLAPPING #-} (Applicative f, ApplyVariadic f a' b', b ~ (f a -> b')) => ApplyVariadic f (a -> a') b where
applyVariadic :: f (a -> a') -> b
applyVariadic f (a -> a')
f f a
fa = f a' -> b'
forall (f :: * -> *) a b. ApplyVariadic f a b => f a -> b
applyVariadic (f (a -> a')
f f (a -> a') -> f a -> f a'
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f a
fa)
allTo :: forall f a b. ApplyVariadic f a b => a -> b
allTo :: forall (f :: * -> *) a b. ApplyVariadic f a b => a -> b
allTo a
a = (f a -> b
forall (f :: * -> *) a b. ApplyVariadic f a b => f a -> b
applyVariadic :: f a -> b) (a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a)
class Monad f => ApplyVariadic1 f a b where
applyVariadic1 :: f a -> b
instance (Monad f, b ~ f a) => ApplyVariadic1 f (f a) b where
applyVariadic1 :: f (f a) -> b
applyVariadic1 = f (f a) -> b
f (f a) -> f a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join
instance (Monad f, ApplyVariadic1 f a' b', b ~ (f a -> b')) => ApplyVariadic1 f (a -> a') b where
applyVariadic1 :: f (a -> a') -> b
applyVariadic1 f (a -> a')
f f a
fa = f a' -> b'
forall (f :: * -> *) a b. ApplyVariadic1 f a b => f a -> b
applyVariadic1 (f (a -> a')
f f (a -> a') -> f a -> f a'
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f a
fa)
argsTo :: forall f a b. ApplyVariadic1 f a b => a -> b
argsTo :: forall (f :: * -> *) a b. ApplyVariadic1 f a b => a -> b
argsTo a
a = (f a -> b
forall (f :: * -> *) a b. ApplyVariadic1 f a b => f a -> b
applyVariadic1 :: f a -> b) (a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a)
class ApplyVariadic2 f g a b where
applyVariadic2 :: (forall x. f x -> g x) -> a -> b
instance (b ~ g a) => ApplyVariadic2 f g (f a) b where
applyVariadic2 :: (forall (x :: k). f x -> g x) -> f a -> b
applyVariadic2 forall (x :: k). f x -> g x
natfg = f a -> b
f a -> g a
forall (x :: k). f x -> g x
natfg
instance (ApplyVariadic2 f g a' b', b ~ (a -> b')) => ApplyVariadic2 f g (a -> a') b where
applyVariadic2 :: (forall (x :: k). f x -> g x) -> (a -> a') -> b
applyVariadic2 forall (x :: k). f x -> g x
natfg a -> a'
f a
a = (forall (x :: k). f x -> g x) -> a' -> b'
forall {k} (f :: k -> *) (g :: k -> *) a b.
ApplyVariadic2 f g a b =>
(forall (x :: k). f x -> g x) -> a -> b
applyVariadic2 f x -> g x
forall (x :: k). f x -> g x
natfg (a -> a'
f a
a)
outTo :: forall g f a b. ApplyVariadic2 f g a b => (forall x. f x -> g x) -> a -> b
outTo :: forall {k} (g :: k -> *) (f :: k -> *) a b.
ApplyVariadic2 f g a b =>
(forall (x :: k). f x -> g x) -> a -> b
outTo forall (x :: k). f x -> g x
natfg = (forall (x :: k). f x -> g x) -> a -> b
forall {k} (f :: k -> *) (g :: k -> *) a b.
ApplyVariadic2 f g a b =>
(forall (x :: k). f x -> g x) -> a -> b
applyVariadic2 f x -> g x
forall (x :: k). f x -> g x
natfg :: a -> b
newtype Tag (s :: Symbol) a = Tag {forall (s :: Symbol) a. Tag s a -> a
unTag :: a} deriving (Tag s a -> Tag s a -> Bool
(Tag s a -> Tag s a -> Bool)
-> (Tag s a -> Tag s a -> Bool) -> Eq (Tag s a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (s :: Symbol) a. Eq a => Tag s a -> Tag s a -> Bool
$c== :: forall (s :: Symbol) a. Eq a => Tag s a -> Tag s a -> Bool
== :: Tag s a -> Tag s a -> Bool
$c/= :: forall (s :: Symbol) a. Eq a => Tag s a -> Tag s a -> Bool
/= :: Tag s a -> Tag s a -> Bool
Eq, Int -> Tag s a -> ShowS
[Tag s a] -> ShowS
Tag s a -> String
(Int -> Tag s a -> ShowS)
-> (Tag s a -> String) -> ([Tag s a] -> ShowS) -> Show (Tag s a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (s :: Symbol) a. Show a => Int -> Tag s a -> ShowS
forall (s :: Symbol) a. Show a => [Tag s a] -> ShowS
forall (s :: Symbol) a. Show a => Tag s a -> String
$cshowsPrec :: forall (s :: Symbol) a. Show a => Int -> Tag s a -> ShowS
showsPrec :: Int -> Tag s a -> ShowS
$cshow :: forall (s :: Symbol) a. Show a => Tag s a -> String
show :: Tag s a -> String
$cshowList :: forall (s :: Symbol) a. Show a => [Tag s a] -> ShowS
showList :: [Tag s a] -> ShowS
Show)
instance Functor (Tag s) where
fmap :: forall a b. (a -> b) -> Tag s a -> Tag s b
fmap a -> b
f (Tag a
a) = forall (s :: Symbol) a. a -> Tag s a
Tag @s (a -> b
f a
a)
instance Applicative (Tag s) where
pure :: forall a. a -> Tag s a
pure = a -> Tag s a
forall (s :: Symbol) a. a -> Tag s a
Tag
Tag a -> b
f <*> :: forall a b. Tag s (a -> b) -> Tag s a -> Tag s b
<*> Tag a
a = forall (s :: Symbol) a. a -> Tag s a
Tag @s (a -> b
f a
a)
tag :: forall (s :: Symbol) fun. (CNumArgs (CountArgs fun) fun) => fun -> Apply (Tag s) (CountArgs fun) fun
tag :: forall (s :: Symbol) fun.
CNumArgs (CountArgs fun) fun =>
fun -> Apply (Tag s) (CountArgs fun) fun
tag = forall (f :: * -> *) fun.
(Applicative f, CNumArgs (CountArgs fun) fun) =>
fun -> Apply f (CountArgs fun) fun
applyLast @(Tag s)
data Nat = Z | S Nat
data NumArgs :: Nat -> Type -> Type where
NAZ :: NumArgs Z a
NAS :: NumArgs n b -> NumArgs (S n) (a -> b)
type family CountArgs (f :: Type) :: Nat where
CountArgs (a -> b) = S (CountArgs b)
CountArgs result = Z
class CNumArgs (numArgs :: Nat) (arrows :: Type) where
getNA :: NumArgs numArgs arrows
instance CNumArgs Z a where
getNA :: NumArgs 'Z a
getNA = NumArgs 'Z a
forall a. NumArgs 'Z a
NAZ
instance CNumArgs n b => CNumArgs (S n) (a -> b) where
getNA :: NumArgs ('S n) (a -> b)
getNA = NumArgs n b -> NumArgs ('S n) (a -> b)
forall (n :: Nat) b a. NumArgs n b -> NumArgs ('S n) (a -> b)
NAS NumArgs n b
forall (numArgs :: Nat) arrows.
CNumArgs numArgs arrows =>
NumArgs numArgs arrows
getNA
type family Apply (f :: Type -> Type) (n :: Nat) (arrows :: Type) :: Type where
Apply f (S n) (a -> b) = a -> Apply f n b
Apply f Z a = f a
applyLast :: forall f fun. (Applicative f, CNumArgs (CountArgs fun) fun) => fun -> Apply f (CountArgs fun) fun
applyLast :: forall (f :: * -> *) fun.
(Applicative f, CNumArgs (CountArgs fun) fun) =>
fun -> Apply f (CountArgs fun) fun
applyLast = forall (f' :: * -> *) (n :: Nat) fun'.
Applicative f' =>
NumArgs n fun' -> fun' -> Apply f' n fun'
applyLast' @f (NumArgs (CountArgs fun) fun
forall (numArgs :: Nat) arrows.
CNumArgs numArgs arrows =>
NumArgs numArgs arrows
getNA :: NumArgs (CountArgs fun) fun)
where
applyLast' :: forall f' n fun'. Applicative f' => NumArgs n fun' -> fun' -> Apply f' n fun'
applyLast' :: forall (f' :: * -> *) (n :: Nat) fun'.
Applicative f' =>
NumArgs n fun' -> fun' -> Apply f' n fun'
applyLast' NumArgs n fun'
NAZ fun'
x = fun' -> f' fun'
forall a. a -> f' a
forall (f :: * -> *) a. Applicative f => a -> f a
pure fun'
x
applyLast' (NAS NumArgs n b
n) fun'
f = forall (f' :: * -> *) (n :: Nat) fun'.
Applicative f' =>
NumArgs n fun' -> fun' -> Apply f' n fun'
applyLast' @f' NumArgs n b
n (b -> Apply f' n b) -> (a -> b) -> a -> Apply f' n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. fun'
a -> b
f