GHC/HetMet/CodeTypes.hs

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