General.v: add boolean and/or functions
[coq-hetmet.git] / examples / TypeSafeRun.hs
1 {-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds #-}
2 module TypeSafeRun
3 where
4 import Prelude hiding ( id, (.) )
5
6 --------------------------------------------------------------------------------
7 -- Examples of "running" code; these examples illustrate the sorts of
8 -- scoping problems that the Taha-Nielsen environment classifiers look
9 -- for in the context of HOMOGENEOUS metaprogramming.  You can't
10 -- actually define these functions for ALL generalized arrows -- only
11 -- those for which you've defined some sort of interpretation in Haskell.
12
13 run :: forall a. (forall b. <[a]>@b) -> a
14 run = undefined
15
16 -- the typchecker correctly rejects this bogosity if you uncomment it:
17 -- bogus = <[ \x -> ~~( run <[ x ]> ) ]>
18
19 -- The Calcano-Moggi-Taha paper on environment classifier inference
20 -- had a special type for closed code and two special expressions
21 -- "close" and "open".  These are unnecessary in SystemFC1 where we
22 -- can use higher-rank polymorphism to get the same result (although
23 -- in truth it's cheating a bit since their type inference is
24 -- decidable with no annotations, whereas Rank-N inference is not):
25
26 data ClosedCode a = ClosedCode (forall b. <[a]>@b)
27
28 open :: forall a b. ClosedCode a -> <[a]>@b
29 open (ClosedCode x) = x
30
31 close :: (forall b. <[a]>@b) -> ClosedCode a
32 close x = ClosedCode x
33
34 run_closed :: ClosedCode a -> a
35 run_closed = undefined