{-# LANGUAGE MultiParamTypeClasses, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts #-}
-----------------------------------------------------------------------------
-- |
--- Module : GHC.HetMet.GArrow
+-- Module : Control.GArrow
-- Copyright : none
-- License : public domain
--
-- Stability : experimental
-- Portability : portable
-module GHC.HetMet.GArrow (
+module Control.GArrow (
GArrow(..),
GArrowDrop(..),
GArrowCopy(..),
+++ /dev/null
-{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators -XFlexibleInstances -XFunctionalDependencies -XEmptyDataDecls #-}
------------------------------------------------------------------------------
--- |
--- Module : GHC.HetMet.Arrow
--- Copyright : none
--- License : public domain
---
--- Maintainer : Adam Megacz <megacz@acm.org>
--- Stability : experimental
--- Portability : portable
-
-module GHC.HetMet.Arrow where
-import GHC.HetMet.GArrow
-import Control.Arrow
-import Control.Category
-
-------------------------------------------------------------------------------
--- GArrow instances for Control.Arrow; this is kept in a separate
--- module because having it available to GHC's instance-search
--- algorithm often creates overlapping or even undecidable
--- instance-search problems
-
-type Id a = a
-
-instance Arrow a => GArrow a (,) () where
- ga_first = first
- ga_second = second
- ga_cancell = arr (\((),x) -> x)
- ga_cancelr = arr (\(x,()) -> x)
- ga_uncancell = arr (\x -> ((),x))
- ga_uncancelr = arr (\x -> (x,()))
- ga_assoc = arr (\((x,y),z) -> (x,(y,z)))
- ga_unassoc = arr (\(x,(y,z)) -> ((x,y),z))
-
-instance Arrow a => GArrowDrop a (,) () where
- ga_drop = arr (\x -> ())
-
-instance Arrow a => GArrowCopy a (,) () where
- ga_copy = arr (\x -> (x,x))
-
-instance Arrow a => GArrowSwap a (,) () where
- ga_swap = arr (\(x,y) -> (y,x))
-
-instance Arrow a => GArrowConstant a (,) () t t where
- ga_constant x = arr (\() -> x)
-
-instance Arrow a => GArrowReify a (,) () x y x y where
- ga_reify = arr
-
-instance ArrowLoop a => GArrowLoop a (,) () where
- ga_loopr = loop
- ga_loopl f = loop (ga_swap >>> f >>> ga_swap)
-
-instance ArrowApply a => GArrowApply a (,) () a where
- ga_applyl = ga_swap >>> app
- ga_applyr = app
-
-instance Arrow a => GArrowProd a (,) () where
-
--- The uninhabited type
-data Void
-
--- In Coq we could simply prove that these cases are impossible; in Haskell we need to have some faith.
-voidImpossible :: Void -> a
-voidImpossible = error "this is impossible; you have a bug in your compiler"
-
-instance ArrowChoice a => GArrow a Either Void where
- ga_first = left
- ga_second = right
- ga_uncancell = arr Right
- ga_uncancelr = arr Left
- ga_cancell = arr unVoidLeft
- where
- unVoidLeft (Left v) = voidImpossible v
- unVoidRight (Right x) = x
- ga_cancelr = arr unVoidRight
- where
- unVoidRight (Left x) = x
- unVoidRight (Right v) = voidImpossible v
- ga_assoc = arr eitherAssoc
- where
- eitherAssoc (Left (Left x)) = Left x
- eitherAssoc (Left (Right y)) = Right (Left y)
- eitherAssoc (Right z ) = Right (Right z)
- ga_unassoc = arr eitherUnAssoc
- where
- eitherUnAssoc (Left x ) = Left (Left x)
- eitherUnAssoc (Right (Left y)) = Left (Right y)
- eitherUnAssoc (Right (Right z)) = Right z
-
-instance ArrowChoice a => GArrowSum a Either Void where
- ga_never = arr voidImpossible
- ga_merge = arr merge
- where
- merge (Left x) = x
- merge (Right x) = x
-
-
-
+++ /dev/null
-{-# OPTIONS -fwarn-incomplete-patterns #-}
-{-# LANGUAGE RankNTypes, FlexibleInstances, TypeFamilies, MultiParamTypeClasses, GADTs, DatatypeContexts, TypeOperators #-}
------------------------------------------------------------------------------
---
--- | The instance witnessing the fact that (forall g . GArrow g => g a b) is fully enriched in Hask.
---
--- Module : GHC.HetMet.GArrowFullyEnriched
--- Copyright : none
--- License : public domain
---
--- Maintainer : Adam Megacz <megacz@acm.org>
--- Stability : experimental
--- Portability : portable
---
--- TO DO: not entirely sure that when ga_first/ga_second are applied
--- to a (B f f') that it's always necessarily the right idea to toss
--- out the half which would force us to do a swap. What if the thing
--- being firsted contains only unit wires? That might not be
--- possible, since B's necessarily use their argument.
---
-
-module GHC.HetMet.GArrowFullyEnriched (
--- | It's easy to write a function with this type:
---
--- > homfunctor :: (GArrow g (,) () => g a b -> (g () a -> g () b))
---
--- ... it's nothing more than the precomposition function:
---
--- > homfunctor = (.)
---
--- however, writing its *inverse* is not so easy:
---
--- > homfunctor_inv :: (GArrow g (,) () => (g () a -> g () b) -> g a b)
---
--- Think about it. This is saying that every way of turning a @(g ()
--- a)@ into a @(g () b)@ is equivalent to precomposition, for some
--- magically-divined value of type @(g a b)@. That's hard to believe!
--- In fact, it's flat out false unless we exploit parametricity. This
--- module does that, and wraps up all of the magic in an easy-to-use
--- implementation of homfunctor_inv.
---
--- This module actually provides something slightly more general:
---
--- > homfunctor_inv :: (GArrow g (**) u => (g u a -> g x b) -> g (a**x) b)
---
--- ... where the actual "hom functor" case has x=u
---
--- Note that @homfunctor_inv@ needs instances of @GArrowDrop@,
--- @GArrowCopy@, and @GArrowSwap@ in order to work this magic.
--- However, ga_drop/ga_copy/ga_swap will only be used if necessary.
---
-
- homfunctor_inv
-
--- * Category Theoretic Background
--- $extradoc1
-
-) where
-import Control.Category
-import GHC.HetMet.GArrow
---import GHC.HetMet.GArrowEnclosure
-import Prelude hiding ((.), id)
-
-data GArrow g (**) u => Polynomial g (**) u t x y
- = L (g (t**x) y) -- uses t, wants it as the left arg
- | R (g (x**t) y) -- uses t, wants it as the right arg
- | B (g (t**x) y) (g (x**t) y) -- uses t, doesn't care which arg
- | N (g x y) -- doesn't use t
-
-instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => Category (Polynomial g (**) u t) where
- id = N id
- (N g) . (N f) = N $ g . f
- (N g) . (L f) = L $ g . f
- (N g) . (R f) = R $ g . f
- (N g) . (B f f') = B (f >>> g) (f' >>> g)
- (L g) . (N f) = L $ g . ga_second f
- (R g) . (N f) = R $ g . ga_first f
- (B g g') . (N f) = B (ga_second f >>> g) (ga_first f >>> g')
- (L g) . (L f) = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g
- (L g) . (B f f') = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g
- (R g) . (R f) = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f >>> g
- (B g g') . (R f) = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f >>> g'
- (B g g') . (L f) = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g
- (R g) . (B f f') = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f' >>> g
- (R g) . (L f) = L $ ga_first ga_copy >>> ga_assoc >>> ga_second f >>> ga_swap >>> g
- (L g) . (R f) = R $ ga_second ga_copy >>> ga_unassoc >>> ga_first f >>> ga_swap >>> g
- (B g g') . (B f f') = B (ga_first ga_copy >>> ga_assoc >>> ga_second f >>> g)
- (ga_second ga_copy >>> ga_unassoc >>> ga_first f' >>> g')
-
-instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrow (Polynomial g (**) u t) (**) u where
- ga_first (N f) = N $ ga_first f
- ga_first (L f) = L $ ga_unassoc >>> ga_first f
- ga_first (R f) = B (ga_unassoc >>> ga_first (ga_swap >>> f))
- (ga_assoc >>> ga_second ga_swap >>> ga_unassoc >>> ga_first f)
- ga_first (B f _) = L $ ga_unassoc >>> ga_first f
- ga_second (N g) = N $ ga_second g
- ga_second (L f) = B (ga_unassoc >>> ga_first ga_swap >>> ga_assoc >>> ga_second f)
- (ga_assoc >>> ga_second (ga_swap >>> f))
- ga_second (R g) = R $ ga_assoc >>> ga_second g
- ga_second (B _ g) = R $ ga_assoc >>> ga_second g
- ga_cancell = N ga_cancell
- ga_cancelr = N ga_cancelr
- ga_uncancell = N ga_uncancell
- ga_uncancelr = N ga_uncancelr
- ga_assoc = N ga_assoc
- ga_unassoc = N ga_unassoc
-
-instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowCopy (Polynomial g (**) u t) (**) u
- where
- ga_copy = N ga_copy
-
-instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowDrop (Polynomial g (**) u t) (**) u
- where
- ga_drop = N ga_drop
-
-instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => GArrowSwap (Polynomial g (**) u t) (**) u
- where
- ga_swap = N ga_swap
-
---instance (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u, GArrowLoop g (**) u)
--- => GArrowLoop (Polynomial g (**) u t) (**) u
--- where
--- ga_loopl = error "FIXME: GArrowFullyEnriched loopl not implemented"
--- ga_loopr = error "FIXME: GArrowFullyEnriched loopl not implemented"
-
---instance GArrowEnclosure q g (**) u => GArrowEnclosure (Polynomial q (**) u t) g (**) u where
--- enclose f = N (enclose f)
-
---
--- | Given an **instance-polymorphic** Haskell function @(g () a)->(g b c)@ we can produce
--- a self-contained instance-polymorphic term @(g (a**b) c)@. The "trick" is that we supply
--- the instance-polymorphic Haskell function with a modified dictionary (type class instance)
---
-homfunctor_inv :: forall a b c.
- (forall g (**) u . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g u a -> g b c) ->
- (forall g (**) u . (GArrowSwap g (**) u, GArrowCopy g (**) u, GArrowDrop g (**) u) => g (a**b) c)
-homfunctor_inv f =
- case f (B ga_cancelr ga_cancell) of
- (N f') -> ga_first ga_drop >>> ga_cancell >>> f'
- (L f') -> f'
- (R f') -> ga_swap >>> f'
- (B f' _) -> f'
-
---
--- $extradoc1
---
--- A few more comments are in order. First of all, the function
--- @homfunctor@ above really is a hom-functor; its domain is the
--- category whose objects are Haskell types and whose morphisms a->b
--- are Haskell terms of type @(GArrow g => g a b)@ -- note how the
--- term is polymorphic in @g@.
---
--- This category is Hask-enriched: for each choice of @a@ and @b@, the
--- collection of all morphisms a->b happens to be a Hask-object, and
--- all the other necessary conditions are met.
---
--- I use the term "fully enriched" to mean "enriched such that the
--- hom-functor at the terminal object is a full functor". For any
--- morphism f whose domain and codomain are in the range of the
--- hom-functor, the function homfunctor_inv above will pick out a
--- morphism in its domain which is sent to f -- it is the witness
--- to the fact that the functor is full.
---
GuestCharLiteral, guestCharLiteral
) where
import Prelude (Integer, String, Char, Bool, error)
-import GHC.HetMet.GArrow
+import Control.GArrow
import GHC.HetMet.CodeTypes
-- Note that stringwise-identical identifiers at different syntactic
+++ /dev/null
-{-# LANGUAGE RankNTypes, MultiParamTypeClasses, TypeOperators, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}
------------------------------------------------------------------------------
--- |
--- Module : GHC.HetMet.IGArrow
--- Copyright : none
--- License : public domain
---
--- Maintainer : Adam Megacz <megacz@acm.org>
--- Stability : experimental
--- Portability : portable
-
-module GHC.HetMet.IGArrow (
- IGArrow(..),
- IGArrowDrop(..),
- IGArrowCopy(..),
- IGArrowSwap(..),
- IGArrowLoop(..),
-
- IGArrowEval(..),
- IGArrowConstant(..),
- IGArrowLiteral(..),
-
- IGArrowReify(..),
- IGArrowReflect(..),
-
- -- IGArrowSum(..), ga_inl, ga_inr,
- -- IGArrowProd(..),
-
-) where
-import Control.Category
-import GHC.HetMet.GArrow
-import GHC.HetMet.GArrowFullyEnriched
-import Prelude hiding (id, (.))
-
---
--- Importing GHC.HetMet.Arrow leads to overlapping instances; that's
--- why you see (GArrow (->) (,) () => ...) below in many places
--- instead of simply providing the instance defined in
--- GHC.HetMet.Arrow.
---
---import GHC.HetMet.Arrow
-
-
-
-
-------------------------------------------------------------------------
--- Internal GArrows
---
--- | An "internal generalized arrow" is a GArrow except that it uses
--- some *other* GArrow in place of Haskell's function space.
---
-class GArrow g (**) u => IGArrow g (**) u gg (***) uu | g -> (**), (**) -> u, gg -> (***), (***) -> uu where
- iga_id :: g u (gg x x)
- iga_comp :: g ((gg x y) ** (gg y z)) (gg x z)
- iga_first :: g (gg x y) (gg (x *** z) (y *** z))
- iga_second :: g (gg x y) (gg (z *** x) (z *** y))
- iga_cancell :: g u (gg (uu***x) x)
- iga_cancelr :: g u (gg (x***uu) x)
- iga_uncancell :: g u (gg x (uu***x))
- iga_uncancelr :: g u (gg x (x***uu))
- iga_assoc :: g u (gg ((x*** y)***z ) ( x***(y ***z)))
- iga_unassoc :: g u (gg ( x***(y ***z)) ((x*** y)***z ))
-
-class IGArrow g (**) u gg (***) uu => IGArrowCopy g (**) u gg (***) uu where
- iga_copy :: g u (gg x (x***x))
-
-class IGArrow g (**) u gg (***) uu => IGArrowDrop g (**) u gg (***) uu where
- iga_drop :: g u (gg x uu)
-
-class IGArrow g (**) u gg (***) uu => IGArrowSwap g (**) u gg (***) uu where
- iga_swap :: g u (gg (x***y) (y***x))
-
-class IGArrow g (**) u gg (***) uu => IGArrowLoop g (**) u gg (***) uu where
- iga_loopr :: g (gg (x***z) (y***z)) (gg x y)
- iga_loopl :: g (gg (z***x) (z***y)) (gg x y)
-
-class IGArrow g (**) u gg (***) uu => IGArrowLiteral g (**) u gg (***) uu t r where
- iga_literal :: g t (gg uu r)
-
-class IGArrow g (**) u gg (***) uu => IGArrowEval g (**) u gg (***) uu r t where
- iga_eval :: g (gg uu r) t
-
-class IGArrow g (**) u gg (***) uu => IGArrowConstant g (**) u gg (***) uu t r where
- iga_constant :: g t (gg uu r)
-
-class IGArrow g (**) u gg (***) uu => IGArrowReify g (**) u gg (***) uu x y r q where
- iga_reify :: g (g x y) (gg r q)
-
-class IGArrow g (**) u gg (***) uu => IGArrowReflect g (**) u gg (***) uu r q x y where
- iga_reflect :: g (gg r q) (g x y)
-
-
-
-------------------------------------------------------------------------
--- Externalization
---
--- | An IGArrow may be "externalized" to form a normal generalized
--- arrow. If the IGArrow was an instance of class IGArrowXX, the
--- externalization will be an instance of GArrowYY.
---
--- TODO: I should be one level deeper here: assuming an (IGArrow
--- (IGArrow g)), create an (IGArrow g).
---
-
-newtype Ex g x y = Ex (g x y)
-
---
--- | Every IGArrow of (->) is a GArrow
---
-instance IGArrow (->) (,) () g (**) u => Category (Ex g) where
- id = Ex (iga_id ())
- (Ex g) . (Ex f) = Ex (iga_comp (f,g))
-
-instance IGArrow (->) (,) () g (**) u => GArrow (Ex g) (**) u where
- ga_first (Ex f) = Ex $ iga_first f
- ga_second (Ex f) = Ex $ iga_second f
- ga_cancell = Ex $ iga_cancell ()
- ga_cancelr = Ex $ iga_cancelr ()
- ga_uncancell = Ex $ iga_uncancell ()
- ga_uncancelr = Ex $ iga_uncancelr ()
- ga_assoc = Ex $ iga_assoc ()
- ga_unassoc = Ex $ iga_unassoc ()
-
-instance IGArrowCopy (->) (,) () g (**) u => GArrowCopy (Ex g) (**) u where
- ga_copy = Ex $ iga_copy ()
-instance IGArrowDrop (->) (,) () g (**) u => GArrowDrop (Ex g) (**) u where
- ga_drop = Ex $ iga_drop ()
-instance IGArrowSwap (->) (,) () g (**) u => GArrowSwap (Ex g) (**) u where
- ga_swap = Ex $ iga_swap ()
-
-
-
-
-
-------------------------------------------------------------------------
--- Internalization
---
--- | Every GArrow is internal to the GArrow instance on (->)
---
-
-newtype In g x y = In (g x y)
-
-instance (GArrow (->) (,) (), GArrow g (**) u) => IGArrow (->) (,) () (In g) (**) u where
- iga_id _ = In $ id
- iga_comp (In f,In g) = In $ f >>> g
- iga_first (In f) = In $ ga_first f
- iga_second (In f) = In $ ga_second f
- iga_cancell _ = In $ ga_cancell
- iga_cancelr _ = In $ ga_cancelr
- iga_uncancell _ = In $ ga_uncancell
- iga_uncancelr _ = In $ ga_uncancelr
- iga_assoc _ = In $ ga_assoc
- iga_unassoc _ = In $ ga_unassoc
-instance (GArrow (->) (,) (), GArrowCopy g (**) u) => IGArrowCopy (->) (,) () (In g) (**) u where
- iga_copy _ = In $ ga_copy
-instance (GArrow (->) (,) (), GArrowDrop g (**) u) => IGArrowDrop (->) (,) () (In g) (**) u where
- iga_drop _ = In $ ga_drop
-instance (GArrow (->) (,) (), GArrowSwap g (**) u) => IGArrowSwap (->) (,) () (In g) (**) u where
- iga_swap _ = In $ ga_swap
-
-
-
-
-
-------------------------------------------------------------------------
--- Kappa
---
--- | This is named "kappa" for its similarity to an operator in
--- Hasegawa's kappa-calculus, but the formal connection is a bit of
--- a stretch; the method iga_kappa below is used by the flattener to
--- implement the typing rule for abstraction in Kappa-calculus.
---
--- x , 1->a |- b ->c
--- -------------------------- [Kappa]
--- x |- (a,b)->c
---
---
-class GArrow g (**) u => IKappa g (**) u where
- iga_kappa :: forall a b c .
- (forall gg (***) uu . (IGArrowCopy g (**) u gg (***) uu,
- IGArrowDrop g (**) u gg (***) uu,
- IGArrowSwap g (**) u gg (***) uu) =>
- g (gg uu a) (gg b c)) ->
- (forall gg (***) uu . (IGArrowCopy g (**) u gg (***) uu,
- IGArrowDrop g (**) u gg (***) uu,
- IGArrowSwap g (**) u gg (***) uu) =>
- g u (gg (a***b) c))
- -- TO DO: change the above to iga_kappal, add iga_kappar
-
---
--- | The (->) GArrow has the Kappa property.
---
-instance GArrow (->) (,) () => IKappa (->) (,) () where
- iga_kappa f = case (homfunctor_inv (\x -> case f (In x) of In x' -> x')) of Ex x -> \() -> x
-
-
-
-
-
-
-------------------------------------------------------------------------------
--- Self-Internal GArrows
-
---
--- | A self-internal GArrow is, well, internal to itself
---
-class IGArrow g (**) u g (**) u => SelfInternalGArrow g (**) u
-
---
--- | Self-internal GArrows have curry/apply
---
-instance SelfInternalGArrow g (**) u => GArrowApply g (**) u g where
- ga_applyl = error "FIXME: SelfInternalGArrow => GArrowApply not implemented yet"
- ga_applyr = error "FIXME: SelfInternalGArrow => GArrowApply not implemented yet"
-
---
--- | Self-internal GArrows have curry/apply
---
-instance SelfInternalGArrow g (**) u => GArrowCurry g (**) u g where
- ga_curryl = error "FIXME: SelfInternalGArrow => GArrowCurry not implemented yet"
- ga_curryr = error "FIXME: SelfInternalGArrow => GArrowCurry not implemented yet"
-
---
--- | Haskell's function space is self-internal
---
-instance GArrow (->) (,) () => IGArrow (->) (,) () (->) (,) () where
- iga_id _ = id
- iga_comp (f,g) = f >>> g
- iga_first = ga_first
- iga_second = ga_second
- iga_cancell _ = ga_cancell
- iga_cancelr _ = ga_cancelr
- iga_uncancell _ = ga_uncancell
- iga_uncancelr _ = ga_uncancelr
- iga_assoc _ = ga_assoc
- iga_unassoc _ = ga_unassoc
-
---instance GArrow (->) (,) () => SelfInternalGArrow (->) (,) ()
{-# LANGUAGE RankNTypes, ScopedTypeVariables, NoMonomorphismRestriction, TypeOperators, FunctionalDependencies, FlexibleContexts #-}
-----------------------------------------------------------------------------
-- |
--- Module : GHC.HetMet.GArrow
+-- Module : GHC.HetMet.Private
-- Copyright : none
-- License : public domain
--
) where
import Control.Category ( (>>>) )
import qualified Control.Category
-import GHC.HetMet.GArrow
+import Control.GArrow
-------------------------------------------------------------------------
-- Used internally by the compiler, subject to change without notice!!
GHC.ForeignPtr,
GHC.HetMet,
GHC.HetMet.CodeTypes,
- GHC.HetMet.GArrow,
- GHC.HetMet.GArrowFullyEnriched,
GHC.HetMet.GuestLanguage,
- GHC.HetMet.IGArrow,
GHC.HetMet.Private,
- GHC.HetMet.Arrow,
GHC.MVar,
GHC.IO,
GHC.IO.IOMode,
Control.Concurrent.SampleVar,
Control.Exception,
Control.Exception.Base
+ Control.GArrow,
Control.OldException,
Control.Monad,
Control.Monad.Fix,
projects / ghc-base.git / commitdiff