search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.2k stars 139 forks source link

Consider developing a standard library of theorems #1277

Open rosekunkel opened 6 years ago

rosekunkel commented 6 years ago

I think Liquid Haskell would be more attractive as a theorem prover if there were a library of theorems available already, so that users didn't have to e.g. prove that list append is associative. I could build this myself, but I think it would be better if there was an officially-supported standard library.

This does have several complications, however. If we want to prove results about Prelude, we need some way to reflect the functions it defines, or we need to write our own Prelude and tell everyone to compile with -XNoImplicitPrelude.

Also, from a library design perspective, it would be nice to be able to reflect class methods (see #1196), so we could write something like

class VerifiedMonoid a where
  {-@ reflect vmempty @-}
  vmempty :: a

  {-@ reflect vmappend @-}
  vmappend :: a -> a -> a

  {-@ vmLeftId :: x:a -> {vmappend vmempty x = x} @-}
  vmLeftId :: a -> Proof

  {-@ vmRightId :: x:a -> {vmappend x vmempty = x} @-}
  vmRightId :: a -> Proof

  {-@ vmAssoc :: x:a -> y:a -> z:a -> {vmappend (vmappend x y) z = vmappend x (vmappend y z)} @-}
  vmAssoc :: a -> a -> a -> Proof

and provide a unified interface to the proof that any monoid is associative.

atondwal commented 6 years ago

Hmm, wonder if we should take more inspiration from agda (haskell-y) or Isabelle (classical) re: what to include....

If we want to prove results about Prelude, we need some way to reflect the functions it defines, or we need to write our own Prelude and tell everyone to compile with -XNoImplicitPrelude.

Actually, LH does currently support library specs written outside the hs file (but IIRC only those that are shipped with LH?). For example, this is the spec for Data.Maybe:

https://github.com/ucsd-progsys/liquidhaskell/blob/563cccbd69dfd4b0c4bdfcad5ac73205917b99a4/include/Data/Maybe.spec

reflect class methods

Coming soon! See @RyanGlScott 's fork.

rosekunkel commented 6 years ago

@atondwal I assume those spec files can't actually use reflection, though — we'd have to print out whatever spec reflecting generates and paste it into the spec file. That might be usable if it were automated, but we'll probably end up with weird errors if the LH version, library version, and Prelude version don't all match.

ranjitjhala commented 6 years ago

Good point! As @wkunkell .spec approach really isn’t feasible.

I wonder if there is some way to get access to code from the prelude...

On Sat, Mar 31, 2018 at 5:29 PM Anish Tondwalkar notifications@github.com wrote:

Hmm, wonder if we should take more inspiration from agda (haskell-y) or Isabelle (classical) re: what to include....

If we want to prove results about Prelude, we need some way to reflect the functions it defines, or we need to write our own Prelude and tell everyone to compile with -XNoImplicitPrelude.

Actually, LH does currently support library specs written outside the hs file (but IIRC only those that are shipped with LH?). For example, this is the spec for Data.Maybe:

https://github.com/ucsd-progsys/liquidhaskell/blob/563cccbd69dfd4b0c4bdfcad5ac73205917b99a4/include/Data/Maybe.spec

reflect class methods

Coming soon! See @RyanGlScott https://github.com/RyanGlScott 's fork.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1277#issuecomment-377731900, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOIOwtyxc1OYSkFz4TqQk40AgkdL6ks5tkBdpgaJpZM4TCpo- .

facundominguez commented 5 months ago

Probably resolving #2126 will make this more approachable.