{-# 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