Re: Deprecating Safe Haskell, or heavily investing in it?

I think some flavor / iterations of lambda bot has used it for example. On Fri, Jan 13, 2023 at 1:44 PM Jaro Reinders wrote: > I do agree that Safe Haskell would be useful even if it was only used for > enforcing type safety and avoiding accidental use of unsafe features, but > the &

Re: Deprecating Safe Haskell, or heavily investing in it?

I do agree that Safe Haskell would be useful even if it was only used for enforcing type safety and avoiding accidental use of unsafe features, but the paper [1] makes it quite clear that one of the main goals is to safely execute untrusted code: "Safe Haskell makes it possible to co

Re: Deprecating Safe Haskell, or heavily investing in it?

Indeed type safety is exactly what it’s for! The other notions of safety were never part of the goals. And it was designed so that the end user could decide which codes they deem trustworthy. On Wed, Dec 28, 2022 at 6:04 PM davean wrote: > The only part of Safe Haskell I ever really cared ab

Re: Deprecating Safe Haskell, or heavily investing in it?

The only part of Safe Haskell I ever really cared about was type safety. That's what matters, I think. I've wanted to use it a number of times and played with it, but it's never actually managed to become an important part of anything for me. So take that as you will. I'd love it if it worked

Re: Deprecating Safe Haskell, or heavily investing in it?

On Tue, Dec 27, 2022 at 08:33:04PM -0700, Chris Smith wrote: > This conversation reminds me of a parable I encountered somewhere, in which > someone declares "I don't understand why this decision was ever made, and I > we should change it", and someone responds, "No, if you don't understand > the

Re: Deprecating Safe Haskell, or heavily investing in it?

I hope that some effort can be expended to specifically identify what changes would be necessary to make Safe Haskell work consistent with its name. Only then can a reasoned decision about how to proceed be made. Also, rejecting the status quo implies that making a decision is a high priority

Re: Deprecating Safe Haskell, or heavily investing in it?

and crude analogies that completely miss what's unique and interesting about SafeHaskell in the first place. On Tue, Dec 27, 2022, 10:10 AM Hécate wrote: > Hi everyone, and happy holidays. > > I am looking into whether or not Safe Haskell is still worth maintaining. > > Currentl

Re: Deprecating Safe Haskell, or heavily investing in it?

I have implemented something like that actually:  https://github.com/cgohla/pledgeWorking out a portable API could be difficult.Sent from my Galaxy Original message From: Hécate Date: 27/12/22 20:39 (GMT+00:00) To: ghc-devs@haskell.org Subject: Re: Deprecating Safe Haskell

Re: Deprecating Safe Haskell, or heavily investing in it?

Hello, I disagree that Safe Haskell is a failed experiment, and I think with a little work could be a very valuable tool for auditing Haskell source code. The main change I think we should make is to completely remove the source code annotations, and instead expose an external mechanism (e.g

Re: Deprecating Safe Haskell, or heavily investing in it?

Something based upon eBPF would certainly incur less modifications to > the RTS? Indeed, it would be simpler to leverage existing virtualisation and/or containerisation technologies, than build a new microkernel within the RTS. Consequently, I guess I am saying that "Safe Haskell"

Re: Deprecating Safe Haskell, or heavily investing in it?

On Tue, Dec 27, 2022 at 10:31:07PM +0100, Jaro Reinders wrote: > The bytestring package does have run time bounds checks. So maybe Safe > Haskell is safer than you think? No. The safety depends on careful Safe/Unsafe marking of an unmanageable and growing set of modules. How does GH

Re: Deprecating Safe Haskell, or heavily investing in it?

The bytestring package does have run time bounds checks. So maybe Safe Haskell is safer than you think? On December 27, 2022 9:12:44 PM GMT+01:00, Viktor Dukhovni wrote: >On Tue, Dec 27, 2022 at 06:09:59PM +0100, Hécate wrote: > >> Now, there are two options (convenient!) that ar

Re: Deprecating Safe Haskell, or heavily investing in it?

Viktor Dukhovni writes: > On Tue, Dec 27, 2022 at 06:09:59PM +0100, Hécate wrote: > >> Now, there are two options (convenient!) that are left to us: >> >> 1. Deprecate Safe Haskell: We remove the Safe mechanism as it exists >> today, and keep the IO

Re: Deprecating Safe Haskell, or heavily investing in it?

of that? Something based upon eBPF would certainly incur less modifications to the RTS? Le 27/12/2022 à 21:12, Viktor Dukhovni a écrit : On Tue, Dec 27, 2022 at 06:09:59PM +0100, Hécate wrote: Now, there are two options (convenient!) that are left to us: 1. Deprecate Safe Haskell: We remove

Re: Deprecating Safe Haskell, or heavily investing in it?

On Tue, Dec 27, 2022 at 06:09:59PM +0100, Hécate wrote: > Now, there are two options (convenient!) that are left to us: > > 1. Deprecate Safe Haskell: We remove the Safe mechanism as it exists > today, and keep the IO restriction under another name. This will > certainly cause m

Deprecating Safe Haskell, or heavily investing in it?

Hi everyone, and happy holidays. I am looking into whether or not Safe Haskell is still worth maintaining. Currently there are two sides on which Safe Haskell hurts us: 1. GHC Development 2. Library development For point n°1: You can easily take the measure of what Safe Haskell raises in GHC

Re: Is Safe Haskell intended to allow segfaults?

* Mikhail Glushenkov: > Hi, > > On 9 August 2016 at 01:32, David Terei wrote: >> I imagine in Java, that I can construct an invalid pointer in foreign >> code, and then cause segfaults without the Java code having any >> issues. Just guessing at this, so very interested to

Re: Is Safe Haskell intended to allow segfaults?

On 2016-08-12 20:37, Edward Kmett wrote: > What about consuming Storable Vectors carefully, or simply working > parameterized over vector type, where Storable vectors are one of the > options? > There was actually a great paper about a very similar thing (i.e. "here's the usual interface" vs.

Re: Is Safe Haskell intended to allow segfaults?

ing what bins it falls into and to track that >>>> while type checking, etc. >>>> >>> >>> Well, *maybe* it is a slippery slope that leads to a full effect >>> system. But I'd like to see these issues enumerated. Does memory safety >>> as a goal really involve so many different effects? Do you think there >>> will be 1, 3, 10, or 100 things beyond Foreign.Ptr to worry about? >>> >>> 3.) On the other hand, someone could _build_ an effect system in Haskell >>>> that happens to sit on top of IO, holding effects in an HList, undischarged >>>> nullary class constraint, etc. >>>> >>> >>> Well, sure, I hope we will continue to aim for this as well. This is >>> effectively what we do with our "LVish" Par monad, where we use Safe >>> Haskell to ensure users cannot break the effect system in -XSafe code. >>> >>> Best, >>> -Ryan >>> >> >> > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Is Safe Haskell intended to allow segfaults?

ing what bins it falls into and to track that >>> while type checking, etc. >>> >> >> Well, *maybe* it is a slippery slope that leads to a full effect >> system. But I'd like to see these issues enumerated. Does memory safety >> as a goal really involv

Re: Is Safe Haskell intended to allow segfaults?

erated. Does memory safety as a goal > really involve so many different effects? Do you think there will be 1, 3, > 10, or 100 things beyond Foreign.Ptr to worry about? > > 3.) On the other hand, someone could _build_ an effect system in Haskell >> that happens to sit on top of

Re: Is Safe Haskell intended to allow segfaults?

Hi Simon, On Wed, Aug 10, 2016 at 4:24 AM, Simon Marlow > wrote: > Definining a safe subset of IO is usually an application-specific > decision, e.g. do you want to allow access to the filesystem but without >

Re: Is Safe Haskell intended to allow segfaults?

> 3.) On the other hand, someone could _build_ an effect system in Haskell >> that happens to sit on top of IO, holding effects in an HList, undischarged >> nullary class constraint, etc. >> > > Well, sure, I hope we will continue to aim for this as well. This is >

Re: Is Safe Haskell intended to allow segfaults?

Right - Safe Haskell provides the minimum that you need to be able to safely run untrusted code: the ability to trust the type system and the module system. Definining a safe subset of IO is usually an application-specific decision, e.g. do you want to allow access to the filesystem but without

Re: Is Safe Haskell intended to allow segfaults?

the utility of Safe Haskell to me. Many of them expose a few combinators here and there that happen to live in IO and I can view offering Safe or Trustworthy to users as a 'the pure stuff looks really pure' guarantee. For the most part it 'just works' and Trustworthy annotations can be put in when

Re: Is Safe Haskell intended to allow segfaults?

Heh, ok, segfaults themselves are a red herring. More precisely: The operational semantics for a SafeIO language should always accurately model its memory state. The application should not compute (take a step in the semantics) in a way that exposes corrupt memory or arbitrary undefined

Re: Is Safe Haskell intended to allow segfaults?

On Tue, Aug 9, 2016 at 4:19 PM, Edward Z. Yang wrote: > If you can execute subprocesses, you could always spawn gdb to > attach via ptrace() to the parent process and then poke around > memory. > Don't even need that if you're just talking segfaults, you can always spawn a

Re: Is Safe Haskell intended to allow segfaults?

I'm hearing that Safe Haskell is great for pure use cases (lambda bot). But that doesn't depend on being able to write arbitrary IO code inside the Safe bubble, does it? In fact *all* of IO could be outside the safe boundary for this use case, could it not? Are there any existing cases where

Re: Is Safe Haskell intended to allow segfaults?

I've always treated Safe Haskell as "Safe until you allow IO" -- in that all 'evil' things get tainted by an IO type that you can't get rid of by the usual means. So if you go to run pure Safe Haskell code in say, lambdabot, which doesn't give the user a means to execute IO, it can'

Re: Is Safe Haskell intended to allow segfaults?

FFI calls. > > When someone, e.g. Bob Harper > <https://existentialtype.wordpress.com/2012/08/14/haskell-is-exceptionally-unsafe/>, > points out a problem in Haskell, we sometimes respond "hey, *Safe Haskell* > is the real objet d'art! It's a safe language." Yet it isn't r

Re: Is Safe Haskell intended to allow segfaults?

https://existentialtype.wordpress.com/2012/08/14/haskell-is-exceptionally-unsafe/>, points out a problem in Haskell, we sometimes respond "hey, *Safe Haskell* is the real objet d'art! It's a safe language." Yet it isn't really a full *language* if people cannot write and run programs i

Re: Is Safe Haskell intended to allow segfaults?

Hi, On 9 August 2016 at 01:32, David Terei wrote: > I imagine in Java, that I can construct an invalid pointer in foreign > code, and then cause segfaults without the Java code having any > issues. Just guessing at this, so very interested to know how it's > prevented if I

Re: Is Safe Haskell intended to allow segfaults?

n are really internal to the language. My > interest is in a type safe language with a memory model in the IO monad. I > think it's quite reasonable to expect Safe Haskell to be as safe as Java! > There are hundreds of thousands or millions of lines of code written in the > IO monad [1], and

Re: Is Safe Haskell intended to allow segfaults?

y to lock down IO -- > but that's not really the issue here. > > Sure, there are many use cases that require an RIO newtype, but the memory > model and memory protection are really internal to the language. My > interest is in a type safe language with a memory model *in the IO mon

Re: Is Safe Haskell intended to allow segfaults?

1. Redefine -XSafe to guarantee something about IO and its memory safety (and even its memory model) 2. Add a fourth safety level, "SafeExceptIO", that corresponds to the current guarantees, while extending "Safe" to say something about IO. 3. Leave safe Haskell as it i

Re: Is Safe Haskell intended to allow segfaults?

Hello Ryan, The guarantee that Safe Haskell gives with regards to IO is a little subtle and is mentioned in Section 3.1 of the paper, and detailed in Section 5.1. Essentially, to use Safe Haskell, you are responsible for defining the type at which untrusted code is to be called. Using

Re: Is Safe Haskell intended to allow segfaults?

> > Pretty sure it's impossible to allow IO without enabling all of it one way > or another. And as soon as you allow *any* IO, you're open to various kinds > of failures including segfaults. The only way you will get your type system > to prevent that is fully specified dependent typing both in

Re: Is Safe Haskell intended to allow segfaults?

On Mon, Aug 8, 2016 at 1:27 PM, Ryan Newton <rrnew...@gmail.com> wrote: > As usual? So it is ok to segfault GHC? Elsewhere it says "in the safe > language you can trust the types", and I'd always assumed that meant Safe > Haskell is a type safe language, even in the I

Is Safe Haskell intended to allow segfaults?

We're trying to spend some cycles pushing on Safe Haskell within the stackage packages. (It's looking like a slog.) But we're running up against some basic questions regarding the core packages and Safe Haskell guarantees. The manual currently says: <https://downloads.haskell.org/~ghc/lat

Re: Generalized Newtype Deriving not allowed in Safe Haskell

; haskell Cafe | Subject: Re: Generalized Newtype Deriving not allowed in Safe Haskell | | On 10 April 2015 at 01:48, Simon Peyton Jones simo...@microsoft.com | wrote: | | prefer, such as only exporting the Coerce instance if all the | | constructors are exported, it seems that the ship

Re: Generalized Newtype Deriving not allowed in Safe Haskell

Of | David Terei | Sent: 12 April 2015 09:52 | To: Simon Peyton Jones | Cc: Omari Norman; ghc-devs@haskell.org; haskell Cafe | Subject: Re: Generalized Newtype Deriving not allowed in Safe Haskell | | On 10 April 2015 at 01:48, Simon Peyton Jones simo...@microsoft.com | wrote: | | prefer

RE: Generalized Newtype Deriving not allowed in Safe Haskell

| Subject: Re: Generalized Newtype Deriving not allowed in Safe Haskell | | On 10 April 2015 at 01:48, Simon Peyton Jones simo...@microsoft.com | wrote: | | prefer, such as only exporting the Coerce instance if all the | | constructors are exported, it seems that the ship sailed

Re: Generalized Newtype Deriving not allowed in Safe Haskell

On 12 April 2015 at 13:01, Richard Eisenberg e...@cis.upenn.edu wrote: On Apr 12, 2015, at 9:51 AM, David Terei dave.te...@gmail.com wrote: Ideally I'd like to find a way forward that works for everyone and isn't just a Safe Haskell mode setting. Agreed. I'm not convinced this can be done

Re: Generalized Newtype Deriving not allowed in Safe Haskell

On Apr 12, 2015, at 9:51 AM, David Terei dave.te...@gmail.com wrote: Ideally I'd like to find a way forward that works for everyone and isn't just a Safe Haskell mode setting. Agreed. I'm not convinced this can be done, but it's certainly worth trying. I think the first question

Re: [commit: ghc] master: Be consistent with placement of Safe Haskell mode at top of file (2a523eb)

of Safe Haskell mode at top of file Why is that necessary? Fwiw, I'm afraid that's gonna be hard to retain; it's more obvious/easier to keep all LANGUAGE pragmas in alphabetic order (I've probably done that a couple of times in `base` deliberately myself) than to introduce such an artificial

Re: [commit: ghc] master: Be consistent with placement of Safe Haskell mode at top of file (2a523eb)

Necessary is a strong statement, it's obviously not as it's style. I personally think it's better to have Safe Haskell pragmas at the top as they aren't like other pragmas, they don't just turn something on but make a hard statement about the module in question. As such it seems better to me

Safe Haskell

David Any views about https://ghc.haskell.org/trac/ghc/ticket/8827? We propose to remove the recursive check (see the ticket for what that means). Simon ___ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

Re: GND and Safe Haskell

to the designers of Safe Haskell. Richard On Nov 4, 2013, at 10:59 AM, Roman Cheplyaka r...@ro-che.info wrote: GHC HEAD still doesn't seem to recognize GND as Safe. I guess we can lift this restriction now that we have roles? Roman ___ ghc-devs mailing list

Safe Haskell and abstraction

Hi David, Joachim, Simon, and I have been trying to figure out how roles and newtype coercions fit in with Safe Haskell. (See, for example http://www.haskell.org/pipermail/ghc-devs/2013-September/002526.html, which I will try to summarize here.) It all boils down to this: Does Safe Haskell

Re: Safe Haskell validate failure

On Fri, May 10, 2013 at 09:25:42AM +0100, Simon Marlow wrote: These are still happening. Use BINDIST=YES to reproduce: = ImpSafeOnly01(normal) 22 of 124 [0, 0, 0] cd ./check/pkg01 $MAKE -s --no-print-directory mkPackageDatabase.ImpSafeOnly01 VANILLA=--disable-library-vanilla

Re: Safe Haskell validate failure

(below) from Safe Haskell.*** * ** ** Unexpected failures: ghci/scripts Defer02 [bad stderr] (ghci) indexed-types/should_fail T7786 [stderr mismatch] (normal) perf/compiler T3064 [stat too good] (normal) safeHaskell/check/pkg01

Re: Safe Haskell validate failure

I thought the parallel problems had all been resolved. I'll try to replicate locally. On 23 April 2013 01:11, Simon Peyton-Jones simo...@microsoft.com wrote: When running validate I got these failures (below) from Safe Haskell. ** ** Unexpected failures: ghci/scripts