Thursday, May 24, 2012

A toy version of Safe Haskell

The idea of Safe Haskell is to control unsafe operations. Here is an alternative idea of implementation. Define a class

> {-# LANGUAGE FlexibleContexts, Rank2Types #-}
> class Unsafe a where
The "a" parameter is unneccessary, but it is required by GHC.

Add the unsafe constraint to each operation.

> unsafePerformIO :: Unsafe () => IO a -> a
> unsafePerformIO = undefined  -- implementation skipped

> unsafeCoerce :: Unsafe () => a -> b
> unsafeCoerce = undefined

That's it. You can now code with unsafe functions. The constraint "Unsafe" is contagious: everything that internally uses unsafe* will be tagged. Old code does not have to be changed except type signatures.

The compiler only has to prohibit users from defining instance Unsafe (). If you do this, you are releasing the brakes, and back to normal Unsafe Haskell.

Safe Haskell has "trustworthy" modules, which can use unsafe features, but their authors claim their interfaces are safe.

This idea can be implemented if there was a special function allowed in trustworthy modules removing the constraint:

> unsafe :: forall a. (Unsafe () => a) -> a
> unsafe = undefined

Of course this falls short of real Safe Haskell, which must forbid Template Haskell, overlapping instances etc. I like the fact that unsafeness of unsafePerformIO is expressed in its type.

I hope this demonstrates zero-parameter type classes might be something reasonable. For now, you can simulate them with -XConstraintKinds and -XDataKinds:

{-# LANGUAGE ConstraintKinds, KindSignatures, DataKinds #-}
class Unsafe' (a :: ())
type Unsafe = Unsafe' '()


I just realized you can have unsafe instances:

instance (Unsafe (), Show a) => Show (IORef a) where                          
  show = show . unsafePerformIO . readIORef


Edward Kmett said...

FYI- you can make a fundep to ensure only one instance can and will exist for a given class.

class Unsafe a | -> a

is legal

I use it from time to time to ensure that no further instances of a class can be constructed.

Anonymous said...

Or using more modern type machinery

class (a ~ ()) => Unsafe a

Anonymous said...

Actually, that solves the "stop people from defining an instance" problem, too.

module Unsafe(Unsafe) where

data UnsafeT = UnsafeT -- not exported
class (a ~ UnsafeT) => Unsafe a