Injections.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Main
  ( main
  ) where

import Control.Applicative
import GHC.Generics
import Data.Proxy
import Data.Kind

class Sum (f :: Type -> Type) where
  type Q f x y :: Type
  k :: forall x y. (f () -> x) -> Q f x y -> y

instance Sum f => Sum (M1 i c f) where
  type Q (M1 i c f) x y = Q f x y
  k :: forall x y. (M1 i c f () -> x) -> Q f x y -> y
  k inj = k (inj . M1)

instance Sum U1 where
  type Q U1 x y = x -> y
  k :: forall x y. (U1 () -> x) -> (x -> y) -> y
  k inj f = f (inj U1)

instance Sum (K1 i t) where
  type Q (K1 i t) x y = (t -> x) -> y
  k :: forall x y. (K1 i t () -> x) -> ((t -> x) -> y) -> y
  k inj f = f (inj . K1)

instance (Sum f, Sum g) => Sum (f :+: g) where
  type Q (f :+: g) x y = Q f x (Q g x y)
  k :: forall x y. ((f :+: g) () -> x) -> Q f x (Q g x y) -> y
  k inj =
    let
      r0 = k @g @x @(      y) (inj . R1)
      l0 = k @f @x @(Q g x y) (inj . L1)
    in
      r0 . l0

withInjections :: forall t y. (Generic t, Sum (Rep t)) => Q (Rep t) t y -> y
withInjections = k @(Rep t) @t to

withInjections' :: forall t y. (Generic t, Sum (Rep t)) => Proxy t -> Q (Rep t) t y -> y
withInjections' _ = withInjections @t

kEither :: forall e a x. ((e -> Either e a) -> (a -> Either e a) -> x) -> x
kEither = withInjections' (Proxy @(Either e a))

data Either4 a b c d
  = E4_1 a
  | E4_2 b
  | E4_3 c
  | E4_4 d
  deriving (Generic, Show)

main :: IO ()
main = do
  withInjections @(Either Int Bool) \left right ->
    print [left 3, right False]

  withInjections @(Maybe Int) \nothing just ->
    print [nothing, just 3]

  withInjections @(Either4 Int Bool Char Double) \e1 e2 e3 e4 ->
    print [e1 3, e2 False, e3 'a', e4 3.14]