X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=GHC%2FHetMet%2FCodeTypes.hs;h=5e650408bbd3541626a40ee9d4fe9899cfc85f4f;hb=671fdd151ac7f8e4c67f1a2b55189cc48f2e5983;hp=d6291195753ccad07178b4d4e5295b82d46db2c7;hpb=11dca0057d71161c2b93af91f7921a648e6d9558;p=ghc-base.git diff --git a/GHC/HetMet/CodeTypes.hs b/GHC/HetMet/CodeTypes.hs index d629119..5e65040 100644 --- a/GHC/HetMet/CodeTypes.hs +++ b/GHC/HetMet/CodeTypes.hs @@ -1,142 +1,45 @@ -{-# 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, + hetmet_kappa, + hetmet_kappa_app, 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 :: 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 :: 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?" -hetmet_flatten :: - forall g . - GArrowSTKC g => - forall x y. - <[ x -> y ]>@g - -> - (g x y) -hetmet_flatten x = unG (pga_flatten x) +hetmet_kappa :: forall a b c . (( () -> a ) -> ( b -> c )) -> ( (a,b) -> c ) +hetmet_kappa = Prelude.error "hetmet_kappa should never be evaluated; did you forget to compile with -fcoqpass?" --- 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. +hetmet_kappa_app :: forall a b c . ( (a,b) -> c ) -> ( () -> a ) -> ( b -> c ) +hetmet_kappa_app = Prelude.error "hetmet_kappa_app should never be evaluated; did you forget to compile with -fcoqpass?" -- Technically these functions ought to be invoked *during -- compilation*; in the future I would like to use Template Haskell to -- do that. class GuestIntegerLiteral c where - guestIntegerLiteral :: Integer -> <[ Integer ]>@c + guestIntegerLiteral :: Integer -> <{ Integer }>@c class GuestStringLiteral c where - guestStringLiteral :: String -> <[ String ]>@c + 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. - + guestCharLiteral :: Char -> <{ Char }>@c