{-|
Module      : Data.Void.HKT
Description : A poly-kinded uninhabited type.
Copyright   : ©2020 James Alexander Feldman-Crough
License     : MPL-2.0
Maintainer  : alex@fldcr.com
-}
{-# OPTIONS_GHC -Wno-unused-binds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
module Data.Void.HKT (Void, Uninhabited(..)) where

import           Data.Profunctor                ( Profunctor(..)
                                                , Strong(..)
                                                , Choice(..)
                                                )
import           Data.Bifunctor                 ( Bifunctor(..) )

-- | A poly-kinded, uninhabited type family.
data family Void :: k

-- | The uninhabited type taking no arguments.
data instance Void

-- | The uninhabited type taking one argument.
newtype instance Void (a :: ka) = Void1 Void

-- | The uninhabited type taking two arguments.
newtype instance Void (a :: ka) (b :: kb) = Void2 Void

-- | The uninhabited type taking three arguments.
newtype instance Void (a :: ka) (b :: kb) (c :: kc) = Void3 Void

-- | Defines uninhabited types.
class Uninhabited a where
    -- | If @a@ is an uninhabited type, we will never receive a value of type
    -- @a@ and thus we can return a value of any type.
    absurd :: a -> b

instance Uninhabited Void where
    absurd :: Void -> b
absurd = \case {}

instance Uninhabited (Void a) where
    absurd :: Void a -> b
absurd = \case {}

instance Uninhabited (Void a b) where
    absurd :: Void a b -> b
absurd = \case {}

instance Uninhabited (Void a b c) where
    absurd :: Void a b c -> b
absurd = \case {}

instance Functor Void where
    fmap :: (a -> b) -> Void a -> Void b
fmap = (Void a -> Void b) -> (a -> b) -> Void a -> Void b
forall a b. a -> b -> a
const Void a -> Void b
forall a b. Uninhabited a => a -> b
absurd

instance Functor (Void a) where
    fmap :: (a -> b) -> Void a a -> Void a b
fmap = (Void a a -> Void a b) -> (a -> b) -> Void a a -> Void a b
forall a b. a -> b -> a
const Void a a -> Void a b
forall a b. Uninhabited a => a -> b
absurd

instance Functor (Void a b) where
    fmap :: (a -> b) -> Void a b a -> Void a b b
fmap = (Void a b a -> Void a b b) -> (a -> b) -> Void a b a -> Void a b b
forall a b. a -> b -> a
const Void a b a -> Void a b b
forall a b. Uninhabited a => a -> b
absurd

instance Bifunctor Void where
    bimap :: (a -> b) -> (c -> d) -> Void a c -> Void b d
bimap = ((c -> d) -> Void a c -> Void b d)
-> (a -> b) -> (c -> d) -> Void a c -> Void b d
forall a b. a -> b -> a
const ((Void a c -> Void b d) -> (c -> d) -> Void a c -> Void b d
forall a b. a -> b -> a
const Void a c -> Void b d
forall a b. Uninhabited a => a -> b
absurd)

instance Bifunctor (Void a) where
    bimap :: (a -> b) -> (c -> d) -> Void a a c -> Void a b d
bimap = ((c -> d) -> Void a a c -> Void a b d)
-> (a -> b) -> (c -> d) -> Void a a c -> Void a b d
forall a b. a -> b -> a
const ((Void a a c -> Void a b d) -> (c -> d) -> Void a a c -> Void a b d
forall a b. a -> b -> a
const Void a a c -> Void a b d
forall a b. Uninhabited a => a -> b
absurd)

instance Profunctor Void where
    dimap :: (a -> b) -> (c -> d) -> Void b c -> Void a d
dimap = ((c -> d) -> Void b c -> Void a d)
-> (a -> b) -> (c -> d) -> Void b c -> Void a d
forall a b. a -> b -> a
const ((Void b c -> Void a d) -> (c -> d) -> Void b c -> Void a d
forall a b. a -> b -> a
const Void b c -> Void a d
forall a b. Uninhabited a => a -> b
absurd)

instance Profunctor (Void a) where
    dimap :: (a -> b) -> (c -> d) -> Void a b c -> Void a a d
dimap = ((c -> d) -> Void a b c -> Void a a d)
-> (a -> b) -> (c -> d) -> Void a b c -> Void a a d
forall a b. a -> b -> a
const ((Void a b c -> Void a a d) -> (c -> d) -> Void a b c -> Void a a d
forall a b. a -> b -> a
const Void a b c -> Void a a d
forall a b. Uninhabited a => a -> b
absurd)

instance Strong Void where
    first' :: Void a b -> Void (a, c) (b, c)
first'  = Void a b -> Void (a, c) (b, c)
forall a b. Uninhabited a => a -> b
absurd
    second' :: Void a b -> Void (c, a) (c, b)
second' = Void a b -> Void (c, a) (c, b)
forall a b. Uninhabited a => a -> b
absurd

instance Strong (Void a) where
    first' :: Void a a b -> Void a (a, c) (b, c)
first'  = Void a a b -> Void a (a, c) (b, c)
forall a b. Uninhabited a => a -> b
absurd
    second' :: Void a a b -> Void a (c, a) (c, b)
second' = Void a a b -> Void a (c, a) (c, b)
forall a b. Uninhabited a => a -> b
absurd

instance Choice Void where
    left' :: Void a b -> Void (Either a c) (Either b c)
left'  = Void a b -> Void (Either a c) (Either b c)
forall a b. Uninhabited a => a -> b
absurd
    right' :: Void a b -> Void (Either c a) (Either c b)
right' = Void a b -> Void (Either c a) (Either c b)
forall a b. Uninhabited a => a -> b
absurd

instance Choice (Void a) where
    left' :: Void a a b -> Void a (Either a c) (Either b c)
left'  = Void a a b -> Void a (Either a c) (Either b c)
forall a b. Uninhabited a => a -> b
absurd
    right' :: Void a a b -> Void a (Either c a) (Either c b)
right' = Void a a b -> Void a (Either c a) (Either c b)
forall a b. Uninhabited a => a -> b
absurd