Safe Haskell at the export symbol granularity?

[Ryan Newton]

Separate from whether or not we actually want this -- is it feasible?

Here's my situation.  When working on parallel programming libraries in Haskell there are very often unsafe operations one wants to do within an otherwise pure model.  For example, Accelerate currently violates safe haskell because it trusts the user to provide an associative function to parallel "fold".  No associativity, no referential transparency.

The solution is to put fold in a separate namespace and mark that module as Unsafe.  Likewise for certain monad-par operations that are unsafe.  But this factoring can have a serious impact.  Not only are extra modules required, but extra type classes as well.  For example, if Accelerate is ever refactored for "Safe Haskell" then the following ParAccelerate type class probably should be as well:

https://github.com/simonmar/monad-par/blob/5cc656bc45dc473d7a185ec99bb156192f54d520/abstract-par-accelerate/Control/Monad/Par/Accelerate.hs#L75

I.e. ParAccelerate & ParAccelerateUnsafe for the "unsafeHybrid" operation.

But this starts to be death by a thousand organizational factorings!  

• The package, abstract-par-accelerate, is already factored out from abstract-par just to avoid an unnecessary Accelerate dependency (which used to mean CUDA errors).  (And *another* factoring is possibly warranted for whether or not the module depends on accelerate-io.)
• The file would be separate to mark it as Safe Haskell.
• The type class ParAccelerateUnsafe would be separate so as to put it in a separate file.

What's a possible solution?  If, in addition to "Safe" and "Unsafe" modules, there were "Partially Safe" modules, which exported a mix of safe and unsafe identifiers, then this could all be much cleaner.

The simple rule is that any reference whatsoever to an unsafe identifier disqualifies the client code.  For example, in the above ParAccelerate type class we would mark the unsafeHybrid binding with something like {-# UNSAFE unsafeHybrid #-}.  We wouldn't even have to factor it out of the type class.

Likewise, Accelerate could mark "fold" as unsafe (providing safe variants as well) without introducing module namespace bloat and confusion.

What do you think?

   -Ryan

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries

[Ryan Newton]

Thanks David.

I'm glad to see it was discussed in the wiki.  (Btw, my 2 cents is that I like the comment pragmas more than new keywords.)

The issue that I think doesn't make it into the wiki is of splitting, not modules, but type-classes. That's where I think it becomes a more serious issue.

Do you think a symbol-level Safe Haskell would be able to distinguish one method of a type class as unsafe, while the others are safe?

  -Ryan

P.S. In my two examples -- 

   There's only one "Acc" type and Accelerate's "fold" can pretty easily be moved into an .Unsafe module, though it breaks the one-giant-module-for-the-whole-programming-model thing it has going now.  In the Par example on the other hand type classes are used to abstract over different implementations, so that's where we run into the safe/unsafe factoring problem.

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries

[Antoine Latter-2]

On Thu, May 17, 2012 at 8:50 AM, Ryan Newton <[hidden email]> wrote:

> Thanks David.
>
> I'm glad to see it was discussed in the wiki.  (Btw, my 2 cents is that I
> like the comment pragmas more than new keywords.)
>
> The issue that I think doesn't make it into the wiki is of splitting, not
> modules, but type-classes. That's where I think it becomes a more serious
> issue.
>
> Do you think a symbol-level Safe Haskell would be able to distinguish one
> method of a type class as unsafe, while the others are safe?
>

You can still do this at the module level, with the down-side of
potentially not being able to implement a class with the safe version:

> module Unsafe where
>
> class MyClass a where
>   safeOp :: a -> Int -> IO ()
>   unsafeOp :: a -> Int -> IO ()
>
> instance MyClass A where ...


> module Safe
>   (MyClass(safeOp))
>   where
>
> import Unsafe

I think this works.

Antoine

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries

[Ryan Newton]

Good point, Antoine!

I think that does the trick. 

On Thu, May 17, 2012 at 10:48 AM, Antoine Latter <[hidden email]> wrote:

On Thu, May 17, 2012 at 8:50 AM, Ryan Newton <[hidden email]> wrote:
> Thanks David.
>
> I'm glad to see it was discussed in the wiki.  (Btw, my 2 cents is that I
> like the comment pragmas more than new keywords.)
>
> The issue that I think doesn't make it into the wiki is of splitting, not
> modules, but type-classes. That's where I think it becomes a more serious
> issue.
>
> Do you think a symbol-level Safe Haskell would be able to distinguish one
> method of a type class as unsafe, while the others are safe?
>

You can still do this at the module level, with the down-side of
potentially not being able to implement a class with the safe version:

> module Unsafe where
>
> class MyClass a where
>   safeOp :: a -> Int -> IO ()
>   unsafeOp :: a -> Int -> IO ()
>
> instance MyClass A where ...


> module Safe
>   (MyClass(safeOp))
>   where
>
> import Unsafe

I think this works.

Antoine

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries

[David Terei-2]

On 17 May 2012 23:50, Ryan Newton <[hidden email]> wrote:
> Thanks David.
>
> I'm glad to see it was discussed in the wiki.  (Btw, my 2 cents is that I
> like the comment pragmas more than new keywords.)

Sure, the proposed syntax wasn't a serious proposal as it has
backwards compatibility issues so pragmas are the better choice. It's
just a clearer syntax when discussing the semantics of the idea.

>
> The issue that I think doesn't make it into the wiki is of splitting, not
> modules, but type-classes. That's where I think it becomes a more serious
> issue.

Thanks, I'll keep that in mind. Let me know how Antoine's suggestion
works out for you and any other feedback you have please.

>
> Do you think a symbol-level Safe Haskell would be able to distinguish one
> method of a type class as unsafe, while the others are safe?

I think so. I'm not very familiar with the type checker in GHC or
typechecking in general but looking through the code just then it
seems doable. There doesn't seem anything other than maybe some hard
engineering work that would prevent this.

~ David

>
>   -Ryan
>
> P.S. In my two examples --
>    There's only one "Acc" type and Accelerate's "fold" can pretty easily be
> moved into an .Unsafe module, though it breaks the
> one-giant-module-for-the-whole-programming-model thing it has going now.  In
> the Par example on the other hand type classes are used to abstract over
> different implementations, so that's where we run into the safe/unsafe
> factoring problem.

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries