Coq Typeclass Hierarchy

This project aims to bring a full-featured hierarchy of typeclasses for functional programming to Coq, inspired by Haskell and PureScript.

Table of Contents

Table of Contents

• Coq Typeclass Hierarchy
  • Table of Contents
  • The Hierarchy
  • Installation
  • Usage
    • Modules and Importing
    • API Documentation
  • Contributing
  • Design and Related Work

The Hierarchy

• Solid arrows point from the general to the specific - if there is an arrow from Foo to Bar it means that every Bar is a Foo.
• Green nodes are complete, with documentation and (at least one) instance(s).
• Black nodes are defined, but have no accompanying instances or documentation.
• Red nodes are incomplete, but planned.

Installation

You can build this package using the Nix package manager:

nix-build . && ls result/lib/coq/8.5/user-contrib/TypeclassHierarchy/

Alternatively, you can use the the standard

./configure && make

If you're using Nix, you can easily intergrate this library with your own package's default.nix or shell.nix, and Coq should automatically find it.

{
  stdenv,
  coq,
  pkgs ? import <nixpkgs> { }
}:
let
  coq_typeclass_hierarchy = with pkgs; callPackage (fetchFromGitHub {
    owner  = "siddharthist";
    repo   = "coq-typeclass-hierarchy";
    rev    = "c079b02364c94b7aa18fc6cb02921ad6a76eb20e"; # customize this
    sha256 = "1l5h02k0j2df4r8jvvf8nws777rda4piy2mfmvl5k2fgwz9slb1r"; # and this
  }) { };
in stdenv.mkDerivation {
  name = "my-coq-project";
  src = ./.;
  buildInputs = [ coq coq_typeclasses ];
  ...
}

Otherwise, just copy what you built to somewhere that Coq will find it.

Usage

Modules and Importing

Each module in TypeclassHierarchy.Interfaces defines all the classes that fall under that one in the tree. For instance, TypeclassHierarchy.Interfaces.Functor defines Functor, Applicative, Monad, etc.

API Documentation

You can view the documentation online, but to build it locally, run

./configure && make html && firefox html/toc.html

Contributing

Pull requests for fixes, new classes, extra instances, or more tests are welcome! Just run

nix-shell

to be dropped into a shell with all dependencies installed.

Design and Related Work

Here, we'll examine the key design principles and how they differ from similar libraries:

• Scope: This project defines only those typeclasses that have compelling use cases for functional programming. This gives us slightly more than Haskell, but fewer than PureScript.
  • math-classes is focused on building the Algebraic Hierarchy, rather than one for functional programming.
  • coq-haskell brings the Haskell typeclasses to Coq, but also includes many other parts of the Haskell standard library.
  • haskell-coq is also similar, but is limited to the Haskell typeclasses, and seems stalled at the moment.
• Bundling of Laws and Functional Extensionality: The only worthwhile instances of typeclasses are lawful ones. Therefore, this library packages the interfaces (fmap, bind) together with proofs that the laws hold. However, some laws include assertions of function equality (think fmap id = id), which is not a native concept to Coq. Therefore, we use a Setoid which encodes extensional equality and allows us to use the setoid rewriting tactics when proving it.
  • coq-haskell uses the function extensionality axiom in the limited sections where it proves the laws for its instances. This approach is less flexible than one based on Setoids, and since the library (rightly) doesn't want to require users to accept this axiom, the laws and interfaces are unbundled, as in Haskell. This causes us to lose the compile-time guarantees of Coq.