Skip to main content

🧮 Experiment on translation from Haskell to Coq

· 5 min read

We present an experiment coq-of-hs that we have made on the translation of Haskell programs to the proof system Coq 🐓. The goal is to formally verify Haskell programs to make them totally bug-free.

Indeed, even with the use of a strict type system, there can still be bugs for properties that cannot be expressed with types. An example of such a property is the backward compatibility of an API endpoint for the new release of a web service when there has been code refactoring. Only formal verification can cover all execution cases and kinds of properties.

The code of the tool is at: github.com/formal-land/coq-of-hs-experiment (AGPL license)

Contact

We propose tools to make your codebase totally bug-free. Contact us at contact@formal.land for more information! We offer a free audit to assess the feasibility of formal verification for your case.

Info

We estimate that the cost of formal verification should be 20% of the development cost. There are no reasons to still have bugs today!

Haskell Logo

Goal of the experiment​

There are already some tools to formally verify Haskell programs:

In this experiment, we want to check the feasibility of translation from Haskell to Coq:

  • 👍 covering all the language without manual configuration or code changes,
  • 👎 even if this is at the cost of a more verbose and low-level translation.

Example​

Here is an example of a Haskell function:

fixObvious :: (a -> a) -> a
fixObvious f = f (fixObvious f)

that coq-of-hs translates to this valid Coq code:

CoFixpoint fixObvious : Val.t :=
  (Val.Lam (fun (f : Val.t) => (Val.App f (Val.App fixObvious f)))).

Infrastructure​

We read the Haskell Core representation of Haskell using the GHC plugin system. Thus, we read the exact same code version as the one that is compiled down to assembly code by GHC, to take into account all compilation options.

Haskell Core is an intermediate representation of Haskell that is close to the lambda calculus and used by the Haskell compiler for various optimizations passes. Here are all the constructors of the Expr type of Haskell Core:

data Expr b
  = Var   Id
  | Lit   Literal
  | App   (Expr b) (Arg b)
  | Lam   b (Expr b)
  | Let   (Bind b) (Expr b)
  | Case  (Expr b) b Type [Alt b]
  | Cast  (Expr b) Coercion
  | Tick  (Tickish Id) (Expr b)
  | Type  Type
  | Coercion Coercion

This paper System FC, as implemented in GHC presents it as System F plus coercions. We translate Haskell code to an untyped version of the lambda calculus in Coq, with co-induction to allow for infinite data structures:

Module Val.
  #[bypass_check(positivity)]
  CoInductive t : Set :=
  | Lit (_ : Lit.t)
  | Con (_ : string) (_ : list t)
  | App (_ _ : t)
  | Lam (_ : t -> t)
  | Case (_ : t) (_ : t -> list (Case.t t))
  | Impossible.
End Val.

We make the translation by induction over the Haskell Core representation, and we translate each constructor to a corresponding constructor of the Coq representation. We pretty-print the Coq code directly without using an intermediate representation. We use the prettyprinter package with the two main following primitives:

concatNest :: [Doc ()] -> Doc ()
concatNest = group . nest 2 . vsep

concatGroup :: [Doc ()] -> Doc ()
concatGroup = group . vsep

to display a sub-term with or without indentation when splitting lines that are too long. This translation works well on all the Haskell expressions that we have tested.

Missing features​

Semantics​

We have not yet defined a semantics. For now, the terms that we generate in Coq are purely descriptive. We will wait to have examples of things to verify to define semantics that are practical to use.

Type-classes​

We have not yet translated typeclasses. The Haskell Core language hides most of the typeclasses-related code. For example, it represents instances as additional function parameters for functions that have a typeclass constraints. But we still need to declare the functions corresponding to the member of the typeclasses, what we have not done yet.

Multi-file projects​

We have not yet implemented the translation of multi-file projects. We have only tested the translation of a single-file project.

Standard library​

Similarly to the handling of multi-file projects, we have not yet tested the translation of projects using external libraries or translating the base library of Haskell.

Strict positivity​

We had to turn off the strict positivity condition for the definition of Val.t in Coq with:

#[bypass_check(positivity)]

This is for to the case:

| Lam (_ : t -> t)

where t appears as a parameter of a function (negative position). We do not know if this causes any problem in practice, on values that correspond to well-typed Haskell programs.

Conclusion​

We have presented an experiment on the translation of Haskell programs to Coq. If you are interested in this project, please get in touch with us at contact@formal.land or go to the GitHub repository of the project.