{-# LANGUAGE TypeFamilies, FlexibleContexts, Rank2Types, QuasiQuotes,
  TypeOperators, ScopedTypeVariables, GADTs, FlexibleInstances,
  MultiParamTypeClasses, UndecidableInstances #-}

{- |

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

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

An explicit perspective on (both parametric and ad-hoc) polymorphic
functions. The datatype representing such a function must be of kind @* -> *@;
the parameter is the type at which the function is to be instantiated.

-}

module Type.Yoko.Fun
  (Domain(..), Dom, Rng, applyU, apply,
   YieldsArrowTSSU, DomF, RngF, eachArrow,
   AsComp(..), WrapComp, WrapCompF
  ) where

import Type.Yoko.Type
import Type.Yoko.Universe
import Type.Yoko.Natural
import Type.Yoko.Sum
import Type.Yoko.BTree




-- | @Domain fn@ is the universe of types at which @fn@ can be applied; it's
-- the type-level domain of @fn@.
newtype Domain fn t = AppBy (fn t -> Dom fn t -> Rng fn t)

-- | @Dom fn t@ is the domain of @fn@ at type @t@; it's the term-level domain
-- of @fn@ at @t@.
type family Dom (fn :: * -> *) t
-- | @Rng fn t@ is the range of @fn@ at type @t@; it's the term-level range of
-- @fn@ at @t@.
type family Rng (fn :: * -> *) t

-- | @applyD@ is analogous to '$'.
applyU :: Domain fn t -> fn t -> Dom fn t -> Rng fn t
applyU (AppBy f) = f

-- | @apply = applyU inhabits@.
apply :: (t ::: Domain fn) => fn t -> Dom fn t -> Rng fn t
apply = applyU inhabits



-- | @YieldsArrowTSSU fn@ also gaurantees that @fn@ at @t@ yields a type of the
-- shape @(DomF fn) t -> (RngF fn) t@; i.e. it guarantees that @Dom fn t@ and
-- @Rng fn t@ both don't depend on @t@ and also are an application of a @* ->
-- *@ to @t@.
data YieldsArrowTSSU fn t where
  YieldsArrowTSSU ::
    (Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t
    ) => Domain fn t -> YieldsArrowTSSU fn t
instance (t ::: Domain fn, Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t
         ) => t ::: YieldsArrowTSSU fn where inhabits = YieldsArrowTSSU inhabits

-- | Used by @YieldsArrowTSSU fn@ to structure the domain of @fn@.
type family DomF (fn :: * -> *) :: * -> *
-- | Used by @YieldsArrowTSSU fn@ to structure the range of @fn@.
type family RngF (fn :: * -> *) :: * -> *

-- | Just a specialization: @yieldsArrowTSSU (YieldsArrowTSSU domD) fn = applyU domU fn@.
yieldsArrowTSSU :: YieldsArrowTSSU fn t -> (forall t. fn t) -> DomF fn t -> RngF fn t
yieldsArrowTSSU (YieldsArrowTSSU domU) fn = applyU domU fn

-- | Defines an @'NT' u@ from a suitably polymorphic type-function @fn@ if @u@
-- is finite and the function yields an arrow at each type in @u@.
eachArrow :: forall fn u.
  (Finite u, Inhabitants u ::: All (YieldsArrowTSSU fn)
  ) => (forall t. fn t) -> NT u (ArrowTSS (DomF fn) (RngF fn))
eachArrow fn = each [qP|YieldsArrowTSSU fn :: *->*|] $
  \d -> yieldsArrowTSSU d fn





type instance Dom (fn :. f) a = Dom fn (f a)
type instance Rng (fn :. f) a = Rng fn (f a)
type instance DomF (fn :. f) = DomF fn
type instance RngF (fn :. f) = RngF fn
instance (f t ::: Domain fn) => t ::: Domain (fn :. f) where
  inhabits = AppBy $ \(Compose fn) -> apply fn





-- | Only instance: @type instance WrapComp_ (f (g a)) = (f :. g) a@.
type WrapComp a = WrapComp_ a
type family WrapComp_ a
type instance WrapComp_ (f (g a)) = (f :. g) a

-- | Only instance: @type instance WrapCompF_ (f (g a)) = f :. g@.
type WrapCompF a = WrapCompF_ a
type family WrapCompF_ a :: * -> *
type instance WrapCompF_ (f (g a)) = f :. g





{- | Defining instances:

@
  type instance Dom (AsComp fn) t = WrapComp (Dom fn t)
  type instance Rng (AsComp fn) t = WrapComp (Rng fn t)
  inhabits = AppBy $ \(AsComp fn) -> wrap . apply fn . unwrap
@

-}
newtype AsComp (fn :: * -> *) t = AsComp (fn t)

type instance Unwrap (AsComp fn) t = fn t
instance Wrapper (AsComp fn) where wrap = AsComp; unwrap (AsComp x) = x

type instance Dom (AsComp fn) t = WrapComp (Dom fn t)
type instance Rng (AsComp fn) t = WrapComp (Rng fn t)

type instance DomF (AsComp fn) = WrapCompF (Dom fn ())
type instance RngF (AsComp fn) = WrapCompF (Rng fn ())

instance (t ::: Domain fn, Dom fn t ~ ex0 (ex1 ex2), Rng fn t ~ ex3 (ex4 ex5)
         ) => t ::: Domain (AsComp fn) where
  inhabits = AppBy $ \(AsComp fn) -> wrap . apply fn . unwrap