GHC/HetMet/CodeTypes.hs

   1 {-# OPTIONS -XModalTypes -XMultiParamTypeClasses #-}
   2 module GHC.HetMet.CodeTypes (
   3   hetmet_brak,
   4   hetmet_esc,
   5   hetmet_csp,
   6   GuestIntegerLiteral, guestIntegerLiteral,
   7   GuestStringLiteral, guestStringLiteral,
   8   GuestCharLiteral, guestCharLiteral,
   9   GuestLanguageMult, <[ (*) ]>,
  10   GuestLanguageAdd,  <[ (+) ]>,
  11   GuestLanguageSub,  <[ (-) ]>, <[ negate ]>,
  12   GuestLanguageFromInteger, <[ fromInteger ]>,
  13   GuestLanguageBool, <[ (||) ]>, <[ (&&) ]>, <[ true ]>, <[ false ]>, <[ ifThenElse ]>,
  14   <[ fromp ]>
  15 ) where
  16 import Prelude (Integer, String, Char, Bool, error)
  17 import GHC.HetMet.GArrow
  18
  19 hetmet_brak :: forall c. forall a. a -> <[a]>@c
  20 hetmet_brak = Prelude.error "hetmet_brak should never be evaluated; did you forget to compile with -fcoqpass?"
  21
  22 hetmet_esc  :: forall c. forall a. <[a]>@c -> a
  23 hetmet_esc = Prelude.error "hetmet_esc should never be evaluated; did you forget to compile with -fcoqpass?"
  24
  25 hetmet_csp :: forall c. forall a. a -> a
  26 hetmet_csp = Prelude.error "hetmet_csp should never be evaluated; did you forget to compile with -fcoqpass?"
  27
  28 <[ fromp ]> :: forall a b . <[ a -> a ]>@b
  29 <[ fromp ]> = <[ \x -> x ]>
  30
  31 {-
  32 -- After the flattening pass the argument and result types of this
  33 -- function are identical (for any instantiation), so the flattener
  34 -- simply turns it into the identity function.  Its only purpose is to
  35 -- act as a "safe type cast" during pre-flattening
  36 -- type-inference/checking:
  37 hetmet_flatten ::
  38    forall g.
  39     GArrow     g (**) =>
  40     GArrowDrop g (**) =>
  41     GArrowCopy g (**) =>
  42     GArrowSwap g (**) =>
  43     GArrowLoop g (**) =>
  44       forall x y.
  45          <[ x -> y ]>@g
  46          ->
  47          (g x y)
  48 hetmet_flatten _ = Prelude.error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?"
  49 -}
  50
  51 class GuestIntegerLiteral c where
  52   guestIntegerLiteral :: Integer -> <[ Integer ]>@c
  53
  54 class GuestStringLiteral c where
  55   guestStringLiteral :: String -> <[ String ]>@c
  56
  57 class GuestCharLiteral c where
  58   guestCharLiteral :: Char -> <[ Char ]>@c
  59
  60 -- Note that stringwise-identical identifiers at different syntactic
  61 -- depths are different identifiers; for this reason the operators
  62 -- below can have a different type at syntactical depth 1 than at
  63 -- syntactical depth 0.
  64
  65 class GuestLanguageMult c t where
  66   <[ (*)    ]> :: <[ t -> t -> t ]>@c
  67
  68 class GuestLanguageAdd c t where
  69   <[ (+)    ]> :: <[ t -> t -> t ]>@c
  70
  71 class GuestLanguageSub c t where
  72   <[ (-)    ]> :: <[ t -> t -> t ]>@c
  73   <[ negate ]> :: <[ t -> t      ]>@c   -- used for unary (-)
  74
  75 class GuestLanguageFromInteger c t where
  76   <[ fromInteger ]> :: <[ Integer -> t ]>@c
  77
  78 class GuestLanguageBool c where
  79   <[ (||) ]>       :: <[ Bool -> Bool -> Bool ]>@c
  80   <[ (&&) ]>       :: <[ Bool -> Bool -> Bool ]>@c
  81   <[ true ]>       :: <[ Bool ]>@c
  82   <[ false ]>      :: <[ Bool ]>@c
  83   <[ ifThenElse ]> :: <[ Bool -> t -> t -> t ]>@c
  84
  85 -- For heterogeneous metaprogramming, the meaning of "running" a
  86 -- program is fairly ambiguous, and moreover is highly sensitive to
  87 -- which subclasses of GuestLanguage the expression assumes it is
  88 -- dealing with.  For example, in homogeneous metaprogramming, "run"
  89 -- has this type:
  90 --
  91 --  ga_run :: forall a. (forall c. <[a]>@c) -> a
  92 --
  93 -- However, an expression which uses, say (*) at level 1 will never
  94 -- be able to be passed to this expression, since
  95 --
  96 --   square :: forall c t. GuestLanguageMult ct => <[t]>@c -> <[t]>@c
  97 --   square x = <[ ~~x * ~~x ]>
  98 --
  99
 100 -- So even though this expression is polymorphic in the environment
 101 -- classifier "c", it isn't "polymorphic enough".  This isn't merely a
 102 -- technical obstacle -- the more features you assume the guest
 103 -- language has, the more work the "run" implementation is obligated
 104 -- to perform, and the type system must track that obligation.
 105 --
 106 -- The upshot is that we can define special-purpose "run" classes such as:
 107 --
 108 --   class GuestLanguageRunMult t where
 109 --     ga_runMult :: forall a. (forall c. GuestLanguageMult c t => <[a]>@c) -> a
 110 --
 111 -- Any implementation of this class will need to know how to interpret
 112 -- the (*) operator.  Unfortunately, to my knowledge, there is no way
 113 -- to quantify over type classes in the Haskell type system, which is
 114 -- what we would need to define a type-class-indexed version of the
 115 -- GuestLanguageRun class; if we could do that, then we would have:
 116 --
 117 --   class GuestLanguageRun ( t ::: * -> TYPECLASS ) where
 118 --     ga_runMult :: forall a. (forall c. TYPECLASS c => <[a]>@c) -> a
 119 --
 120 -- It might be possible to pull this of using type families; I need to
 121 -- look into that.
 122