[Haskell-cafe] 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

[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.

[Antoine Latter]

On Thu, May 17, 2012 at 8:50 AM, Ryan Newton <rrne...@gmail.com> 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

_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Ryan Newton]

Good point, Antoine!

I think that does the trick. 

[David Terei]

On 17 May 2012 23:50, Ryan Newton <rrne...@gmail.com> 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.

[Gábor Lehel]

I have a related-seeming question:

Say I have a type class with methods, and some functions implemented
on top of it. The class methods are inherently unsafe. Instances of
the class are supposed to satisfy some conditions, and if those
conditions are met, the functions built on top are safe.

So say I put the class in an Unsafe module, and re-export the class
without its methods along with the derived functions in a Safe module.
For anything unsafe to happen, the Unsafe module has to be imported
somewhere. But if someone imports it and implements a bad instance,
the Safe module *also* becomes potentially unsafe! What's the
recommended practice here?

(I can't really tell if this is the same question as originally posed
by Ryan, but I think it's not.)

> _______________________________________________
> Libraries mailing list
> Libr...@haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>



--
Work is punishment for failing to procrastinate effectively.

[David Terei]

So this is a good question, sorry for the late reply. It's tricky as
the way typeclasses are imported and exported in Haskell is confusing.

Basically, instances are hard to control access to as they aren't part
of import or export statements. Importing a module that defines an
instances gives you those instances. This works transitively so you
have access to all instances defined below you in the dependency
graph.

Controlling access to a typeclass function is easy though, it works
just like a normal function. So in your example, the Safe module
wouldn't necessarily become unsafe but there is some unsatisfactory
trickiness.

- untrusted code still couldn't access the type class as the
functions for it aren't exported.
- the derived functions may or may not be safe anymore depending on
polymorphism:
- If the derived functions don't have any polymorphism that would
allow consumers of the functions to choose what underlying typeclass
is used, then the module is still safe.
- If they do, then yes untrusted code could choose what types to
use to cause the unsafe instance to be used, thus making the derived
functions unsafe. (This assumes the untrusted code has access to the
unsafe instance but as I said, this is hard to reason about since
instances are somewhat global).

there are solutions to this problem but its a tricky situation with
the solutions really being to be careful... I don't know how we could
do better. Tracking safety at the symbol level doesn't seem like it
would change this situation. Basically you want closed type classes or
a way to control what instances can be used (maybe by simply making
instances part of import/export lists) both of which are big changes
to Haskell.

I wrote some example code and a note about this stuff:

https://github.com/dterei/SafeHaskellExamples/tree/master/typeclasses

Cheers,
David

[Gábor Lehel]

Thanks for the long answer!

It just occured to me that Data.Typeable is in basically the same
situation. Data.Typeable is a Trustworthy module with a type class,
and with functions built on that class, which are safe if they are
used with types for which the instances of the class are "proper".
Using only safe modules and imports, it is not possible to subvert
that safety: instances can only be derived, and derived instances are
guaranteed to be "proper". But if someone makes a Trustworthy module
with an improper manual Typeable instance and you import it, suddenly
the functions in Data.Typeable can be unsafe, even though nothing in
that module has changed.

The only difference in my situation is that there's no
guaranteed-to-be-safe deriving mechanism, it all rests on whether the
Trustworthy modules importing my Unsafe module to write their
instances are behaving themselves.

I think one way to resolve this might be to say that Safe Haskell's
mission is to help prevent bad things from happening in a global
sense, but not necessarily to delineate which functions can or cannot
be causing the bad things once unsafeness has crept into the program.
Trustworthy modules are inherently risky: they declare of themselves
that they're trustworthy, but really, they could do anything. The
burden is on the administrator to decide what they actually trust.
What Safe Haskell says is that if the administrator does this properly
and only trusts packages/modules which are actually safe, then
programs will not behave unsafely. But if they make a bad decision and
trust an unsafe module, then whether it does the bad things directly,
or indirectly by breaking the invariants another module depends on,
doesn't make much of a practical difference. You've lost either way.

[David Terei]

On 17 June 2012 13:30, Gábor Lehel <illi...@gmail.com> wrote:
> Thanks for the long answer!

No problem. It was a nice question as it made me think of some new aspects.

Yes. This is exactly how you should think of it. If people aren't
thinking of it this way (which there is a good chance they aren't)
then Safe Haskell technically is fine but I'm failing at communicating
the design. Trustworthy modules by definition are outside the scope of
provability. So the safety very much relies on the trust you have of
trustworthy modules, that they do what you believe they do.

I will have to look at the userguide again as I think it needs a
paragraph like the one of yours above but I don't know if it does
right now.