liquidhaskell-boot-0.9.2.5.0: Liquid Types for Haskell
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Haskell.Liquid.GHC.Plugin.Tutorial

Synopsis

    Introduction and Requirements

    This tutorial describes the general approach of using LiquidHaskell using the new compiler plugin. Due to some recent changes and improvements to the compiler plugin API (which LiquidHaskell requires) the minimum supported version of GHC is 8.10.1.

    Your first package

    Generally speaking, in order to integrate LiquidHaskell (LH for brevity from now on) with your existing (or brand new) project, we need to tell GHC that we want to use the LH plugin, and it can be done by adding the -fplugin=LiquidHaskell option in the ghc-options of your Cabal manifest.

    If we do the above, our Cabal manifest should look similar to this:

    cabal-version: 1.12
    
    name:           toy-package-a
    version:        0.1.0.0
    description:    This is a toy example.
    homepage:
    bug-reports:
    author:         Author name here
    maintainer:     example@example.com
    copyright:      2019 Author name here
    license:        BSD3
    license-file:   LICENSE
    build-type:     Simple
    
    library
      exposed-modules:
          Toy.A
      hs-source-dirs:
          src
      build-depends:
            base
          , liquidhaskell                  -- Add this!
      default-language: Haskell2010
      ghc-options: -fplugin=LiquidHaskell  -- Add this!
    

    Let's now define a very simple module called A:

    module Toy.A ( notThree, one, two) where
    
    {-@ one :: {v:Int | v = 1 } @-}
    one :: Int
    one = 1
    
    {-@ assume notThree :: {v : Nat | v != 3 } @-}
    notThree :: Int
    notThree = 4
    
    {-@ two :: Nat @-}
    two :: Int
    two = one + one
    

    Now, if we build the package with (for example) cabal v2-build toy-package-a, we should see something like this:

    Resolving dependencies...
    Build profile: -w ghc-8.10.1 -O1
    In order, the following will be built (use -v for more details):
     - toy-package-a-0.1.0.0 (lib) (configuration changed)
    Configuring library for toy-package-a-0.1.0.0..
    Warning: The 'license-file' field refers to the file LICENSE which does not
    exist.
    Preprocessing library for toy-package-a-0.1.0.0..
    Building library for toy-package-a-0.1.0.0..
    
    [3 of 3] Compiling Toy.A            ( src/Toy/A.hs, ... )
    
    **** LIQUID: SAFE (7 constraints checked) **************************************
    

    The "SAFE" banner here is LH's way of saying "all is well". What happens if we try to violate a refinement? Let's find out. If change one to look like this:

    one :: Int
    one = 2
    

    Upon next recompilation, GHC (or rather, LH) will bark at us:

    Building library for toy-package-a-0.1.0.0..
    [3 of 3] Compiling Toy.A            ( src/Toy/A.hs, ... )
    
    **** LIQUID: UNSAFE ************************************************************
    
    src/Toy/A.hs:36:1: error:
        Liquid Type Mismatch
        .
        The inferred type
          VV : {v : GHC.Types.Int | v == 2}
        .
        is not a subtype of the required type
          VV : {VV : GHC.Types.Int | VV == 1}
        .
       |
    36 | one = 2
       | ^^^^^^^
    

    Using GHCi

    Using GHCi is supported out of the box, and it will work as expected.

    Passing options

    Passing options to LH is possible and works using the standard mechanism the plugin system already provides. For example let's image we want to skip verification of our A module. At this point, we have two options:

    1. We can add the option directly in the module, as a "pragma":

      {-@ LIQUID "--compilespec" @-}
      module Toy.A ( notThree, one, two) where
      ...
      
    2. We can add this "globally" (if that's really what we want), like this:

      cabal-version: 1.12
      name:           toy-package-a
        ..
        default-language: Haskell2010
        ghc-options: -fplugin=LiquidHaskell -fplugin-opt=LiquidHaskell:--compilespec
      

    Understanding LiquidHaskell Spec resolution strategies

    Let's revisit our A module. There are two different ways to annotate an existing Haskell module, and they are the following:

    1. (Recommended) Add the LH annotations directly inside the Haskell file (like in the example above). This has the advantage that any changes to the annotations trigger recompilation, and ensure the specs will never get stale and go out-of-sync. The disadvantage of this approach is that it can clutter quite a bit the target Module.
    2. Add the specifications as a separate companion .spec file to be placed alongside the Haskell one. To rehash the example above, we could have also added a new Toy/A.spec file living in the same folder of our A.hs file, with a content like this:
      module spec Toy.A where
    
      one :: {v:Int | v = 1 }
      assume notThree :: {v : Nat | v != 3 }
      two :: Nat
      

    This has the advantage of being more compartmentalised, but it's also a weakness as it might not be immediately obvious that a Haskell module has associated refinements.

    Providing specifications for existing packages

    If you have control over the package or project you would like to annotate with LH refinements, all is well. But what about packages you don't own or maintain? Typically, one solution would be to convince the project's maintainers to get on board and to add LH annotations to the code themselves, but this might not be so easy, for a number of reasons:

    • The package you are trying to "refine" is not maintained anymore, or the maintainer is very difficult to reach;
    • The package is fairly important in the Haskell ecosystem and making changes to it might not be so easy, especially for packages which come as part of a GHC installation (think base, for example).

    The designed workflow in these cases is to create a brand new package (that we can call an "assumptions" package), which would contain the required LH annotations. This is what we have done for things like vector and parallel, for example, by providing liquid-vector and liquid-parallel.

    There are some guidelines to drive this process:

    1. Typically you want to clearly identify this package as part of the LH ecosystem by using an appropriate prefix for your package name, something like liquid-foo where foo is the original package you are adding annotations for;
    2. If you want to have Liquid Haskell load the specs automatically when finding an import of a module A.B.C, put the specs in a module named A.B.C_LHAssumptions.
    3. You need to abide to a set of PVP rules, like tracking the version of the upstream package first and in case of changes to either the LH language or the specs in the mirror package, bump the last two digits of the version scheme, in a format like this:
    liquid-<package-name>-A.B.C.D.X.Y

    Where A.B.C.D would be used to track the upstream package version and X.Y would enumerate the versions of this mirror package. Bumping X would signify there was a breaking change in the LH language that required a new release of this plugin, whereas bumping Y would mean something changed in the specs provided as part of this assumptions package (e.g. more refinements were added, bugs were fixed etc).