--- /dev/null
+{-# OPTIONS -XModalTypes -XMultiParamTypeClasses #-}
+module GHC.HetMet.CodeTypes (
+ hetmet_brak,
+ hetmet_esc,
+ hetmet_csp,
+ GuestIntegerLiteral, guestIntegerLiteral,
+ GuestStringLiteral, guestStringLiteral,
+ GuestCharLiteral, guestCharLiteral,
+ GuestLanguageMult, <[ (*) ]>,
+ GuestLanguageAdd, <[ (+) ]>,
+ GuestLanguageSub, <[ (-) ]>, <[ negate ]>,
+ GuestLanguageFromInteger, <[ fromInteger ]>,
+ GuestLanguageBool, <[ (||) ]>, <[ (&&) ]>, <[ true ]>, <[ false ]>, <[ ifThenElse ]>,
+ <[ fromp ]>
+) where
+import Prelude (Integer, String, Char, Bool, error)
+import GHC.HetMet.GArrow
+
+hetmet_brak :: forall c. forall a. a -> <[a]>@c
+hetmet_brak = Prelude.error "hetmet_brak should never be evaluated; did you forget to compile with -fcoqpass?"
+
+hetmet_esc :: forall c. forall a. <[a]>@c -> a
+hetmet_esc = Prelude.error "hetmet_esc should never be evaluated; did you forget to compile with -fcoqpass?"
+
+hetmet_csp :: forall c. forall a. a -> a
+hetmet_csp = Prelude.error "hetmet_csp should never be evaluated; did you forget to compile with -fcoqpass?"
+
+<[ fromp ]> :: forall a b . <[ a -> a ]>@b
+<[ fromp ]> = <[ \x -> x ]>
+
+{-
+-- After the flattening pass the argument and result types of this
+-- function are identical (for any instantiation), so the flattener
+-- simply turns it into the identity function. Its only purpose is to
+-- act as a "safe type cast" during pre-flattening
+-- type-inference/checking:
+hetmet_flatten ::
+ forall g.
+ GArrow g (**) =>
+ GArrowDrop g (**) =>
+ GArrowCopy g (**) =>
+ GArrowSwap g (**) =>
+ GArrowLoop g (**) =>
+ forall x y.
+ <[ x -> y ]>@g
+ ->
+ (g x y)
+hetmet_flatten _ = Prelude.error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?"
+-}
+
+class GuestIntegerLiteral c where
+ guestIntegerLiteral :: Integer -> <[ Integer ]>@c
+
+class GuestStringLiteral c where
+ guestStringLiteral :: String -> <[ String ]>@c
+
+class GuestCharLiteral c where
+ guestCharLiteral :: Char -> <[ Char ]>@c
+
+-- 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.
+
--- /dev/null
+{-# OPTIONS -XRankNTypes -XMultiParamTypeClasses -XNoMonomorphismRestriction -XTypeOperators #-}
+module GHC.HetMet.GArrow (
+ GArrow(..),
+ GArrowDrop(..),
+ GArrowCopy(..),
+ GArrowSwap(..),
+ GArrowLoop(..),
+ GArrowReify(..),
+ GArrowReflect(..)
+) where
+
+class GArrow g (**) where
+ ga_id :: g x x
+ ga_comp :: g x y -> g y z -> g x z
+ ga_first :: g x y -> g (x ** z) (y ** z)
+ ga_second :: g x y -> g (z ** x) (z ** y)
+ ga_cancell :: g (()**x) x
+ ga_cancelr :: g (x**()) x
+ ga_uncancell :: g x (()**x)
+ ga_uncancelr :: g x (x**())
+ ga_assoc :: g ((x**y)**z) (x**(y**z))
+ ga_unassoc :: g (x**(y**z)) ((x**y)**z)
+
+class GArrow g (**) => GArrowDrop g (**) where
+ ga_drop :: g x ()
+
+class GArrow g (**) => GArrowCopy g (**) where
+ ga_copy :: g x (x**x)
+
+class GArrow g (**) => GArrowSwap g (**) where
+ ga_swap :: g (x**y) (y**x)
+ --ga_second f = ga_comp (ga_comp ga_swap (ga_first f)) ga_swap
+
+class GArrow g (**) => GArrowLoop g (**) where
+ ga_loop :: g (x**z) (y**z) -> g x y
+
+class GArrow g (**) => GArrowLiteral g (**) a where
+ ga_literal :: a -> g () a
+
+-- not sure
+class GArrow g (**) => GArrowReify g (**) where
+ ga_reify :: (x -> y) -> g x y
+
+-- not sure
+class GArrow g (**) => GArrowReflect g (**) where
+ ga_reflect :: g x y -> (x -> y)
+
+
projects / ghc-base.git / commitdiff