{-# LANGUAGE UndecidableInstances #-}
module Data.Kind.Extra
( type Extends
, type Konst
, (:~:)
, type From
, type Apply
, Labelled
, Named
, Name
, type (:#)
, Anonymous
, 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)
import Data.Type.Equality ((:~:))
import GHC.TypeLits (Symbol)
type Extends a = (a -> Type :: Type)
type family From (t :: a -> Type) :: a
type Konst (a :: k) = ((:~:) a :: Extends k)
type instance From ((:~:) a) = a
data Named s
data Name :: Symbol -> Extends s -> Extends (Named s)
type (name :: Symbol) :# (x :: Extends s) = Name name x
infixr 7 :#
data Anonymous (x :: Extends (Named s)) :: Extends s
data Labelled (s :: Symbol) :: Extends a -> Extends a
type instance From (Labelled s t) = From t
type family Apply (f :: Extends (a -> b)) (x :: a) :: b
type f $ x = Apply f x
data (:>>>:) :: Extends (good -> better) -> Extends (better -> best) -> Extends (good -> best)
infixl 1 :>>>:
type instance Apply (f :>>>: g) x = g $ (f $ x)
data (:^>>>:) :: Extends (good -> better) -> Extends (better -> best) -> Extends (Extends good -> best)
infixl 1 :^>>>:
type instance Apply (f :^>>>: g) x = g $ (f $ From x)
data (:>>>^:) :: Extends (good -> better) -> Extends (better -> best) -> Extends (good -> Extends best)
infixl 1 :>>>^:
type instance Apply (f :>>>^: g) x = Konst (g $ (f $ x))
data Extract :: Extends (Extends x -> x)
type instance Apply Extract x = From x
data (:>>=:) :: Extends a -> Extends (a -> Extends b) -> Extends b
infixl 1 :>>=:
type instance From (x :>>=: f) = From (f $ From x)
data Optional :: Extends t -> Extends (s -> Extends t) -> Extends (Maybe s -> Extends t)
type instance Apply (Optional fallback f) ('Just s) = f $ s
type instance Apply (Optional fallback f) 'Nothing = fallback
type family
FoldMap
(append :: Extends (b -> Extends (b -> b)))
(zero :: b)
(f :: Extends (a -> b))
(xs :: [(a :: Type)]) :: (b :: Type) where
FoldMap append zero f '[] = zero
FoldMap append zero f (x ': xs) = append $ (f $ x) $ FoldMap append zero f xs
data Fun1 :: (a -> Extends b)
-> Extends (a -> Extends b)
type instance Apply (Fun1 f) x = (f x)
data Fun2 :: (a -> b -> Extends c)
-> Extends (a -> Extends (b -> Extends c))
type instance Apply (Fun2 f) x = Fun1 (f x)
data Fun3 :: (a -> b -> c -> Extends d)
-> Extends (a -> Extends (b -> Extends (c -> Extends d)))
type instance Apply (Fun3 f) x = Fun2 (f x)
data Fun4 :: (a -> b -> c -> d -> Extends e)
-> Extends (a -> Extends (b -> Extends (c -> Extends (d -> Extends e))))
type instance Apply (Fun4 f) x = Fun3 (f x)