Main.purs

module Main where

import Data.Either (Either(Left, Right))
import Data.Tuple (Tuple(Tuple))
import Data.Unit (Unit, unit)
import Data.Void (Void, absurd)
import Type.Proxy (Proxy(Proxy))

class Function f a b | f -> a b where
  apply :: Proxy f -> a -> b

class Function f a b <= Injective f a b -- where

applyInjective :: forall a b f. Injective f a b => a -> b
applyInjective = apply (Proxy :: Proxy f)

class Function f a b <= Surjective f a b -- where

applySurjective :: forall a b f. Surjective f a b => a -> b
applySurjective = apply (Proxy :: Proxy f)

class (Injective f a b, Surjective f a b) <= Bijective f a b -- where

applyBijective :: forall a b f. Bijective f a b => a -> b
applyBijective = apply (Proxy :: Proxy f)

instance bijective :: (Injective f a b, Surjective f a b) => Bijective f a b

data Identity a

instance functionIdentity :: Function (Identity a) a a where
  apply _ x = x

instance injectiveIdentity :: Injective (Identity a) a a

instance surjectiveIdentity :: Surjective (Identity a) a a

instance bijectiveIdentity :: Bijective (Identity a) a a

data Terminal a

instance functionTerminal :: Function (Terminal a) a Unit where
  apply _ _ = unit

instance surjectiveTerminal :: Surjective (Terminal a) a Unit

data Initial a

instance functionInitial :: Function (Initial Void) Void a where
  apply _ = absurd

instance injectiveInitial :: Injective (Initial Void) Void a

data First a b

instance functionFirst :: Function (First a b) (Tuple a b) a where
  apply _ (Tuple x _) = x

instance surjectiveFirst :: Surjective (First a b) (Tuple a b) a

data Second a b

instance functionSecond :: Function (Second a b) (Tuple a b) b where
  apply _ (Tuple _ x) = x

instance surjectiveSecond :: Surjective (Second a b) (Tuple a b) b

data Left a b

instance functionLeft :: Function (Left a b) a (Either a b) where
  apply _ x = Left x

instance injectiveLeft :: Injective (Left a b) a (Either a b)

data Right a b

instance functionRight :: Function (Right a b) b (Either a b) where
  apply _ x = Right x

instance injectiveRight :: Injective (Right a b) b (Either a b)