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