Natural.hs

{-# LANGUAGE ExistentialQuantification, QuasiQuotes, TypeOperators,
  Rank2Types, GADTs, ScopedTypeVariables, TypeFamilies #-}

{- |

Module      :  Type.Yoko.Natural
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Natural transformations and pairs.

-}

module Type.Yoko.Natural where

import Type.Yoko.Type
import Type.Yoko.Universe



type NT_ u f = forall t. u t -> f t

-- | Natural transformations. We use 'Unwrap' to lighten the user interface at
-- the value level, though it clutters the types a little.
newtype NT u f = NT (forall t. u t -> Unwrap f t)

nt_ :: [qP|f :: *->*|] -> (forall t. u t -> Unwrap f t) -> NT u f
nt_ p f = NT f


appNT :: NT u f -> u t -> Unwrap f t
appNT (NT f) x = f x

appNTF :: Wrapper f => NT u f -> NT_ u f
appNTF (NT f) x = wrap (f x)


-- | Defining an @NT@ via type-level backtracking; ':||' uses 'Pred' to
-- short-circuit, preferring inhabitation of @u@ over @v@.
orNT :: NT u f -> NT v f -> NT (u :|| v) f
orNT (NT f) (NT g) = NT $ \uv -> case uv of
  LeftU  u -> f u
  RightU v -> g v


constNT :: Unwrap f t -> NT ((:=:) t) f
constNT = constNT_ Proxy

constNT_ :: [qP|f :: *->*|] -> Unwrap f t -> NT ((:=:) t) f
constNT_ p x = nt_ p $ \Refl -> x

constNTF :: Wrapper f => f t -> NT ((:=:) t) f
constNTF x = NT $ \Refl -> unwrap x


firstNT :: NT_ u g -> NT g f -> NT u f
firstNT g (NT f) = NT $ f . g





-- | Natural pairs.
data NP u f = forall t. NP (u t) (Unwrap f t)

-- | Analog to "Control.Arrow"@.first@.
firstNP :: NT_ u v -> NP u f -> NP v f
firstNP f (NP u x) = NP (f u) x


-- | @ArrowTSS@ can be partially applied, and hence occur as the second
-- argument of @NT@, where as @f _ -> g _@ cannot.
newtype ArrowTSS f g a = ArrowTSS (f a -> g a)
type instance Unwrap (ArrowTSS f g) a = f a -> g a
instance Wrapper (ArrowTSS f g) where wrap = ArrowTSS; unwrap (ArrowTSS f) = f

appNTtoNP :: (Wrapper f, Wrapper g) => NT u (ArrowTSS f g) -> NP u f -> NP u g
appNTtoNP (NT f) (NP u x) = NP u $ unwrap $ f u $ wrap x