MuniHac 2020 Workshop: Andres Löh - Liquid Haskell

Liquid Haskell is an extension to Haskell that adds refinement types to the language, which are then checked via an external theorem prover such as z3. With refinement types, one can express many interesting properties of programs that are normally out of reach of Haskell's type system or only achievable via quite substantial encoding efforts and advanced type system constructs. On the other hand, the overhead for checking refinement types is often rather small, because the external solver is quite powerful.

Liquid Haskell used to be an external, standalone executable, but is now available as a GHC plugin, making it much more convenient to use.

In this tutorial, we'll discuss how refinement types work, give many examples of their use and learn how to work with Liquid Haskell productively.

Prerequisites
Good familiarity with Haskell basics is useful. However, no knowledge of type system language extensions or type-level programming is required.

Workshop Preparation

[flowname]

how will liquid-base compose with the upcoming linear-base?

[natasha_zuckerbaeck]

41:29 Does Liquid Haskell allow Quantifying now?

[amigalemming]

2:30:00 I do not see the termination issue here. 'repeat a' in a sense does not terminate, but it is a perfectly total Haskell function. If LiquidHaskell requires lists to become shorter in a recursive call then it would prohibit 'repeat'.
Imagine the recursive call to 'merge' would actually be a 'repeat'. Would this be ok? It would be, because the recursive branch already produced something and thus no infinite loop occurs. Thus I think, the initial definition of 'merge' should be accepted because in every branch there is either no recursion at all or the recursion only happens after producing new data.

[amigalemming]

1:41:00 exampleSorted: I assume that with the given definition of SortedList the validity check requires quadratic runtime?