strict-types: A type level predicate ranging over strict types

[ bsd3, library, unclassified ] [ Propose Tags ]

A type class for types T where forall x :: T . rnf x = ⊥ <=> rwhnf x = ⊥


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1.0, 0.1.0.1, 0.1.0.2, 0.1.0.3, 0.1.0.4, 0.1.0.5, 0.1.0.6, 0.1.0.7, 0.1.1, 0.1.2, 0.1.3
Dependencies array, base (<5), bytestring, containers, deepseq, hashable, text, unordered-containers, vector [details]
License BSD-3-Clause
Copyright Jose Iborra Lopez, 2017
Author Pepe Iborra
Maintainer Pepe Iborra (pepeiborra@gmail.com)
Home page https://github.com/pepeiborra/strict-types
Uploaded by PepeIborra at 2018-10-06T15:49:50Z
Distributions NixOS:0.1.3
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 6335 total (32 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2018-10-06 [all 1 reports]

Readme for strict-types-0.1.3

[back to package description]

Travis Build Status Hackage Stackage Nightly

strict-types

This package provides two pattern synonyms Strict and Rnf to constrain value strictness.

Use Strict when you can and Rnf when you must.

The Rnf pattern

The Rnf pattern matches every value of a type with an NFData instance, forcing it to rigid normal form before binding it.

> let !(Rnf x) = [trace "One" 1, trace "Two" 2]
One
Two

The bang pattern is needed to force the Rnf x closure to weak head normal form (whnf).

Rnf is very handy to avoid space leaks when working with non-strict data, but forcing structured data with rnf has a cost even if the data is already forced, and it should be avoided in inner loops. Too few Rnf patterns and one risks a space leak, too many and one ends up with squared complexity factors.

The Strict pattern

If our datatypes are strict, then their weak head normal form is already fully evaluated and Rnf is morally just seq. In practice, it depends on what the NFData instance does. One would hope it would be implemented as a noop, but in practice this is not always the case for first order types, and can never be for higher kinded types which cannot make any assumptions about the strictness of their type parameters.

But not all is lost! We can ask the typechecker to inspect the GHC Generics representation for a type to check if it is strict, and avoid calling rnf if that is the case. This is what the Strict pattern synonym does:

> let !(Strict x) = [1, 2]
<interactive>:1:7: error:
    • [Int] has an unnamed lazy field in constructor :
    • In the pattern: Strict y
      In the pattern: !(Strict y)
      In a pattern binding:
        !(Strict y) = [trace "1" 1, trace "2" (2 :: Int)]

Lists are not strict, so the expression above does not type check.

If we define our own strict list datatype with a Generic instance, the type checker can certify the property that !(Strict x) is equivalent to !(Rnf x):

> data StrictList a = Nil | Cons !a (StrictList a) deriving Generic ; infixr :!
> let !(Strict y) = trace "one" 1 :! trace "two" 2 :! Nil
two
one

The StrictType class

Not all strict types derive Generic. For such cases where the type checker is unable to see the strictness information we can "promise" that a type is deep strict by adding an instance of the StrictType class.

Caveats

Non regular recursive types, also known as nested datatypes, will cause the type checker to loop and run out of fuel when trying to prove deep strictness.

FAQ

  • What about the Strict and StrictData pragmas ?

The Strict pragma adds an implicit bang pattern on every binding, but it doesn't force values to normal form.

The StrictData pragma adds an implicit bang pattern on every field of a data type guaranteeing that first order types are strict, but does not help with higher kinded types.