module Data.Kind.Extra
( type A(..)
, type IsA
, type IsAn
, type Return
, type Pure
, type Eval
, type (:->)
, type Id
, type Apply
, type (^*^)
, type ($~)
, type (:>>=:)
, type (:>>>:)
, type (:^>>>:)
, type (:>>>^:)
, type (:^>>>^:)
, type Extract
, type Optional
, type FoldMap
, type Fun1
, type Fun2
, type Fun3
, type Fun4
) where
import Data.Kind (type Type)
data A :: forall foo . foo -> Type where
MkA :: A foo
type IsA (foo :: k) = (A foo -> Type :: Type)
type IsAn (oo :: k) = (IsA oo :: Type)
type family Eval (t :: A foo -> Type) :: foo
data Pure (f :: o) :: IsAn o
type instance Eval (Pure f) = f
type Return f = Pure f
data (:->) foo bar
type family (f :: IsA (foo :-> bar)) $~ (x :: foo) :: bar
infixl 0 $~
type Apply f x = f $~ x
data Id :: IsA (foo :-> foo)
type instance Id $~ x = x
type (^*^) (f :: IsA (foo :-> bar)) (x :: IsA foo) = f $~ (Eval x)
infixl 0 ^*^
data (:>>>:) :: IsA (good :-> better) -> IsA (better :-> best) -> IsA (good :-> best)
infixl 1 :>>>:
type instance (f :>>>: g) $~ x = g $~ (f $~ x)
data (:^>>>:) :: IsA (good :-> better) -> IsA (better :-> best) -> IsA (IsA good :-> best)
infixl 1 :^>>>:
type instance (f :^>>>: g) $~ x = g $~ (f $~ Eval x)
data (:>>>^:) :: IsA (good :-> better) -> IsA (better :-> best) -> IsA (good :-> IsA best)
infixl 1 :>>>^:
type instance (f :>>>^: g) $~ x = Return (g $~ (f $~ x))
data (:^>>>^:) :: IsA (good :-> better) -> IsA (better :-> best) -> IsA (IsA good :-> IsA best)
infixl 1 :^>>>^:
type instance (f :^>>>^: g) $~ x = Return (g $~ (f $~ Eval x))
data Extract :: IsA (IsA x :-> x)
type instance Extract $~ x = Eval x
data (:>>=:) :: IsA foo -> IsA (foo :-> IsA bar) -> IsA bar
infixl 1 :>>=:
type instance Eval (x :>>=: f) = Eval (f $~ Eval x)
data Optional :: IsA t -> IsA (s :-> IsA t) -> IsA (Maybe s :-> IsA t)
type instance (Optional fallback f) $~ ('Just s) = f $~ s
type instance (Optional fallback f) $~ 'Nothing = fallback
type family
FoldMap
(append :: IsA (bar :-> IsA (bar :-> bar)))
(zero :: bar)
(f :: IsA (foo :-> bar))
(xs :: [(foo :: Type)]) :: (bar :: Type) where
FoldMap append zero f '[] = zero
FoldMap append zero f (x ': xs) = append $~ (f $~ x) $~ FoldMap append zero f xs
data Fun1 :: (a -> IsA b)
-> IsA (a :-> IsA b)
type instance (Fun1 f) $~ x = (f x)
data Fun2 :: (a -> b -> IsA c)
-> IsA (a :-> IsA (b :-> IsA c))
type instance (Fun2 f) $~ x = Fun1 (f x)
data Fun3 :: (a -> b -> c -> IsA d)
-> IsA (a :-> IsA (b :-> IsA (c :-> IsA d)))
type instance (Fun3 f) $~ x = Fun2 (f x)
data Fun4 :: (a -> b -> c -> d -> IsAn e)
-> IsA (a :-> IsA (b :-> IsA (c :-> IsA (d :-> IsAn e))))
type instance (Fun4 f) $~ x = Fun3 (f x)