{-# LANGUAGE EmptyCase, LambdaCase, TypeOperators, GADTs, TypeFamilies, NoImplicitPrelude #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Void
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.Void where

import Data.Kind (Type)

import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation


data Void a b

magic :: Void a b -> x
magic :: forall a b x. Void a b -> x
magic = \case { }

-- | `Void` is the category with no objects.
instance Category Void where

  src :: forall a b. Void a b -> Obj Void a
src = forall a b x. Void a b -> x
magic
  tgt :: forall a b. Void a b -> Obj Void b
tgt = forall a b x. Void a b -> x
magic

  . :: forall b c a. Void b c -> Void a b -> Void a c
(.) = forall a b x. Void a b -> x
magic


voidNat :: (Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)
  => f -> g -> Nat Void d f g
voidNat :: forall f g (d :: * -> * -> *).
(Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d,
 Cod g ~ d) =>
f -> g -> Nat Void d f g
voidNat f
f g
g = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f g
g forall a b x. Void a b -> x
magic


data Magic (k :: Type -> Type -> Type) = Magic
-- | Since there is nothing to map in `Void`, there's a functor from it to any other category.
instance Category k => Functor (Magic k) where
  type Dom (Magic k) = Void
  type Cod (Magic k) = k

  Magic k
Magic % :: forall a b.
Magic k
-> Dom (Magic k) a b -> Cod (Magic k) (Magic k :% a) (Magic k :% b)
% Dom (Magic k) a b
f = forall a b x. Void a b -> x
magic Dom (Magic k) a b
f