From 4818fc6a8e0454c4a6f962e78df955678d277fd2 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 19 Jun 2011 19:01:12 -0700 Subject: [PATCH] add IGArrow: internal GArrows --- GHC/HetMet/IGArrow.hs | 180 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 180 insertions(+) create mode 100644 GHC/HetMet/IGArrow.hs diff --git a/GHC/HetMet/IGArrow.hs b/GHC/HetMet/IGArrow.hs new file mode 100644 index 0000000..cc6bd04 --- /dev/null +++ b/GHC/HetMet/IGArrow.hs @@ -0,0 +1,180 @@ +{-# LANGUAGE RankNTypes, MultiParamTypeClasses, NoMonomorphismRestriction, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts, FlexibleInstances, DatatypeContexts #-} +----------------------------------------------------------------------------- +-- | +-- Module : GHC.HetMet.IGArrow +-- Copyright : none +-- License : public domain +-- +-- Maintainer : Adam Megacz +-- 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 hiding ((.)) +import GHC.HetMet.GArrow +import Prelude hiding (id) +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 IGArrow 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 u) + +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) + + + + + +------------------------------------------------------------------------------ +-- 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 gg where +-- ga_applyl = :: g (x**(g x y) ) y +-- ga_applyr :: g ( (g x y)**x) y +-- +-- +-- | Self-internal GArrows have curry/apply +-- +-- instance SelfInternalGArrow g (**) u gg (***) uu => GArrowCurry g (**) u gg where +-- ga_curryl :: g (x**y) z -> g x (g y z) +-- ga_curryr :: g (x**y) z -> g y (g x z) + + + + + +------------------------------------------------------------------------------ +-- Instances + +-- +-- | Every GArrow is internal to the GArrow instance on (->) +-- +instance GArrow g (**) u => IGArrow (->) (,) () g (**) u 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 + + + + + + +------------------------------------------------------------------------ +-- 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 + IGArrow g (**) u q (***) uu => + Ext g (**) u q (***) uu x y + = Ext { unExt :: g u (q x y) } + +-- instance IGArrow g (**) u gg (***) uu => GArrowCopy g (**) u gg (***) uu where +-- iga_copy = undefined +-- +-- instance IGArrow g (**) u gg (***) uu => GArrowDrop g (**) u gg (***) uu where +-- iga_drop = undefined +-- +-- instance IGArrow g (**) u gg (***) uu => GArrowSwap g (**) u gg (***) uu where +-- iga_swap = undefined +-- +-- instance IGArrow g (**) u gg (***) uu => GArrowLoop g (**) u gg (***) uu where +-- iga_loopr = undefined +-- iga_loopl = undefined +-- +-- instance IGArrow g (**) u gg (***) uu => GArrowLiteral g (**) u gg (***) uu t r where +-- iga_literal = undefined +-- +-- instance IGArrow g (**) u gg (***) uu => GArrowEval g (**) u gg (***) uu r t where +-- iga_eval = undefined +-- +-- instance IGArrow g (**) u gg (***) uu => GArrowConstant g (**) u gg (***) uu t r where +-- iga_constant = undefined +-- +-- instance IGArrow g (**) u gg (***) uu => GArrowReify g (**) u gg (***) uu x y r q where +-- iga_reify = undefined +-- +-- instance IGArrow g (**) u gg (***) uu => GArrowReflect g (**) u gg (***) uu r q x y where +-- iga_reflect = undefined -- 1.7.10.4