reorganized examples directory

[coq-hetmet.git] / examples / TypeSafeRun.hs

diff --git a/examples/TypeSafeRun.hs b/examples/TypeSafeRun.hs
new file mode 100644 (file)
index 0000000..52978da
--- /dev/null
+++ b/examples/TypeSafeRun.hs
@@ -0,0 +1,35 @@
+{-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds #-}
+module TypeSafeRun
+where
+import Prelude hiding ( id, (.) )
+
+--------------------------------------------------------------------------------
+-- Examples of "running" code; these examples illustrate the sorts of
+-- scoping problems that the Taha-Nielsen environment classifiers look
+-- for in the context of HOMOGENEOUS metaprogramming.  You can't
+-- actually define these functions for ALL generalized arrows -- only
+-- those for which you've defined some sort of interpretation in Haskell.
+
+run :: forall a. (forall b. <[a]>@b) -> a
+run = undefined
+
+-- the typchecker correctly rejects this bogosity if you uncomment it:
+-- bogus = <[ \x -> ~~( run <[ x ]> ) ]>
+
+-- The Calcano-Moggi-Taha paper on environment classifier inference
+-- had a special type for closed code and two special expressions
+-- "close" and "open".  These are unnecessary in SystemFC1 where we
+-- can use higher-rank polymorphism to get the same result (although
+-- in truth it's cheating a bit since their type inference is
+-- decidable with no annotations, whereas Rank-N inference is not):
+
+data ClosedCode a = ClosedCode (forall b. <[a]>@b)
+
+open :: forall a b. ClosedCode a -> <[a]>@b
+open (ClosedCode x) = x
+
+close :: (forall b. <[a]>@b) -> ClosedCode a
+close x = ClosedCode x
+
+run_closed :: ClosedCode a -> a
+run_closed = undefined