move things out of GHC.HetMet.CodeTypes into GHC.HetMet.GuestLanguage

[ghc-base.git] / GHC / HetMet / GuestLanguage.hs

diff --git a/GHC/HetMet/GuestLanguage.hs b/GHC/HetMet/GuestLanguage.hs
new file mode 100644 (file)
index 0000000..43a391e
--- /dev/null
+++ b/GHC/HetMet/GuestLanguage.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE ModalTypes, MultiParamTypeClasses, KindSignatures, FlexibleContexts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  GHC.HetMet.GuestLanguage
+-- Copyright   :  none
+-- License     :  public domain
+--
+-- Maintainer  :  Adam Megacz <megacz@acm.org>
+-- Stability   :  experimental
+-- Portability :  portable
+
+module GHC.HetMet.GuestLanguage (
+  GuestLanguageMult, <[ (*) ]>,
+  GuestLanguageAdd,  <[ (+) ]>,
+  GuestLanguageSub,  <[ (-) ]>, <[ negate ]>,
+  GuestLanguageFromInteger, <[ fromInteger ]>,
+  GuestLanguageBool, <[ (||) ]>, <[ (&&) ]>, <[ true ]>, <[ false ]>, <[ ifThenElse ]>,
+  GuestIntegerLiteral, guestIntegerLiteral,
+  GuestStringLiteral, guestStringLiteral,
+  GuestCharLiteral, guestCharLiteral
+) where
+import Prelude (Integer, String, Char, Bool, error)
+import GHC.HetMet.GArrow
+import GHC.HetMet.CodeTypes
+
+-- 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.