Skip to content

Latest commit

 

History

History
106 lines (72 loc) · 2.52 KB

README.md

File metadata and controls

106 lines (72 loc) · 2.52 KB
Raw

LiquidHaskell Tutorial

TODO: UPDATE the website with the new code

NOTE The PDF/HTML are sometimes not up-to-date with the latest LiquidHaskell release. Please clone the github repository and run locally for best results.

How to Do The Tutorial

LH is available as a GHC plugin from version 0.8.10.

Thus, the best way to do this tutorial is to

Step 1 Clone this repository,

$ git clone https://github.com/ucsd-progsys/liquidhaskell-tutorial.git

Step 2: Iteratively edit-compile until it builds without any liquid type errors

$ cabal v2-build

or

$ stack build --fast --file-watch

The above workflow will let you use whatever Haskell tooling you use for your favorite editor, to automatically display LH errors as well.

Contents

Part I: Refinement Types

  1. Introduction
  2. Logic & SMT
  3. Refinement Types
  4. Polymorphism
  5. Refined Datatypes

Part II: Measures

  1. Boolean Measures
  2. Numeric Measures
  3. Set Measures

Part III : Case Studies

  1. Case Study: Okasaki's Lazy Queues
  2. Case Study: Associative Maps
  3. Case Study: Pointers & Bytes
  4. Case Study: AVL Trees

Update

$ git pull origin master
$ git submodule update --recursive

Building

Deploy on Github

$ cp package.yaml.pandoc package.yaml
$ mkdir _site dist
$ stack install pandoc
$ make html
$ make pdf
$ cp dist/pbook.pdf _site/book.pdf
$ git add _site
$ git commit -a -m "updating GH-PAGES"
$ git push --force-with-lease origin HEAD:gh-pages

Prerequisites

  • Install LaTeX dependencies:
    • Texlive
    • texlive-latex-extra
    • texlive-fonts-extra

Producing .pdf Book

$ make pdf
$ evince dist/pbook.pdf

Solutions to Exercises

Solutions are in separate private repo

TODO

A work list of TODO items can be found in the bug tracker

Feedback and Gotchas

Editing feedback and various gotchas can be found in feedback.md