# An Introduction to Liquid Haskell

## TL;DR

Liquid Haskell is a tool that extends Haskell's type system with liquid types, enabling programmers to verify complex program properties efficiently through a tutorial that covers its principles, algorithms, and practical examples.

## Contribution

This paper provides an accessible introduction to Liquid Haskell, detailing its underlying liquid type technology, inference algorithms, and demonstrating its application with practical Haskell examples.

## Key findings

- Liquid Haskell can verify non-trivial properties of Haskell programs.
- The type inference algorithm effectively manages property proofs.
- Practical examples illustrate the system's capabilities.

## Abstract

This paper is a tutorial introducing the underlying technology and the use of the tool Liquid Haskell, a type-checker for the functional language Haskell that can help programmers to verify non-trivial properties of their programs with a low effort. The first sections introduce the technology of Liquid Types by explaining its principles and summarizing how its type inference algorithm manages to prove properties. The remaining sections present a selection of Haskell examples and show the kind of properties that can be proved with the system.