Allow monomorphism annotations for type variables
There has been a steady proliferation of
unsafe...IO :: IO a -> a pseudo-definitions in recent years since the first appearance of
All of them (and future variations thereof!) can potentially be used to break the type system by allowing the definition of polymorphic references. In the apparent absence of progress towards finding suitable alternatives, remedial measures are sorely needed.
One widely-accepted solution is implemented via Standard ML's value restriction: prevent mutable values from receiving polymorphic types. This is done by rendering all the type's variables for such values monomorphic. This is a relatively simple process as Standard ML reserves dedicated syntax for defining references:
let val r = ref #"a" in ...
In contrast, Haskell uses functions to define mutable values with actions; these typically being monadic e.g:
newIORef :: a -> IO (IORef a)
newEmptyMVar :: IO (MVar a)
Introduce a new reserved word e.g.
monomo for rendering type variables monomorphic:
primitive newIORef :: monomo a . a -> IO (IORef a)
primitive newEmptyMVar :: monomo a . IO (MVar a)
Its use in the type signatures for such primitives would prevent the definition of polymorphic references in all contexts - the canonical example of abuse:
let v = unsafeLocalState $ newIORef undefined in do writeIORef v ("0" :: [Char]) n <- readIORef v return (n + 1 :: Int)`
...would cause a type error - the type of
undefined is also made monomorphic by the annotated type of
newIORef, resulting in the type
monomo a . IORef a for
v, preventing its dual specialisation to
IORef [Char] and
(Definitions relying on the old behaviour would be modified to use, or replaced by new primitives.)