Attempt to design "runParThenFreeze"

RunParThenFreeze.hs

{-# LANGUAGE RankNTypes, DataKinds, KindSignatures, MagicHash, CPP, DefaultSignatures #-}
{-# LANGUAGE TypeFamilies, TypeSynonymInstances, FlexibleInstances #-}


import GHC.Prim (unsafeCoerce#)

#if 0
import Control.LVish
import Data.LVar.IVar as IV
#else
-- Some fake versions to make the file self contained:
data IVar s a 
data Par (d::Determinism) s a
data Determinism = Det | QuasiDet
put_ :: IVar s a -> a -> Par d s ()
put_ = undefined
new :: Par d s (IVar s a)
new = undefined
runPar :: (forall s . Par Det s a) -> a
runPar = undefined
instance Monad (Par d s) where
instance Functor (Par d s) where  
#endif


-- | DeepFreezing is type-level (guaranteed O(1) time complexity)
-- operation.  It marks an LVar and its contents (recursively) as
-- frozen.  DeepFreezing is not an action that can be taken directly
-- by the user, however.  Rather it is an optional final-step in a
-- `runPar` invocation.
class DeepFreeze a where
  -- | This type function is public.  It maps pre-frozen types to
  -- frozen ones.  It should be idempotent.
  type FrzType a :: *

  -- | Private: not exported to the end user.
  frz :: a-> FrzType a

  -- | While `frz` is not exported, users may opt-in to the `DeepFreeze`
  -- class for their datatypes and take advantage of the default instance.
  -- Doing so REQUIRES that `type FrzType a = a`.
  default frz :: a -> a 
  frz a = a
  
-- | An uninhabited type that signals an LVar has been frozen.
--   LVars should use this inplace of their `s` parameter.
data Frzn

-- | An uninhabited type that signals an LVar is not only frozen, but
-- it may be traversed in whatever order its internal representation
-- dictates.
data Trvrsbl 

-- | DeepFreeze is just a type-coercion.  No bits change at runtime:
instance DeepFreeze a => DeepFreeze (IVar s a) where
  type FrzType (IVar s a) = IVar Frzn (FrzType a)
  frz = unsafeCoerce# -- unsafeCoerceLVar

instance DeepFreeze String where
  type FrzType String = String
  frz x = x

--------------------------------------------------------------------------------
-- A simple program to try to run:

-- Return a frozen version of a nested IVar (accesible from pure code).
par :: Par Det s (IVar s (IVar s String))
par = 
 do v  <- new
    v2 <- new
    put_ v v2
    put_ v2 "hi"
    return v

--------------------------------------------------------------------------------
-- Approach 1: broken:
--------------------------------------------------------------------------------

-- Simon says: try to put the proof inside the inner scope:
-- rptf :: forall b . (forall a s . (FrzType a ~ b) => Par Det s a) -> b
-- rptf = undefined

runParThenFreeze :: DeepFreeze a => (forall s . Par Det s a) -> (FrzType a)
runParThenFreeze p = runPar (freezePar p)

-- This won't typecheck:
-- ex1_broke :: IVar Frzn (IVar Frzn String)
-- ex1_broke = runParThenFreeze par


--------------------------------------------------------------------------------
-- Approach 2: works but insufficient
--------------------------------------------------------------------------------

-- Here we beak the freezing process into two phases.  But the problem is we can't
-- force the user to NOT use `freezePar` except immediately before `runPar`.

-- | Let's try something different' make it a two-step process
freezePar :: DeepFreeze a => Par d s a -> Par d s (FrzType a)  
freezePar = fmap frz

ex2 :: IVar Frzn (IVar Frzn String)
ex2 = runPar (freezePar par)