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