-{-# OPTIONS -XModalTypes -XMultiParamTypeClasses -XKindSignatures -XFlexibleContexts #-}
+{-# LANGUAGE ModalTypes, MultiParamTypeClasses, KindSignatures, FlexibleContexts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : GHC.HetMet.CodeTypes
+-- Copyright : none
+-- License : public domain
+--
+-- Maintainer : Adam Megacz <megacz@acm.org>
+-- Stability : experimental
+-- Portability : portable
module GHC.HetMet.CodeTypes (
hetmet_brak,
hetmet_esc,
hetmet_csp,
- hetmet_flatten,
- pga_flatten,
- pga_unflatten,
- pga_flattened_id,
GuestIntegerLiteral, guestIntegerLiteral,
GuestStringLiteral, guestStringLiteral,
- GuestCharLiteral, guestCharLiteral,
- GuestLanguageMult, <[ (*) ]>,
- GuestLanguageAdd, <[ (+) ]>,
- GuestLanguageSub, <[ (-) ]>, <[ negate ]>,
- GuestLanguageFromInteger, <[ fromInteger ]>,
- GuestLanguageBool, <[ (||) ]>, <[ (&&) ]>, <[ true ]>, <[ false ]>, <[ ifThenElse ]>
+ GuestCharLiteral, guestCharLiteral
) where
-import Prelude (Integer, String, Char, Bool, error)
-import GHC.HetMet.GArrow
-import GHC.HetMet.Private
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_csp :: forall (c :: * -> * -> *). forall a. a -> a
hetmet_csp = Prelude.error "hetmet_csp should never be evaluated; did you forget to compile with -fcoqpass?"
-hetmet_flatten ::
- forall g .
- GArrowSTKCL g =>
- forall x y.
- <[ x -> y ]>@g
- ->
- (g x y)
-hetmet_flatten x = unG (pga_flatten 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 (pga_flattened_id).
--- Its only purpose is to act as a "safe type cast" during pre-flattening
--- type-inference/checking:
-pga_flatten ::
- forall g x y.
- <[ x -> y ]>@g ->
- PGArrow g x y
-pga_flatten = error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?"
-pga_unflatten ::
- forall g x y.
- PGArrow g x y ->
- <[ x -> y ]>@g
-pga_unflatten = error "hetmet_flatten should never be evaluated; did you forget to compile with -fcoqpass?"
-
-pga_flattened_id ::
- forall g x y.
- PGArrow g x y ->
- PGArrow g x y
-pga_flattened_id x = x
-
-
--- FIXME: move these and the three above to "prim" or something like that.
-
-- Technically these functions ought to be invoked *during
-- compilation*; in the future I would like to use Template Haskell to
-- do that.
guestStringLiteral :: String -> <[ String ]>@c
class GuestCharLiteral c where
guestCharLiteral :: Char -> <[ Char ]>@c
-
-
-class GuestLanguageConstant c t where
- guestLanguageConstant :: t -> <[ t ]>@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
+{-# 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.
projects / ghc-base.git / commitdiff