GHC/HetMet/GuestLanguage.hs

   1 {-# LANGUAGE ModalTypes, MultiParamTypeClasses, KindSignatures, FlexibleContexts #-}
   2 -----------------------------------------------------------------------------
   3 -- |
   4 -- Module      :  GHC.HetMet.GuestLanguage
   5 -- Copyright   :  none
   6 -- License     :  public domain
   7 --
   8 -- Maintainer  :  Adam Megacz <megacz@acm.org>
   9 -- Stability   :  experimental
  10 -- Portability :  portable
  11
  12 module GHC.HetMet.GuestLanguage (
  13   GuestLanguageMult, <[ (*) ]>,
  14   GuestLanguageAdd,  <[ (+) ]>,
  15   GuestLanguageSub,  <[ (-) ]>, <[ negate ]>,
  16   GuestLanguageFromInteger, <[ fromInteger ]>,
  17   GuestLanguageBool, <[ (||) ]>, <[ (&&) ]>, <[ true ]>, <[ false ]>, <[ ifThenElse ]>,
  18   GuestIntegerLiteral, guestIntegerLiteral,
  19   GuestStringLiteral, guestStringLiteral,
  20   GuestCharLiteral, guestCharLiteral
  21 ) where
  22 import Prelude (Integer, String, Char, Bool, error)
  23 import GHC.HetMet.GArrow
  24 import GHC.HetMet.CodeTypes
  25
  26 -- Note that stringwise-identical identifiers at different syntactic
  27 -- depths are different identifiers; for this reason the operators
  28 -- below can have a different type at syntactical depth 1 than at
  29 -- syntactical depth 0.
  30
  31 class GuestLanguageMult c t where
  32   <[ (*)    ]> :: <[ t -> t -> t ]>@c
  33
  34 class GuestLanguageAdd c t where
  35   <[ (+)    ]> :: <[ t -> t -> t ]>@c
  36
  37 class GuestLanguageSub c t where
  38   <[ (-)    ]> :: <[ t -> t -> t ]>@c
  39   <[ negate ]> :: <[ t -> t      ]>@c   -- used for unary (-)
  40
  41 class GuestLanguageFromInteger c t where
  42   <[ fromInteger ]> :: <[ Integer -> t ]>@c
  43
  44 class GuestLanguageBool c where
  45   <[ (||) ]>       :: <[ Bool -> Bool -> Bool ]>@c
  46   <[ (&&) ]>       :: <[ Bool -> Bool -> Bool ]>@c
  47   <[ true ]>       :: <[ Bool ]>@c
  48   <[ false ]>      :: <[ Bool ]>@c
  49   <[ ifThenElse ]> :: <[ Bool -> t -> t -> t ]>@c
  50
  51 -- For heterogeneous metaprogramming, the meaning of "running" a
  52 -- program is fairly ambiguous, and moreover is highly sensitive to
  53 -- which subclasses of GuestLanguage the expression assumes it is
  54 -- dealing with.  For example, in homogeneous metaprogramming, "run"
  55 -- has this type:
  56 --
  57 --  ga_run :: forall a. (forall c. <[a]>@c) -> a
  58 --
  59 -- However, an expression which uses, say (*) at level 1 will never
  60 -- be able to be passed to this expression, since
  61 --
  62 --   square :: forall c t. GuestLanguageMult ct => <[t]>@c -> <[t]>@c
  63 --   square x = <[ ~~x * ~~x ]>
  64 --
  65
  66 -- So even though this expression is polymorphic in the environment
  67 -- classifier "c", it isn't "polymorphic enough".  This isn't merely a
  68 -- technical obstacle -- the more features you assume the guest
  69 -- language has, the more work the "run" implementation is obligated
  70 -- to perform, and the type system must track that obligation.
  71 --
  72 -- The upshot is that we can define special-purpose "run" classes such as:
  73 --
  74 --   class GuestLanguageRunMult t where
  75 --     ga_runMult :: forall a. (forall c. GuestLanguageMult c t => <[a]>@c) -> a
  76 --
  77 -- Any implementation of this class will need to know how to interpret
  78 -- the (*) operator.  Unfortunately, to my knowledge, there is no way
  79 -- to quantify over type classes in the Haskell type system, which is
  80 -- what we would need to define a type-class-indexed version of the
  81 -- GuestLanguageRun class; if we could do that, then we would have:
  82 --
  83 --   class GuestLanguageRun ( t ::: * -> TYPECLASS ) where
  84 --     ga_runMult :: forall a. (forall c. TYPECLASS c => <[a]>@c) -> a
  85 --
  86 -- It might be possible to pull this of using type families; I need to
  87 -- look into that.