Skip to content

avanov/liquid-haskell-parsing-demo

Repository files navigation

Liquid Haskell Example

This is a self-contained Liquid Haskell example.

nix-shell --run "make run"

Consider the function apiCallProvideRedundancy.

Imagine it's a part of "Core API" that needs to be safe and free from redundant case-analysis of input data. Liquid Haskell helps us to express types and filter values based on predicates that go beyond NonEmpty kinds of constructors. As soon as I declare that type Destinations is a list of at least two non-empty textual values, the compiler requires me to prove that the data I call apiCallProvideRedundancy with does satisfy that criteria of the firsrt argument. Hence the helper parsing functions have to exist at the boundaries of my API, and not somewhere inside apiCallProvideRedundancy.

About

A small demo of how Liquid Haskell and refinement types can aid API design

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published