Difference between revisions of "Safe Haskell"

From HaskellWiki
Jump to navigation Jump to search
m (Added link to blog post, cleaned up layout, fixed typo)
m (Extra formatting)
 
(8 intermediate revisions by 3 users not shown)
Line 1: Line 1:
  +
{| class="wikitable" style="background-color:white" align=right
⚫
= Introduction =
 
  +
|<tt>{-# LANGUAGE Safe #-}</tt>
  +
|}
  ⚫
== Introduction ==
   
 
Safe Haskell is a Haskell language extension. It is described in detail:
  
Safe Haskell is a Haskell language extension. It is described in detail:
   
−
; ''In the GHC user manual:'' : http://www.haskell.org/ghc/docs/latest/html/users_guide/safe-haskell.html
 +
* ''The [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/ GHC user guide] has a section about Safe Haskell [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/exts/safe_haskell.html# here].''
−
; ''In the Safe Haskell paper:'' : http://community.haskell.org/~simonmar/papers/safe-haskell.pdf
 +
* ''In the Safe Haskell paper:'' : http://community.haskell.org/~simonmar/papers/safe-haskell.pdf
−
; ''Further technical discussion of Safe Haskell is on the GHC Wiki:'' : http://hackage.haskell.org/trac/ghc/wiki/SafeHaskell
 +
* ''Further technical discussion of Safe Haskell is on the GHC Wiki:'' : https://gitlab.haskell.org/ghc/ghc/wikis/safe-haskell
   
 
For a high-level overview, see this blog post: http://begriffs.com/posts/2015-05-24-safe-haskell.html.
  
For a high-level overview, see this blog post: http://begriffs.com/posts/2015-05-24-safe-haskell.html.
   
−
= In detail =
+
== In detail ==
 
 
−
As the Safe Haskell paper describes, it "hardens" the Haskell language by providing five properties: type safety, referential transparency, strict module encapsulation, modular reasoning and semantic consistency.
 +
As the Safe Haskell paper describes, it "hardens" the Haskell language by providing five properties:
  +
* type safety
  +
* referential transparency,
  +
* strict module encapsulation
  +
* modular reasoning
  +
* semantic consistency.
   
  +
=== What Safe Haskell doesn't do ===
⚫
Safe Haskell is ''not'' magic, and not about catching bugs. It does not ensure that library authors who mark modules as "Trustworthy" are not lying, or incorrect. It does not ensure code inferred safe but in IO cannot perform arbitrary IO. It ''does'' ensure that untrusted code inferred to be safe will, assuming its "Trustworthy" imports are ''indeed'' "Trustworthy" obey the above five properties. As such, again assuming "Trustworthy" imports are indeed so, Safe Haskell infers that untrusted code inferred safe and ''not'' in IO can be run without fear (aside from fear of resource over-utilization/exhaustion).
  
   
  +
It isn't:
⚫
Most code that most people want to write is going to be Safe Haskell by default. As Simon Marlow has pointed out,
 
  +
* <s>magic</s> <s>omnimiscent</s> [http://www.softpanorama.org/SE/quotes.shtml idiot-proof].
  +
* about catching bugs.
  +
* about ensuring that library authors who mark modules as <code>Trustworthy</code> are not lying, or incorrect.
  +
* about ensuring that <code>IO</code>-based code which is inferred safe cannot perform arbitrary I/O.
   
  ⚫
It ''does'' ensure that untrusted code inferred to be safe will (assuming its <code>Trustworthy</code> imports are ''indeed'' trustworthy!) obey the above five properties. As such, (again assuming <code>Trustworthy</code> imports are indeed so) Safe Haskell infers that untrusted code inferred safe and ''not'' in <code>IO</code> can be run without fear (aside from fear of resource over-utilization/exhaustion).
−
<blockquote>
  
⚫
"Normally when you use an unsafe feature, the purpose is to use it to implement a safe API - if that's the case, all you have to do is add Trustworthy to your language pragma, and the API is available to use from Safe code. 99% of Hackage should be either Safe or Trustworthy. We know that 27% is already inferred Safe (see the paper), and a lot of the rest is just waiting for other libraries to add Trustworthy where necessary."
  
−
</blockquote>
  
   
  +
=== Usage ===
−
Again, as Simon Marlow argues,
 
  ⚫
Most code that most people want to write is going to be Safe Haskell by default. As Simon Marlow has pointed out:
  +
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
  ⚫
Normally when you use an unsafe feature, the purpose is to use it to implement a safe API - if that's the case, all you have to do is add <code>Trustworthy</code> to your language pragma, and the API is available to use from <code>Safe</code> code. 99% of Hackage should be either <code>Safe</code> or <code>Trustworthy</code>. We know that 27% is already inferred <code>Safe</code> (see the paper), and a lot of the rest is just waiting for other libraries to add <code>Trustworthy</code> where necessary.
  +
</div>
   
  +
along with:
−
<blockquote>
  
  +
⚫
"For typical Haskell programmers, using <code>{-# LANGUAGE Safe #-}</code> will be like <code>-Wall</code>: something that is considered good practice from a hygiene point of view. If you don't ''need'' access to unsafe features, then it's better to write in the safe subset, where you have stronger guarantees. Just like -Wall, you get to choose whether to use <code>{-# LANGUAGE Safe #-}</code> or not."
  
  +
<div style="border-left:1px solid lightgray; padding: 1em" alt="blockquote">
−
</blockquote>
  
  ⚫
For typical Haskell programmers, using <code>{-# LANGUAGE Safe #-}</code> will be like <code>-Wall</code>: something that is considered good practice from a hygiene point of view. If you don't ''need'' access to unsafe features, then it's better to write in the safe subset, where you have stronger guarantees. Just like <code>-Wall</code>, you get to choose whether to use <br><code>{-# LANGUAGE Safe #-}</code> or not.
  +
</div>

Latest revision as of 03:00, 5 August 2021

{-# LANGUAGE Safe #-}

Introduction

Safe Haskell is a Haskell language extension. It is described in detail:

For a high-level overview, see this blog post: http://begriffs.com/posts/2015-05-24-safe-haskell.html.

In detail

As the Safe Haskell paper describes, it "hardens" the Haskell language by providing five properties:

  • type safety
  • referential transparency,
  • strict module encapsulation
  • modular reasoning
  • semantic consistency.

What Safe Haskell doesn't do

It isn't:

  • magic omnimiscent idiot-proof.
  • about catching bugs.
  • about ensuring that library authors who mark modules as Trustworthy are not lying, or incorrect.
  • about ensuring that IO-based code which is inferred safe cannot perform arbitrary I/O.

It does ensure that untrusted code inferred to be safe will (assuming its Trustworthy imports are indeed trustworthy!) obey the above five properties. As such, (again assuming Trustworthy imports are indeed so) Safe Haskell infers that untrusted code inferred safe and not in IO can be run without fear (aside from fear of resource over-utilization/exhaustion).

Usage

Most code that most people want to write is going to be Safe Haskell by default. As Simon Marlow has pointed out:

Normally when you use an unsafe feature, the purpose is to use it to implement a safe API - if that's the case, all you have to do is add Trustworthy to your language pragma, and the API is available to use from Safe code. 99% of Hackage should be either Safe or Trustworthy. We know that 27% is already inferred Safe (see the paper), and a lot of the rest is just waiting for other libraries to add Trustworthy where necessary.

along with:

For typical Haskell programmers, using {-# LANGUAGE Safe #-} will be like -Wall: something that is considered good practice from a hygiene point of view. If you don't need access to unsafe features, then it's better to write in the safe subset, where you have stronger guarantees. Just like -Wall, you get to choose whether to use
{-# LANGUAGE Safe #-} or not.

Retrieved from "https://wiki.haskell.org/index.php?title=Safe_Haskell&oldid=64673"