From 5473657eb7aadc0b8da9370c4e0bed87b2f66513 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 19 Jun 2011 22:57:26 -0700 Subject: [PATCH] move things out of GHC.HetMet.CodeTypes into GHC.HetMet.GuestLanguage --- GHC/HetMet/CodeTypes.hs | 127 ++++--------------------------------------- GHC/HetMet/GuestLanguage.hs | 87 +++++++++++++++++++++++++++++ 2 files changed, 98 insertions(+), 116 deletions(-) create mode 100644 GHC/HetMet/GuestLanguage.hs diff --git a/GHC/HetMet/CodeTypes.hs b/GHC/HetMet/CodeTypes.hs index 8269686..18d8579 100644 --- a/GHC/HetMet/CodeTypes.hs +++ b/GHC/HetMet/CodeTypes.hs @@ -1,24 +1,21 @@ -{-# OPTIONS -XModalTypes -XMultiParamTypeClasses -XKindSignatures -XFlexibleContexts #-} +{-# LANGUAGE ModalTypes, MultiParamTypeClasses, KindSignatures, FlexibleContexts #-} +----------------------------------------------------------------------------- +-- | +-- Module : GHC.HetMet.CodeTypes +-- Copyright : none +-- License : public domain +-- +-- Maintainer : Adam Megacz +-- Stability : experimental +-- Portability : portable module GHC.HetMet.CodeTypes ( hetmet_brak, hetmet_esc, hetmet_csp, - hetmet_flatten, - pga_flatten, - pga_unflatten, - pga_flattened_id, GuestIntegerLiteral, guestIntegerLiteral, GuestStringLiteral, guestStringLiteral, - GuestCharLiteral, guestCharLiteral, - GuestLanguageMult, <[ (*) ]>, - GuestLanguageAdd, <[ (+) ]>, - GuestLanguageSub, <[ (-) ]>, <[ negate ]>, - GuestLanguageFromInteger, <[ fromInteger ]>, - GuestLanguageBool, <[ (||) ]>, <[ (&&) ]>, <[ true ]>, <[ false ]>, <[ ifThenElse ]> + GuestCharLiteral, guestCharLiteral ) where -import Prelude (Integer, String, Char, Bool, error) -import GHC.HetMet.GArrow -import GHC.HetMet.Private 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?" @@ -29,40 +26,6 @@ hetmet_esc = Prelude.error "hetmet_esc should never be evaluated; did you forget 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?" -hetmet_flatten :: - forall g . - GArrowSTKCL g => - forall x y. - <[ x -> y ]>@g - -> - (g x y) -hetmet_flatten x = unG (pga_flatten 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 (pga_flattened_id). --- Its only purpose is to act as a "safe type cast" during pre-flattening --- type-inference/checking: -pga_flatten :: - forall g x y. - <[ x -> y ]>@g -> - PGArrow g x y -pga_flatten = error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?" -pga_unflatten :: - forall g x y. - PGArrow g x y -> - <[ x -> y ]>@g -pga_unflatten = error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?" - -pga_flattened_id :: - forall g x y. - PGArrow g x y -> - PGArrow g x y -pga_flattened_id x = x - - --- FIXME: move these and the three above to "prim" or something like that. - -- Technically these functions ought to be invoked *during -- compilation*; in the future I would like to use Template Haskell to -- do that. @@ -72,71 +35,3 @@ class GuestStringLiteral c where guestStringLiteral :: String -> <[ String ]>@c class GuestCharLiteral c where guestCharLiteral :: Char -> <[ Char ]>@c - - -class GuestLanguageConstant c t where - guestLanguageConstant :: t -> <[ t ]>@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/GuestLanguage.hs b/GHC/HetMet/GuestLanguage.hs new file mode 100644 index 0000000..43a391e --- /dev/null +++ b/GHC/HetMet/GuestLanguage.hs @@ -0,0 +1,87 @@ +{-# LANGUAGE ModalTypes, MultiParamTypeClasses, KindSignatures, FlexibleContexts #-} +----------------------------------------------------------------------------- +-- | +-- Module : GHC.HetMet.GuestLanguage +-- Copyright : none +-- License : public domain +-- +-- Maintainer : Adam Megacz +-- Stability : experimental +-- Portability : portable + +module GHC.HetMet.GuestLanguage ( + GuestLanguageMult, <[ (*) ]>, + GuestLanguageAdd, <[ (+) ]>, + GuestLanguageSub, <[ (-) ]>, <[ negate ]>, + GuestLanguageFromInteger, <[ fromInteger ]>, + GuestLanguageBool, <[ (||) ]>, <[ (&&) ]>, <[ true ]>, <[ false ]>, <[ ifThenElse ]>, + GuestIntegerLiteral, guestIntegerLiteral, + GuestStringLiteral, guestStringLiteral, + GuestCharLiteral, guestCharLiteral +) where +import Prelude (Integer, String, Char, Bool, error) +import GHC.HetMet.GArrow +import GHC.HetMet.CodeTypes + +-- 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. -- 1.7.10.4