1 {-# OPTIONS -XModalTypes -XMultiParamTypeClasses -XKindSignatures -XFlexibleContexts #-}
2 module GHC.HetMet.CodeTypes (
10 GuestIntegerLiteral, guestIntegerLiteral,
11 GuestStringLiteral, guestStringLiteral,
12 GuestCharLiteral, guestCharLiteral,
13 GuestLanguageMult, <[ (*) ]>,
14 GuestLanguageAdd, <[ (+) ]>,
15 GuestLanguageSub, <[ (-) ]>, <[ negate ]>,
16 GuestLanguageFromInteger, <[ fromInteger ]>,
17 GuestLanguageBool, <[ (||) ]>, <[ (&&) ]>, <[ true ]>, <[ false ]>, <[ ifThenElse ]>
19 import Prelude (Integer, String, Char, Bool, error)
20 import GHC.HetMet.GArrow
21 import GHC.HetMet.Private
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?"
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?"
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?"
34 GArrowSTKC g (,) () =>
39 hetmet_flatten x = unG (pga_flatten x)
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:
50 pga_flatten = error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?"
55 pga_unflatten = error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?"
61 pga_flattened_id x = x
64 -- FIXME: move these and the three above to "prim" or something like that.
66 -- Technically these functions ought to be invoked *during
67 -- compilation*; in the future I would like to use Template Haskell to
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
77 class GuestLanguageConstant c t where
78 guestLanguageConstant :: t -> <[ t ]>@c
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.
85 class GuestLanguageMult c t where
86 <[ (*) ]> :: <[ t -> t -> t ]>@c
88 class GuestLanguageAdd c t where
89 <[ (+) ]> :: <[ t -> t -> t ]>@c
91 class GuestLanguageSub c t where
92 <[ (-) ]> :: <[ t -> t -> t ]>@c
93 <[ negate ]> :: <[ t -> t ]>@c -- used for unary (-)
95 class GuestLanguageFromInteger c t where
96 <[ fromInteger ]> :: <[ Integer -> t ]>@c
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
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"
111 -- ga_run :: forall a. (forall c. <[a]>@c) -> a
113 -- However, an expression which uses, say (*) at level 1 will never
114 -- be able to be passed to this expression, since
116 -- square :: forall c t. GuestLanguageMult ct => <[t]>@c -> <[t]>@c
117 -- square x = <[ ~~x * ~~x ]>
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.
126 -- The upshot is that we can define special-purpose "run" classes such as:
128 -- class GuestLanguageRunMult t where
129 -- ga_runMult :: forall a. (forall c. GuestLanguageMult c t => <[a]>@c) -> a
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:
137 -- class GuestLanguageRun ( t ::: * -> TYPECLASS ) where
138 -- ga_runMult :: forall a. (forall c. TYPECLASS c => <[a]>@c) -> a
140 -- It might be possible to pull this of using type families; I need to