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.