From 3ad8f1f62daf9614a2edbf97ac6e64191c31d2de Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 19 Mar 2011 12:32:04 -0700 Subject: [PATCH] migrate HetMet base changes to git repo --- GHC/HetMet.hs | 4 ++ GHC/HetMet/CodeTypes.hs | 122 +++++++++++++++++++++++++++++++++++++++++++++++ GHC/HetMet/GArrow.hs | 48 +++++++++++++++++++ base.cabal | 3 ++ 4 files changed, 177 insertions(+) create mode 100644 GHC/HetMet.hs create mode 100644 GHC/HetMet/CodeTypes.hs create mode 100644 GHC/HetMet/GArrow.hs diff --git a/GHC/HetMet.hs b/GHC/HetMet.hs new file mode 100644 index 0000000..d76e062 --- /dev/null +++ b/GHC/HetMet.hs @@ -0,0 +1,4 @@ +module GHC.HetMet +where + +-- just to prevent GHC from complaining about modules named GHC.HetMet.XYZ diff --git a/GHC/HetMet/CodeTypes.hs b/GHC/HetMet/CodeTypes.hs new file mode 100644 index 0000000..9584607 --- /dev/null +++ b/GHC/HetMet/CodeTypes.hs @@ -0,0 +1,122 @@ +{-# OPTIONS -XModalTypes -XMultiParamTypeClasses #-} +module GHC.HetMet.CodeTypes ( + hetmet_brak, + hetmet_esc, + hetmet_csp, + GuestIntegerLiteral, guestIntegerLiteral, + GuestStringLiteral, guestStringLiteral, + GuestCharLiteral, guestCharLiteral, + GuestLanguageMult, <[ (*) ]>, + GuestLanguageAdd, <[ (+) ]>, + GuestLanguageSub, <[ (-) ]>, <[ negate ]>, + GuestLanguageFromInteger, <[ fromInteger ]>, + GuestLanguageBool, <[ (||) ]>, <[ (&&) ]>, <[ true ]>, <[ false ]>, <[ ifThenElse ]>, + <[ fromp ]> +) where +import Prelude (Integer, String, Char, Bool, error) +import GHC.HetMet.GArrow + +hetmet_brak :: forall c. forall a. a -> <[a]>@c +hetmet_brak = Prelude.error "hetmet_brak should never be evaluated; did you forget to compile with -fcoqpass?" + +hetmet_esc :: forall c. forall a. <[a]>@c -> a +hetmet_esc = Prelude.error "hetmet_esc should never be evaluated; did you forget to compile with -fcoqpass?" + +hetmet_csp :: forall c. forall a. a -> a +hetmet_csp = Prelude.error "hetmet_csp should never be evaluated; did you forget to compile with -fcoqpass?" + +<[ fromp ]> :: forall a b . <[ a -> a ]>@b +<[ fromp ]> = <[ \x -> x ]> + +{- +-- After the flattening pass the argument and result types of this +-- function are identical (for any instantiation), so the flattener +-- simply turns it into the identity function. Its only purpose is to +-- act as a "safe type cast" during pre-flattening +-- type-inference/checking: +hetmet_flatten :: + forall g. + GArrow g (**) => + GArrowDrop g (**) => + GArrowCopy g (**) => + GArrowSwap g (**) => + GArrowLoop g (**) => + forall x y. + <[ x -> y ]>@g + -> + (g x y) +hetmet_flatten _ = Prelude.error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?" +-} + +class GuestIntegerLiteral c where + guestIntegerLiteral :: Integer -> <[ Integer ]>@c + +class GuestStringLiteral c where + guestStringLiteral :: String -> <[ String ]>@c + +class GuestCharLiteral c where + guestCharLiteral :: Char -> <[ Char ]>@c + +-- Note that stringwise-identical identifiers at different syntactic +-- depths are different identifiers; for this reason the operators +-- below can have a different type at syntactical depth 1 than at +-- syntactical depth 0. + +class GuestLanguageMult c t where + <[ (*) ]> :: <[ t -> t -> t ]>@c + +class GuestLanguageAdd c t where + <[ (+) ]> :: <[ t -> t -> t ]>@c + +class GuestLanguageSub c t where + <[ (-) ]> :: <[ t -> t -> t ]>@c + <[ negate ]> :: <[ t -> t ]>@c -- used for unary (-) + +class GuestLanguageFromInteger c t where + <[ fromInteger ]> :: <[ Integer -> t ]>@c + +class GuestLanguageBool c where + <[ (||) ]> :: <[ Bool -> Bool -> Bool ]>@c + <[ (&&) ]> :: <[ Bool -> Bool -> Bool ]>@c + <[ true ]> :: <[ Bool ]>@c + <[ false ]> :: <[ Bool ]>@c + <[ ifThenElse ]> :: <[ Bool -> t -> t -> t ]>@c + +-- For heterogeneous metaprogramming, the meaning of "running" a +-- program is fairly ambiguous, and moreover is highly sensitive to +-- which subclasses of GuestLanguage the expression assumes it is +-- dealing with. For example, in homogeneous metaprogramming, "run" +-- has this type: +-- +-- ga_run :: forall a. (forall c. <[a]>@c) -> a +-- +-- However, an expression which uses, say (*) at level 1 will never +-- be able to be passed to this expression, since +-- +-- square :: forall c t. GuestLanguageMult ct => <[t]>@c -> <[t]>@c +-- square x = <[ ~~x * ~~x ]> +-- + +-- So even though this expression is polymorphic in the environment +-- classifier "c", it isn't "polymorphic enough". This isn't merely a +-- technical obstacle -- the more features you assume the guest +-- language has, the more work the "run" implementation is obligated +-- to perform, and the type system must track that obligation. +-- +-- The upshot is that we can define special-purpose "run" classes such as: +-- +-- class GuestLanguageRunMult t where +-- ga_runMult :: forall a. (forall c. GuestLanguageMult c t => <[a]>@c) -> a +-- +-- Any implementation of this class will need to know how to interpret +-- the (*) operator. Unfortunately, to my knowledge, there is no way +-- to quantify over type classes in the Haskell type system, which is +-- what we would need to define a type-class-indexed version of the +-- GuestLanguageRun class; if we could do that, then we would have: +-- +-- class GuestLanguageRun ( t ::: * -> TYPECLASS ) where +-- ga_runMult :: forall a. (forall c. TYPECLASS c => <[a]>@c) -> a +-- +-- It might be possible to pull this of using type families; I need to +-- look into that. + diff --git a/GHC/HetMet/GArrow.hs b/GHC/HetMet/GArrow.hs new file mode 100644 index 0000000..d31436c --- /dev/null +++ b/GHC/HetMet/GArrow.hs @@ -0,0 +1,48 @@ +{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators #-} +module GHC.HetMet.GArrow ( + GArrow(..), + GArrowDrop(..), + GArrowCopy(..), + GArrowSwap(..), + GArrowLoop(..), + GArrowReify(..), + GArrowReflect(..) +) where + +class GArrow g (**) where + ga_id :: g x x + ga_comp :: g x y -> g y z -> g x z + ga_first :: g x y -> g (x ** z) (y ** z) + ga_second :: g x y -> g (z ** x) (z ** y) + ga_cancell :: g (()**x) x + ga_cancelr :: g (x**()) x + ga_uncancell :: g x (()**x) + ga_uncancelr :: g x (x**()) + ga_assoc :: g ((x**y)**z) (x**(y**z)) + ga_unassoc :: g (x**(y**z)) ((x**y)**z) + +class GArrow g (**) => GArrowDrop g (**) where + ga_drop :: g x () + +class GArrow g (**) => GArrowCopy g (**) where + ga_copy :: g x (x**x) + +class GArrow g (**) => GArrowSwap g (**) where + ga_swap :: g (x**y) (y**x) + --ga_second f = ga_comp (ga_comp ga_swap (ga_first f)) ga_swap + +class GArrow g (**) => GArrowLoop g (**) where + ga_loop :: g (x**z) (y**z) -> g x y + +class GArrow g (**) => GArrowLiteral g (**) a where + ga_literal :: a -> g () a + +-- not sure +class GArrow g (**) => GArrowReify g (**) where + ga_reify :: (x -> y) -> g x y + +-- not sure +class GArrow g (**) => GArrowReflect g (**) where + ga_reflect :: g x y -> (x -> y) + + diff --git a/base.cabal b/base.cabal index 6bb96f6..d799867 100644 --- a/base.cabal +++ b/base.cabal @@ -56,6 +56,9 @@ Library { GHC.Foreign, GHC.Float.ConversionUtils, GHC.ForeignPtr, + GHC.HetMet, + GHC.HetMet.CodeTypes, + GHC.HetMet.GArrow, GHC.MVar, GHC.IO, GHC.IO.IOMode, -- 1.7.10.4