7 ms·

Liquid Haskell: Haskell as a Theorem Prover [pdf]

199 points by kumaranvpl 10y ago

DanGarcia595 10y ago
I find this delightfully coincidental that the very moment I found this I was sitting in AI class as my professor stresses the usefulness of a good automated theorem prover.
- curiousgal 10y ago
  Offtopic but I absolutely love it when those "delightful coincidences" or synchronicities occur. Examples also include me learning about something right before someone else brings it up.
  - acomar 10y ago
    I do too. I suspect they're a form of confirmation bias, however, because it's not easy to remember that you heard about an idea or term you're unfamiliar with. On the other hand, something you've just recently heard or learned stands out: it reinforces the lesson you've just learned.
    - curiousgal 10y ago
      >something you've just recently heard or learned stands out Not only does it stand out, at times it seems to appear more frequent. I found out that was called the Baader-Meinhof Phenomenon.
    - ShaneWilton 10y ago
      You'd probably be interested in this article about the phenomenon: https://www.damninteresting.com/the-baader-meinhof-phenomenon/ https://www.damninteresting.com/the-baader-meinhof-phenomeno...
      - acomar 10y ago
        Thanks! This has me down a rabbit-hole because I'm now trying to find the name for a related concept: once you've learned a new idea/model, you start to notice how it applies to everything around you. I find this happening most often with algebraic ideas but the article you linked alludes to the fact that you're liable to notice this effect at play more in the days after reading about it. I want to call it overfitting but that's not quite right.
        marcoperaza 10y ago
        This is the Law of the Instrument: if all you have is a hammer, then everything looks like a nail.
        aninhumer 10y ago
        I don't think that's really the same meaning. Here it's more like, if you're given a hammer, you'll notice a lot of nails you can use more easily now.
    - deleted 10y ago
      [deleted]
    - transposed 10y ago
      Once you've learned a thing, or "studied it" much more, you are more swift in perceiving it, processing, and storing that encounter. Be it an idea, name, combination of low frequency words... Otherwise, many things go in one ear and out the other. What really gives me the goose bumps is if you're, say, listening to a recording of a lecture while looking out the window watching a leaf tumble through the wind - and then the professor uses a leaf blowing in the wind analogy. It's not something you do very frequently; watch and listen to two independent events.
  - pizza 10y ago
    https://en.wikipedia.org/wiki/Coincidence_detection_in_neurobiology https://en.wikipedia.org/wiki/Coincidence_detection_in_neuro...
- eveningcoffee 10y ago
  It would be interesting to know what were your professor arguments and what was suggested as a better solution.
- geooooooooobox 10y ago
  so why is it useful?
primodemus 10y ago
Talk by Niki Vazou, the author of the dissertation: https://www.youtube.com/watch?v=LEsEME7JwEE https://www.youtube.com/watch?v=LEsEME7JwEE
airesQ 10y ago
There is an interactive tutorial at [1]. I find this quite amazing. With refinement types one can say/prove things like: - This function only returns even numbers. - The input for this function is not just any vector, it must be an ordered vector. - It's possible to make compile time unit tests. Where we write a function that exercises the code, and returns True if the test succeeds. Then one adds a refinement type saying that the function must always evaluate to true. The theorem prover does the rest. [1] - http://ucsd-progsys.github.io/liquidhaskell-tutorial/02-logic.html#/examples-arithmetic http://ucsd-progsys.github.io/liquidhaskell-tutorial/02-logi...
- jeff_marshall 10y ago
  There have been quite a few systems that can handle proofs of the kinds of propositions you list above using various different logical frameworks, programming languages, and automatic and/or user-guided proof assistants. That said, it's no small feat to do a correct translation from the semantics of a full, modern, programming language into the semantics of a SMT solver (which appears to be the primary back-end for deciding propositions in this tool). I'll have to go read the actual dissertation to see how far that goes and whether any escape-hatches for user guidance exist (tactics, manual term manipulation, etc.). I haven't yet found a tool that doesn't allow extensive user guidance to be all that effective for proving things about code/systems that are interesting (to me).
bbcbasic 10y ago
Is this providing a similar purpose to say code contracts in .NET? Albeit I am sure this is more comprehensive.
- platz 10y ago
  liquid haskell (refinement types) is similar to F* https://www.fstar-lang.org/ https://www.fstar-lang.org/ which exports code to .Net (and OCaml) I think because Code Contracts are not utiling any form of Dependent Types (i.e. refinement types), there is only so much that it can statically check/enforce. Refinement Types can go much farther, and their whole utility is in static checks, not runtime checks/unit tests.
- nikivazou 10y ago
  It is like contract checking, but all the checks are done statically (at compile time) and automatically by the solver. Also, we allow the checks to only express things that the SMT solvers can decide fast (eg linear arithmetic). So, checking will definitely terminate and it will terminate fast.
alokedesai 10y ago
This is cool because it's in Haskell, but there are a bunch of great formal theorem provers, coq (https://coq.inria.fr/ https://coq.inria.fr/) being one of the most famous ones.
- namarkiv 10y ago
  I would like to emphasize that this gives you a theorem prover "inside" haskell, unlike coq/agda where you need to do program extraction. This means you can combine proofs and programs without a significant impact to the runtime performance.
bbcbasic 10y ago
The very first blogpost http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/ http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/0... gives a very nice jargon and maths-free introduction to this. You don't need to know Haskell to follow it really. The assert function shown in the post is really cool. Amazing how easy it is to define a function that will compile time check an assertion (e.g. something is not "null"). That's code contracts done in the 101 class.
xvilka 10y ago
What the difference with Agda? Why not it?
- nikivazou 10y ago
  Liquid Types use the SMT solver to automatically generate proofs, while in Agda the user needs to manually specify the proofs. Also, Agda is a verification specific language, while (Liquid) Haskell is a general purpose language, which means that with Liquid Haskell your verified code can use general language features, such as exceptions, diverging code, parallelism and all the Haskell optimized libraries.
  - xvilka 10y ago
    Thank you for your explanation and writing this. Added in my todo list to play with. I understand this one is the official repo: https://github.com/ucsd-progsys/liquidhaskell https://github.com/ucsd-progsys/liquidhaskell ?
- namarkiv 10y ago
  While you can write verified programs in agda, and use the MAlonzo FFI to extract haskell code, the generated code is very inefficient. On the other hand, this lets you write proofs in Haskell that coexist with your program, so there's little to no impact on runtime performance. Also, Agda is an implementation of Martin-Lof type theory, which is very, very different from what SMT is.
mkawa 10y ago
If you'd like to learn more about how the Liquid Types style of refinement types works under the covers, I invite you to read Pat Rondon's thesis: http://goto.ucsd.edu/~pmr/papers/rondon-liquid-types.pdf http://goto.ucsd.edu/~pmr/papers/rondon-liquid-types.pdf The UCSD Programming Systems lab has also applied refinement types to dynamic languages[1] and systems programming languages[2]. The MIT Computer Assisted Programming Group has similarly used liquid types-based techniques for program synthesis[3], while a group at Purdue has been working on maching learning of complex refinement types[4,5] that are difficult to state or infer using the liquid types techniques. [1] http://goto.ucsd.edu/~pvekris/docs/pldi16.pdf http://goto.ucsd.edu/~pvekris/docs/pldi16.pdf [2] http://goto.ucsd.edu/~rjhala/papers/low_level_liquid_types.pdf http://goto.ucsd.edu/~rjhala/papers/low_level_liquid_types.p... [3] http://people.csail.mit.edu/polikarn/publications/pldi16.pdf http://people.csail.mit.edu/polikarn/publications/pldi16.pdf [4] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/icfp_my_version.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... [5] https://www.cs.purdue.edu/homes/zhu103/pubs/pldipaper.pdf https://www.cs.purdue.edu/homes/zhu103/pubs/pldipaper.pdf

199 points by kumaranvpl 10y ago

I find this delightfully coincidental that the very moment I found this I was sitting in AI class as my professor stresses the usefulness of a good automated theorem prover.

curiousgal 10y ago
Offtopic but I absolutely love it when those "delightful coincidences" or synchronicities occur. Examples also include me learning about something right before someone else brings it up.
- acomar 10y ago
  I do too. I suspect they're a form of confirmation bias, however, because it's not easy to remember that you heard about an idea or term you're unfamiliar with. On the other hand, something you've just recently heard or learned stands out: it reinforces the lesson you've just learned.
  - curiousgal 10y ago
    >something you've just recently heard or learned stands out Not only does it stand out, at times it seems to appear more frequent. I found out that was called the Baader-Meinhof Phenomenon.
  - ShaneWilton 10y ago
    You'd probably be interested in this article about the phenomenon: https://www.damninteresting.com/the-baader-meinhof-phenomenon/ https://www.damninteresting.com/the-baader-meinhof-phenomeno...
    - acomar 10y ago
      Thanks! This has me down a rabbit-hole because I'm now trying to find the name for a related concept: once you've learned a new idea/model, you start to notice how it applies to everything around you. I find this happening most often with algebraic ideas but the article you linked alludes to the fact that you're liable to notice this effect at play more in the days after reading about it. I want to call it overfitting but that's not quite right.
      - marcoperaza 10y ago
        This is the Law of the Instrument: if all you have is a hammer, then everything looks like a nail.
        aninhumer 10y ago
        I don't think that's really the same meaning. Here it's more like, if you're given a hammer, you'll notice a lot of nails you can use more easily now.
  - deleted 10y ago
    [deleted]
  - transposed 10y ago
    Once you've learned a thing, or "studied it" much more, you are more swift in perceiving it, processing, and storing that encounter. Be it an idea, name, combination of low frequency words... Otherwise, many things go in one ear and out the other. What really gives me the goose bumps is if you're, say, listening to a recording of a lecture while looking out the window watching a leaf tumble through the wind - and then the professor uses a leaf blowing in the wind analogy. It's not something you do very frequently; watch and listen to two independent events.
- pizza 10y ago
  https://en.wikipedia.org/wiki/Coincidence_detection_in_neurobiology https://en.wikipedia.org/wiki/Coincidence_detection_in_neuro...
eveningcoffee 10y ago
It would be interesting to know what were your professor arguments and what was suggested as a better solution.
geooooooooobox 10y ago
so why is it useful?

primodemus 10y ago

Talk by Niki Vazou, the author of the dissertation: https://www.youtube.com/watch?v=LEsEME7JwEE https://www.youtube.com/watch?v=LEsEME7JwEE

airesQ 10y ago

There is an interactive tutorial at [1]. I find this quite amazing. With refinement types one can say/prove things like: - This function only returns even numbers. - The input for this function is not just any vector, it must be an ordered vector. - It's possible to make compile time unit tests. Where we write a function that exercises the code, and returns True if the test succeeds. Then one adds a refinement type saying that the function must always evaluate to true. The theorem prover does the rest. [1] - http://ucsd-progsys.github.io/liquidhaskell-tutorial/02-logic.html#/examples-arithmetic http://ucsd-progsys.github.io/liquidhaskell-tutorial/02-logi...

jeff_marshall 10y ago
There have been quite a few systems that can handle proofs of the kinds of propositions you list above using various different logical frameworks, programming languages, and automatic and/or user-guided proof assistants. That said, it's no small feat to do a correct translation from the semantics of a full, modern, programming language into the semantics of a SMT solver (which appears to be the primary back-end for deciding propositions in this tool). I'll have to go read the actual dissertation to see how far that goes and whether any escape-hatches for user guidance exist (tactics, manual term manipulation, etc.). I haven't yet found a tool that doesn't allow extensive user guidance to be all that effective for proving things about code/systems that are interesting (to me).

bbcbasic 10y ago

Is this providing a similar purpose to say code contracts in .NET? Albeit I am sure this is more comprehensive.

platz 10y ago
liquid haskell (refinement types) is similar to F* https://www.fstar-lang.org/ https://www.fstar-lang.org/ which exports code to .Net (and OCaml) I think because Code Contracts are not utiling any form of Dependent Types (i.e. refinement types), there is only so much that it can statically check/enforce. Refinement Types can go much farther, and their whole utility is in static checks, not runtime checks/unit tests.
nikivazou 10y ago
It is like contract checking, but all the checks are done statically (at compile time) and automatically by the solver. Also, we allow the checks to only express things that the SMT solvers can decide fast (eg linear arithmetic). So, checking will definitely terminate and it will terminate fast.

alokedesai 10y ago

This is cool because it's in Haskell, but there are a bunch of great formal theorem provers, coq (https://coq.inria.fr/ https://coq.inria.fr/) being one of the most famous ones.

namarkiv 10y ago
I would like to emphasize that this gives you a theorem prover "inside" haskell, unlike coq/agda where you need to do program extraction. This means you can combine proofs and programs without a significant impact to the runtime performance.

bbcbasic 10y ago

The very first blogpost http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/ http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/0... gives a very nice jargon and maths-free introduction to this. You don't need to know Haskell to follow it really. The assert function shown in the post is really cool. Amazing how easy it is to define a function that will compile time check an assertion (e.g. something is not "null"). That's code contracts done in the 101 class.

xvilka 10y ago

What the difference with Agda? Why not it?

nikivazou 10y ago
Liquid Types use the SMT solver to automatically generate proofs, while in Agda the user needs to manually specify the proofs. Also, Agda is a verification specific language, while (Liquid) Haskell is a general purpose language, which means that with Liquid Haskell your verified code can use general language features, such as exceptions, diverging code, parallelism and all the Haskell optimized libraries.
- xvilka 10y ago
  Thank you for your explanation and writing this. Added in my todo list to play with. I understand this one is the official repo: https://github.com/ucsd-progsys/liquidhaskell https://github.com/ucsd-progsys/liquidhaskell ?
namarkiv 10y ago
While you can write verified programs in agda, and use the MAlonzo FFI to extract haskell code, the generated code is very inefficient. On the other hand, this lets you write proofs in Haskell that coexist with your program, so there's little to no impact on runtime performance. Also, Agda is an implementation of Martin-Lof type theory, which is very, very different from what SMT is.

mkawa 10y ago

If you'd like to learn more about how the Liquid Types style of refinement types works under the covers, I invite you to read Pat Rondon's thesis: http://goto.ucsd.edu/~pmr/papers/rondon-liquid-types.pdf http://goto.ucsd.edu/~pmr/papers/rondon-liquid-types.pdf The UCSD Programming Systems lab has also applied refinement types to dynamic languages[1] and systems programming languages[2]. The MIT Computer Assisted Programming Group has similarly used liquid types-based techniques for program synthesis[3], while a group at Purdue has been working on maching learning of complex refinement types[4,5] that are difficult to state or infer using the liquid types techniques. [1] http://goto.ucsd.edu/~pvekris/docs/pldi16.pdf http://goto.ucsd.edu/~pvekris/docs/pldi16.pdf [2] http://goto.ucsd.edu/~rjhala/papers/low_level_liquid_types.pdf http://goto.ucsd.edu/~rjhala/papers/low_level_liquid_types.p... [3] http://people.csail.mit.edu/polikarn/publications/pldi16.pdf http://people.csail.mit.edu/polikarn/publications/pldi16.pdf [4] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/icfp_my_version.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/... [5] https://www.cs.purdue.edu/homes/zhu103/pubs/pldipaper.pdf https://www.cs.purdue.edu/homes/zhu103/pubs/pldipaper.pdf