Allow monomorphism annotations for type variables
Motivation
There has been a steady proliferation of unsafe...IO :: IO a -> a
pseudo-definitions in recent years since the first appearance of unsafePerformIO
:
unsafeLocalState
unsafeDupablePerformIO
inlinePerformIO
accursedUnutterablePerformIO
...etc.
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)
Proposal
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 IORef Int
.
(Definitions relying on the old behaviour would be modified to use, or replaced by new primitives.)