haskell / rfcs Goto Github PK

Hi Haskell 2020,

After using Haskell a lot, I am now programming in Ada and Spark.
Despite that SPARK is non-functional, the tooling (using problem solvers like Z3 and cvc4) is still able to prove correctness of functions and procedures, and thus eliminating some needs for testing.
Since Haskell is a pure functional language, the proofs should be easier imho.
However, pre-, post-conditions and invariants can't be expressed in the haskell language: they can only be added in comment. See e.g. https://github.com/TorXakis/TorXakis/blob/develop/sys/valexpr/src/Boute.hs

Please consider adopting a similar approach to SPARK to specify pre- and post-conditions and invariants in Haskell.
Even when tooling can't prove the pre-, post- conditions and invariants, they can still use it as a basis for testing.

Some example

divMod :: Integer -> Integer -> (Integer, Integer)
divMod m n
  with Pre : (dinstinct n 0)
          Post: ( (let ((r (fst divMod'Result))(q (snd divMod'Result))) 
                     (and (<= 0 r (- (abs n) 1)))
                           (= m (+ (* n q) r))
                   )

add :: Integer -> Integer -> Integer
add m n
   with Invariant: add m n = add n m
           Invariant: add m 0 = m
           Invariant: add 0 n = n

Note that the invariants are comparable to the properties of property based testing.

Many classes are not completely defined by the user.
For example a class can be defined using deriving (Eq, Ord, Read, Show, Generic, NFData, Data).

Many users use coverage to determine the quality of their test set.
They aim for a high coverage number.

In Haskell 2010, when a class is defined using deriving, one has to write test code to cover the Top Level Definitions in the generated code.

Could Haskell 2020 make a distinction between user code and generate code, such that coverage only includes user code?

Currently Haskell depends on package with GPL licenses, like integer-gmp.
On some platforms this results in license issues.
I would strongly recommend only using licenses like BSD3 and MIT
such that Haskell 2020 and the product derive with it can be easily used on ALL platforms.

I'd love to see this be successful, but it seems it has stalled.

• Have the contributors lost interest?
• Is there a part of the committee process that is broken, preventing PRs from never advancing past discussion?
• Are meetings happening without notes being posted for transparency and public consumption?

If this process has not stalled it would be lovely to get an update from the team. Thanks for all the hard work!