{-# 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, applyD, apply, YieldsArrowTSSD, 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 '$'. applyD :: Domain fn t -> fn t -> Dom fn t -> Rng fn t applyD (AppBy f) = f -- | @apply = applyD inhabits@. apply :: (t ::: Domain fn) => fn t -> Dom fn t -> Rng fn t apply = applyD inhabits -- | @YieldsArrowTSSD 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 YieldsArrowTSSD fn t where YieldsArrowTSSD :: (Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t ) => Domain fn t -> YieldsArrowTSSD fn t instance (t ::: Domain fn, Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t ) => t ::: YieldsArrowTSSD fn where inhabits = YieldsArrowTSSD inhabits -- | Used by @YieldsArrowTSSD fn@ to structure the domain of @fn@. type family DomF (fn :: * -> *) :: * -> * -- | Used by @YieldsArrowTSSD fn@ to structure the range of @fn@. type family RngF (fn :: * -> *) :: * -> * -- | Just a specialization: @yieldsArrowTSSD (YieldsArrowTSSD domD) fn = applyD domD fn@. yieldsArrowTSSD :: YieldsArrowTSSD fn t -> (forall t. fn t) -> DomF fn t -> RngF fn t yieldsArrowTSSD (YieldsArrowTSSD domD) fn = applyD domD 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 (YieldsArrowTSSD fn) ) => (forall t. fn t) -> NT u (ArrowTSS (DomF fn) (RngF fn)) eachArrow fn = firstNT toUni $ each [qP|YieldsArrowTSSD fn :: *->*|] $ \d -> yieldsArrowTSSD 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