{-# LANGUAGE NoMonomorphismRestriction, Rank2Types #-} -- Checking to see what could go wrong if we don't have the -- quantification over s module Unsafe where import TSCore import TSCPS import Unsafe.Coerce import Control.Applicative import Data.IORef -- The unsafe version of lam without the quantification over s. -- `Bad examples' in this file won't type check in our framework. -- We have to deliberately break it, introducing unsafeLam: unsafeLam :: (Functor m, SSym repr, LamPure repr) => (HV (H repr s a,h) repr a -> J m (HV (H repr s a,h) repr) b) -> J m (HV h repr) (a->b) unsafeLam f = lam (\x -> (unsafeCoerce (f (unsafeCoerce x)))) unsafeLamL :: (Functor m, Monad m, SSym repr, LamLPure repr) => (HV (H repr s a,h) repr a -> J (State Label m) (HV (H repr s a,h) repr) b) -> J (State Label m) (HV h repr) (a->b) unsafeLamL f = lamL (\x -> (unsafeCoerce (f (unsafeCoerce x)))) -- Simple illustration of well-labelling ex0 = lamL(\x -> lamL(\y -> weaken (var x) +: var y)) ex0c = "\\x_0_0 -> \\x_1_1 -> (GHC.Num.+) x_0_0 x_1_1" == runCLI ex0 -- ------------------------------------------------------------------------ -- Illustration that well-scoped de Bruijn indices -- do not statically determine lexical scope -- Example from Sec 3.3 (p822) of -- Chiyan Chen and Hongwei Xi -- Meta-Programming Through Typeful Code Representation -- JFP, 2005 -- We translate the example to our framework and embellish a bit -- We must use unsafeLam to write the example illustrating the -- problem. We cannot write the example in our framework without -- breaking it, fortunately. -- Inferred type exCX1 :: (Applicative m, SSym repr, LamPure repr) => (J m (HV (H repr s1 b, (H repr s a, h)) repr) b -> J m (HV (H repr s1 b, (H repr s a, h)) repr) c) -> J m (HV h repr) (a -> b -> c) exCX1 f = unsafeLam(\y ->unsafeLam (\x -> f (var x))) -- We demonstrate that depending on the argument of exCX1, we -- obtain the code with the different mappings between -- binding and reference occurrences of the variable. -- Thus the mapping -- the scoping -- cannot be statically determined -- just by looking at the exCX1 code, or its type. exCX1_c1 = "\\x_0 -> \\x_1 -> x_1" == runCI (exCX1 id) permute_env = J . fmap (hmap (\ (y,(x,z)) -> (x,(y,z)))) . unJ exCX1_c2 = "\\x_0 -> \\x_1 -> x_0" == runCI (exCX1 permute_env) -- To write exCX1 without unsafeLam, we have to give f a higher-rank -- type -- For example exCX2 :: (Applicative m, SSym repr, LamPure repr) => (forall h. J m (HV h repr) b -> J m (HV h repr) c) -> J m (HV h repr) (a -> b -> c) exCX2 f = lam(\y -> lam (\x -> f (var x))) exCX2_c1 = "\\x_0 -> \\x_1 -> x_1" == runCI (exCX2 id) -- But exCX2_c2 would not type. Indeed, the signature of -- exCX2 promised that the function f maps one piece of the -- future-stage code to another piece, in exactly the same -- environment. Moreover, the function f won't even look -- at that environment. The argument to exCX2_c2 below certainly -- fails that promise. {- exCX2_c2 = runCI (exCX2 permute_env) Couldn't match expected type `h' against inferred type `(t, (t, t1))' `h' is a rigid type variable bound by the polymorphic type `forall h. J TSCore.Identity (HV h TSCore.C) b -> J TSCore.Identity (HV h TSCore.C) c' Expected type: J TSCore.Identity (HV h TSCore.C) a Inferred type: J TSCore.Identity (J ((->) (t, (t, t1))) TSCore.C) a In the first argument of `exCX2', namely `permute_env' -} -- We could try giving exCX a more precise type. We still have to -- use the quantification, to prevent 's' from escaping exCX3 :: (Applicative m, SSym repr, LamPure repr) => (forall h1 h2. J m (HV (h1,(h2,h)) repr) b -> J m (HV (h1,(h2,h)) repr) c) -> J m (HV h repr) (a -> b -> c) exCX3 f = lam(\y -> lam (\x -> f (var x))) exCX3_c1 = "\\x_0 -> \\x_1 -> x_1" == runCI (exCX3 id) -- Now the signature anticipates that f transforms two pieces -- of future-stage code in the environment that has at least two -- slots. The signature says that f will keep the order of these -- slots. But the argument of exCX3 certainly does not. -- The type-checker complains, with a precise error message. {- exCX3_c2 = runCI (exCX3 permute_env) Couldn't match expected type `h1' against inferred type `h2' `h1' is a rigid type variable bound by the polymorphic type `forall h1 h2. J TSCore.Identity (HV (h1, (h2, ())) TSCore.C) b -> J TSCore.Identity (HV (h1, (h2, ())) TSCore.C) c' `h2' is a rigid type variable bound by the polymorphic type `forall h1 h2. J TSCore.Identity (HV (h1, (h2, ())) TSCore.C) b -> J TSCore.Identity (HV (h1, (h2, ())) TSCore.C) c' Expected type: J TSCore.Identity (HV (h1, (h2, ())) TSCore.C) b1 Inferred type: J TSCore.Identity (J ((->) (h2, (h1, ()))) TSCore.C) b1 In the first argument of `exCX3', namely `permute_env' -} -- Finally, we try to give exCX signature to specifically permit -- the argument function f to shuffle the environment -- It won't type then, because the `names', the quantified variable -- associated with y and the quantified variable associated with x -- got mixed up. {- exCX4 :: (Applicative m, SSym repr, LamPure repr) => (forall h1 h2. J m (HV (h1,(h2,h)) repr) a -> J m (HV (h2,(h1,h)) repr) a) -> J m (HV h repr) (a -> a -> a) exCX4 f = lam(\y -> lam (\x -> f (var x))) Couldn't match expected type `s' against inferred type `s1' Expected type: HV (H repr s a, (H repr s1 a, h)) repr a Inferred type: HV (H repr s1 a, (H repr s a, h)) repr a -} -- The following type-checks though -- since applying f twice restores the order exCX5 :: (Applicative m, SSym repr, LamPure repr) => (forall h1 h2. J m (HV (h1,(h2,h)) repr) a -> J m (HV (h2,(h1,h)) repr) a) -> J m (HV h repr) (a -> a -> a) exCX5 f = lam(\y -> lam (\x -> f (f (var x)))) -- But now the following won't type. We promised that the argument of -- exCX5 shall swap the two slots in the environment. {- exCX5_c1 = runCI (exCX5 id) Expected type: J TSCore.Identity (HV (h2, (h1, ())) TSCore.C) a1 Inferred type: J TSCore.Identity (HV (h1, (h2, ())) TSCore.C) a1 -} -- The following types, but the result shows that the variable reference -- corresponds to the inner binding, which has been apparent from exCX5 -- code. No surprises here. exCX5_c2 = "\\x_0 -> \\x_1 -> x_1" == runCI (exCX5 permute_env) -- The following type-checks too exCX6 :: (Applicative m, SSym repr, LamPure repr) => (forall h1 h2 h3 h4. J m (HV (h1,(h2,h)) repr) a -> J m (HV (h3,(h4,h)) repr) a) -> J m (HV h repr) (a -> a -> a) exCX6 f = lam(\y -> lam (\x -> f (var x))) -- but it can only mean that f does not depend on the first two -- slots in the environment. The function f certainly can be a constant -- function. There would not be any variable references in the generated -- code then, regardless of the particular argument we pass to exCX6. -- Again, we determine the scope just by looking at the types. exCX6_c3 = "\\x_0 -> \\x_1 -> 5" == runCI (exCX6 (const (int 5))) -- Recall exCX1 again; let's apply it to a particular function f -- as below. The result may be given the shown type exCX11 :: (Applicative m, SSym repr, LamPure repr) => J m (HV h repr) (Int -> Int -> Int) exCX11 = exCX1 permute_env -- Let's beta-expand, introducing a beta-redex into a generated code exCX7 f = unsafeLam(\y -> unsafeLam (\dummy -> {- beta-redex -} unsafeLam (\x -> f (var x))) $$ (unsafeLam (\z -> var z))) {- beta-redex -} -- Unexpectedly, that has changed the type of the application! {- exCX71 :: (Applicative m, SSym repr, LamPure repr) => J m (HV t repr) (Int -> Int -> Int) exCX71 = exCX7 permute_env Couldn't match expected type `Int' against inferred type `a -> a' Expected type: J m (HV (H repr s2 Int, (H repr s1 (a -> a), (H repr s Int, t))) repr) Int Inferred type: J m (J ((->) (H repr s2 (a -> a), (H repr s1 Int, (H repr s Int, t)))) repr) Int -} -- Now check what happens with labelling exCXL1 f = unsafeLamL(\y ->unsafeLamL (\x -> f (var x))) exCX1L_c1 = "\\x_0_0 -> \\x_1_1 -> x_1_1" == runCLI (exCXL1 id) -- The following typechecks exCXL1_c2 = runCLI (exCXL1 permute_env) -- But running fails the run-time well-labellness test {- *Unsafe> exCXL1_c2 "*** Exception: Ill-labeled: got varname x_0_0 but expected the label 1 -} -- ------------------------------------------------------------------------ -- Reproducing the example from Sec 6.4 of -- Ik-Soon Kim, Kwangkeun Yi, Cristiano Calcagno -- A Polymorphic Modal Type System for Lisp-Like Multi-staged Languages -- POPL 2006 -- let val a = ref `1 -- val f = `(fn x -> fn y -> ,(a := `(x + y); `2)) -- val g = `(fn y -> fn z -> ,(!a)) -- Again we have to use unsafeLam to type check the example. -- Our type system does not permit such a blatant scope extrusion exKYC1 :: (SSym repr, LamPure repr) => J IO (HV h repr) (Int -> Int -> Int) exKYC1 = J $ do a <- unJ (int 1) >>= newIORef f <- unJ $ unsafeLam (\x -> unsafeLam (\y -> J ( unJ ((weaken (var x) +: var y)) >>= writeIORef a >> unJ (int 2)))) g <- unJ $ unsafeLam (\y -> unsafeLam (\z -> J $ readIORef a)) return g exKYC1_c = fmap ("\\x_0 -> \\x_1 -> (GHC.Num.+) x_0 x_1" ==) $ runC exKYC1 -- Indeed, inserting just one safe lam triggers the ire of the type checker {- exKYC2 = J $ do a <- unJ (int 1) >>= newIORef f <- unJ $ lam (\x -> unsafeLam (\y -> J ( unJ ((weaken (var x) +: var y)) >>= writeIORef a >> unJ (int 2)))) g <- unJ $ unsafeLam (\y -> unsafeLam (\z -> J $ readIORef a)) return g Inferred type is less polymorphic than expected Quantified type variable `s' is mentioned in the environment: a :: IORef (HV (H repr s1 Int, (H repr s Int, h)) repr Int) -} -- The obvious problem with exKYC1 is that inserting a beta-redex -- breaks the code -- That is, exKYC3 still type-checks -- but its inferred type is different: -- exKYC3 :: (SSym repr, LamPure repr) => -- IO (HV (H repr s Int, h) repr (Int -> Int -> Int)) exKYC3 = J $ do a <- unJ (int 1) >>= newIORef f <- unJ $ unsafeLam (\x -> unsafeLam (\dummy -> {- beta-redex -} unsafeLam (\y -> J ( unJ ((weaken (weaken (var x)) +: var y)) >>= writeIORef a >> unJ (int 2)))) $$ int 100) {- beta-redex -} g <- unJ $ unsafeLam (\y -> unsafeLam (\z -> J $ readIORef a)) return g -- and so the whole program, which includes the running of the generator, -- breaks. {- exKYC3_c = runC exKYC3 Couldn't match expected type `()' against inferred type `(H repr s Int, h)' Expected type: IO (HV () TSCore.C a) Inferred type: IO (HV (H repr s Int, h) repr (Int -> Int -> Int)) -} -- Checking labelling exKYCL :: (SSym repr, LamLPure repr) => J (State Label IO) (HV h repr) (Int -> Int -> Int) exKYCL = J $ do a <- unJ (int 1) >>= liftState . newIORef f <- unJ $ unsafeLamL (\x -> unsafeLamL (\y -> J ( unJ ((weaken (var x) +: var y)) >>= liftState . writeIORef a >> unJ (int 2)))) g <- unJ $ unsafeLamL (\y -> unsafeLamL (\z -> J $ liftState $ readIORef a)) return g -- So, exKYCL is indeed ill-labelled exKYCL_c = runCL exKYCL {- "*** Exception: Ill-labeled: got varname x_1_3 but expected the label 1 -} -- ------------------------------------------------------------------------ -- Insidious scope extrusion due to exceptions / delimited control -- Although the body of `abort' (see uxs8) may be within the -- apparent scope of lam, in the generated code it will be outside -- the scope. -- The following example from TSCPS didn't type {- exs8 = reset (lam (\x -> int 1 +: abort (var x)) $$ int 100) -} -- and it still doesn't type, for a different reason: the structure -- of the environment differs (the outside of lam has a shorter env) -- Even the system with well-scoped de Bruijn indices would have -- caught this: x has the index 0 but appears as the result of -- an expression that has the context -1 (no binding lambda) {- uxs80 = reset (unsafeLam (\x -> int 1 +: abort (var x)) $$ int 100) -} -- However, if we use the leaked x under another lambda (in the environment -- where the index 0 is valid again), no problems are detected -- uxs8 :: (SSym repr, LamPure repr) => J (CPS w) (HV h repr) (Int -> Int) uxs8 = reset (unsafeLam (\x -> int 1 +: abort (unsafeLam (\u -> (var x))))) -- The code is well-typed and well-formed, but not intended since the -- variable 'x' got `renamed' into the variable 'u' when it was smuggled out uxs8c = "\\x_0 -> x_0" == runCCPS uxs8 -- without unsafeLam, we get the very precise error telling us that -- although two environments are structurally the same, -- (H repr s1 Int, h2) and (H repr s Int, h2) -- they contain variables bound at different sites. Therefore, -- these environments can't be mixed! {- uxs8' = reset (lam (\x -> int 1 +: abort (lam (\_ -> (var (x)))) )) Couldn't match expected type `s1' against inferred type `s' Expected type: HV (H repr2 s1 Int, h2) repr2 Int Inferred type: HV (H repr2 s Int, h2) repr2 Int -} -- The example uxs8 is brittle in the same way as exKYC -- If we introduce a seemingly innocuous beta-redex (beta-expand the code) -- we break the code {- uxs83 = reset (unsafeLam (\x -> int 1 +: abort ( unsafeLam (\dummy -> {- beta-redex -} unsafeLam (\u -> (var x))) $$ unsafeLam (\y-> var y) {- beta-redex -} ))) Occurs check: cannot construct the infinite type: h = (H repr s (a -> a), h) Expected type: J (CPS (J ((->) h) repr (a1 -> a1))) (J ((->) h) repr) (a1 -> a1) Inferred type: J (CPS (J ((->) h) repr (a1 -> a1))) (HV (H repr s (a -> a), h) repr) (a1 -> Int) -} -- One may think that we need weaken (although the beta-expansion -- was introduced *outside* lam (\x -> ...), and so, no -- weaken should be necessary -- it breaks for a different, seemingly bizarre reason {- uxs84 = reset (unsafeLam (\x -> int 1 +: abort ( unsafeLam (\dummy -> {- beta-redex -} unsafeLam (\u -> weaken (var x))) $$ unsafeLam (\y-> var y) {- beta-redex -} ))) Couldn't match expected type `a -> a' against inferred type `Int' Expected type: J (CPS (J ((->) h) repr ((a -> a) -> a -> a))) (J ((->) h) repr) ((a -> a) -> a -> a) Inferred type: J (CPS (J ((->) h) repr ((a -> a) -> a -> a))) (HV h repr) ((a -> a) -> Int) -} -- We understand the reason if we change the type of the beta-redex -- It shouldn't matter. But it does. -- It now type-checks uxs85 = reset (unsafeLam (\x -> int 1 +: abort ( unsafeLam (\dummy -> {- beta-redex -} unsafeLam (\u -> weaken (var x))) $$ int 100 {- beta-redex -} ))) -- but the generated code has a totally different binding structure -- No wonder changing the type of dummy had such an effect uxs85c = "(\\x_0 -> \\x_1 -> x_0) 100" == runCCPS uxs85 -- The following attempt to let-bind x outside its lam is prevented -- by the s-quantification -- ex4f1 = lam (\x -> int 1 +: genlet (var x)) -- without s, the attempt succeeds ux4f1 = unsafeLam (\x -> int 1 +: genlet (var x)) -- The inferred type is nonsense: the answer-type is the richer environment {- ux4f1 :: (SSym repr, SymLet repr, LamPure repr) => J (CPS (HV (H repr s Int, h) repr w)) (HV h repr) (Int -> Int) -} -- So, the error will be detected eventually. But the error message would -- be cryptic and the error will be detected far from the place it is -- committed -- ux4f1c = runCCPS ux4f1 -- Still, with contrivance, the type could be made sense of ux4f2 = reset $ weaken $ unsafeLam (\x -> int 1 +: genlet (var x)) -- Again, the problem is using a term in a unrelated environment, -- albeit with the same structure ux4f2c = "\\x_0 -> let z_1 = x_0\n in \\x_2 -> (GHC.Num.+) 1 z_1" == runCCPS (lam (\u -> ux4f2)) -- The code is well-typed and well-formed, but not intended since the -- variable 'x' got `renamed' into the variable 'u' when it was smuggled -- Errors like these become subtle if we use mutation, real or emulated, -- to move the code around. Without the protection of 's', we move the -- code with and unwittingly `rename' the variables.