Proposal: Using GHC Annotations

[ranjitjhala]

[bit of a brain dump]

As various people have noted (e.g. @kosmikus, @wkunkel, others?) and the old issues with .spec files and vector and bytestring etc. a major hassle with LH is that we can't save and import specifications across packages.

In general, of course, the import story has been problematic for a while.

Requirements

• REQ Write specs inside the modules inside package lib
• REQ Make those specs available to modules inside package client

As a concrete example,

• lib = https://hackage.haskell.org/package/proof-combinators
• client = someone who wants to use proof-combinators.

Right now, you can import proof-combinators but you don't get the refinements which defeats the purpose.

Proposal: GHC Annotations

I think that instead of (only) using the LH comments we should use GHC Annotations

Easy Part

The easy (?) part is moving specs like:

{-@ incr :: x:Nat -> {v:Int | v = x + 1} @-}

to something like

{-# module ANN  "incr :: x:Nat -> {v:Int | v = x + 1}" #-}

and to then slurp in these annotations (using the current parser etc.) (Issue Name resolution across packages? Hopefully ok...)

Difficult Part

The difficult part is dealing with specs that are generated by LH, i.e. the stuff dealt with {load/save}LiftedSpec. These include things like:

• reflect,
• measure, and perhaps the strengthened
• data?

The challenge here is that we need to run LH to actually generate and save the annotations in the compiled interface.

Solution

1. Extend the spec-parsing stuff to read in annotations saved in modules.

2. Write a core-plugin that reads annotations like {-# ANN module "reflect incr" #-} and generates new annotations, e.g. containing the reflected spec.

TODO List

This is going to be a big chunk of work.

• [] Factor out front-end stuff? (e.g. we can't make LH a dependency for vector & bytestring)

Have one approach where zero LH dependencies

• No Lifting vector etc., specs are just the stuff in the ANN and that's it, so no reflect.
• Yes Lifting proof-combinators where there is reflect and so on.

(Comments most welcome!)

[gridaphobe]

1. You can annotate individual values and types, instead of sticking every annotation on the module. This is actually important because IIRC you can only have one ANN per type per value/module/etc. But it also makes Bare a bit easier since there's less name resolution to deal with.

2. You can't annotate local binders, but that's actually fine since the specs don't need to be exported. So we could use regular LH comments for non-exported specs.

3. I didn't realize this, but https://downloads.haskell.org/%7Eghc/master/users-guide/extending_ghc.html#annotating-values suggests that you can embed quasiquoters inside annotations, so this might also be an opportunity to resurrect the quasiquoter stuff michael did a while back.

[ranjitjhala]

Eric,

thanks! (Also for your super blog post which I’ve been using to learn how annotations work!!!)

It turns out you can have multiple annotations per module (I checked and it works :)) so that’s an easy thing but yes we could attach them to binders or datatypes too... but yes it could make name resolution easier. Let me give it a whirl...

On Fri, Apr 20, 2018 at 1:46 PM Eric Seidel notifications@github.com wrote:

1.

You can annotate individual values and types, instead of sticking every annotation on the module. This is actually important because IIRC you can only have one ANN per type per value/module/etc. But it also makes Bare a bit easier since there's less name resolution to deal with. 2.

You can't annotate local binders, but that's actually fine since the specs don't need to be exported. So we could use regular LH comments for non-exported specs. 3.

I didn't realize this, but https://downloads.haskell.org/%7Eghc/master/users-guide/extending_ghc.html#annotating-values suggests that you can embed quasiquoters inside annotations, so this might also be an opportunity to resurrect the quasiquoter stuff michael did a while back.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1305#issuecomment-383217689, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOHLNlNXLz-7E5UBlzVgkBPdl7JkDks5tqkkXgaJpZM4TeBkh .

[gridaphobe]

I wrote a blog post about GHC annotations? I don't remember that :)

On Fri, Apr 20, 2018, at 16:53, Ranjit Jhala wrote:

Eric,

thanks! (Also for your super blog post which I’ve been using to learn how annotations work!!!)

It turns out you can have multiple annotations per module (I checked and it works :)) so that’s an easy thing but yes we could attach them to binders or datatypes too... but yes it could make name resolution easier. Let me give it a whirl...

On Fri, Apr 20, 2018 at 1:46 PM Eric Seidel notifications@github.com wrote:

1.

You can annotate individual values and types, instead of sticking every annotation on the module. This is actually important because IIRC you can only have one ANN per type per value/module/etc. But it also makes Bare a bit easier since there's less name resolution to deal with. 2.

You can't annotate local binders, but that's actually fine since the specs don't need to be exported. So we could use regular LH comments for non-exported specs. 3.

I didn't realize this, but https://downloads.haskell.org/%7Eghc/master/users-guide/extending_ghc.html#annotating-values suggests that you can embed quasiquoters inside annotations, so this might also be an opportunity to resurrect the quasiquoter stuff michael did a while back.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1305#issuecomment-383217689, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOHLNlNXLz-7E5UBlzVgkBPdl7JkDks5tqkkXgaJpZM4TeBkh .

-- You are receiving this because you commented. Reply to this email directly or view it on GitHub: https://github.com/ucsd-progsys/liquidhaskell/issues/1305#issuecomment-383219384

[jprider63]

Are annotations available across module/packages? I've seen some documentation that implies they aren't (although this might be out of date).

Instead of storing a String in the annotation, is it possible for a LH compiler plugin to save its internal representation of the refinement in the annotation? It looks like the internal representation would just need to implement Typeable and Data. For example, after type checking, the LH compiler plugin might add the following annotation:

{-# ANN incr LHInternalRefinementTypeForincr ... #-}

One concern I have is that library creators could write their own annotations (that are wrong) and downstream users would have incorrect/unsafe refinements. Does GHC tell you the source of an annotation (from the source code or from a plugin)? If not, I suppose a compiler plugin could first check if LH annotations exist and throw an error if they do (although a malicious library writer could not run LH at all).

It seems like compiler plugins can't modify syntax, but I've been thinking about how LH syntax could be improved. Here are a few options that might be an improvement.

liquid incr :: x:Nat -> {v:Int | v = x + 1}

$liquid incr :: x:Nat -> {v:Int | v = x + 1}

[liquid| incr :: x:Nat -> {v:Int | v = x + 1} |]

[ranjitjhala]

Yes I believe they are — my summer project was going to be to move all the LH stuff into annotations to allow inter package imports... (still traveling but hope to get to this soon)

The tricky bit has been that somehow GHCs “Binary” class is different than the usual “Binary” class; IIRC the former is what you need for annotations (if we want to store the LH representation) but maybe you’re right that we now just need Typable and Data.

I like your suggestions for syntax! Note that the third kind, with the quasiquotes is actually already available — Grep for ‘[lq|’ in tests/pos for some examples.

On Thu, Jun 21, 2018 at 7:49 PM JP notifications@github.com wrote:

Are annotations available across module/packages? I've seen some documentation https://ghc.haskell.org/trac/ghc/wiki/Plugins/Annotations#OtherConsiderations that implies they aren't (although this might be out of date).

Instead of storing a String in the annotation, is it possible for a LH compiler plugin to save its internal representation of the refinement in the annotation? It looks like https://downloads.haskell.org/%7Eghc/master/users-guide/extending_ghc.html#annotating-values the internal representation would just need to implement Typeable and Data. For example, after type checking, the LH compiler plugin might add the following annotation:

{-# ANN incr LHInternalRefinementTypeForincr ... #-}

One concern I have is that library creators could write their own annotations (that are wrong) and downstream users would have incorrect/unsafe refinements. Does GHC tell you the source of an annotation (from the source code or from a plugin)? If not, I suppose a compiler plugin could first check if LH annotations exist and throw an error if they do (although a malicious library writer could not run LH at all).

It seems like compiler plugins can't modify syntax, but I've been thinking about how LH syntax could be improved. Here are a few options that might be an improvement.

liquid incr :: x:Nat -> {v:Int | v = x + 1}

$liquid incr :: x:Nat -> {v:Int | v = x + 1}

[liquid| incr :: x:Nat -> {v:Int | v = x + 1} |]

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

[jprider63]

Could you expand on how you plan to move LH into annotations? Is there a repository or branch I can look at? I'm interested in this and maybe can find some time to contribute. Does it make sense to split into three separate packages? Packages for liquidhaskell-core, the liquid executable, and a liquidhaskell GHC plugin.

Interesting. Maybe this has to do with GHC's stages. I'd have to play around with it.

Good to know about the quasiquotes!

[ranjitjhala]

Adding this link since I also want to use core-plugins

https://ghc.haskell.org/trac/ghc/ticket/14476#ticket

http://eric.seidel.io/posts/abusing-compiler-plugins/

https://ghc.haskell.org/trac/ghc/ticket/10506#no1

[ranjitjhala]

Copying @jprider63 comments from the above thread:

If we make a compiler plugin/extension, this is the workflow I was thinking about:

    GHC does an initial parse.
    GHC passes LH the AST. LH parses the refinements, inserts the GHC annotations, and sends GHC back an updated AST.
    GHC does normal type checking, transitions to core, etc.
    LH does refinement type checking. In addition, it can send GHC back information like if there are dead code paths, rewriting rules for proven optimizations, etc.

The GHC annotations would need to be standardized across GHC/base versions.

[ranjitjhala]

@jprider63 -- you may be right, it could be that annotations are, in fact, not available across modules and packages, in which case we will have to stick with the .bspec approach :(

[ranjitjhala]

Hooray! thanks to @nomeata for jogging my memory about this thread on loading annotations from interface files (of other modules) -- am assuming this will also work across packages..

https://mail.haskell.org/pipermail/glasgow-haskell-users/2018-April/026727.html

[nomeata]

For inspection-testing, I don't let the user write the ANN, but provide a top-level splice that does that for him. Nicer syntax, and I can do stuff (parsing, sanity checking, creating multiple annotations). Strongly recommend that.

More details on that approach in the self-contained appendix of http://arxiv.org/abs/1803.07130

[alanz]

FYI @wz1000 is doing a GSOC project around getting GHC to save extra information for later (IDE) processing.

So it might be possible to request that some of the ANN information go in there too.

[ranjitjhala]

@nomeata thanks again for pointing out this link about source-plugins!

https://github.com/ghc-proposals/ghc-proposals/pull/107

Do you know if this is already available to play with (couldn't quite tell the status from that thread?)

[nomeata]

It got merged into master: https://github.com/ghc/ghc/commit/c2783ccf545faabd21a234a4dfc569cd856082b9 so you should be able to play with it if you use GHC HEAD, e.g. from https://launchpad.net/~hvr/+archive/ubuntu/ghc. It will be part of GHC-8.6.

[facundominguez]

@ranjitjhala what is the status of this proposal? Has it been addressed by now? IIUC, since LH is a GHC plugin the specs are saved in annotations.

[ranjitjhala]

Yes, this is super old and subsumed by the plugin I believe.

On Mon, Apr 24, 2023 at 12:19 PM Facundo Domínguez @.***> wrote:

@ranjitjhala https://urldefense.com/v3/__https://github.com/ranjitjhala__;!!Mih3wA!EK4UZCw2mW4x-rDQhgv4Vz5ewyyKxazyLD-2Byh-kWbdSXez12xQCiSbW7l8GuqWqULYDuSDm7QdjRd6JGhExrSs$ what is the status of this proposal? Has it been addressed by now? IIUC, since LH is a GHC plugin the specs are saved in annotations.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1305*issuecomment-1520702211__;Iw!!Mih3wA!EK4UZCw2mW4x-rDQhgv4Vz5ewyyKxazyLD-2Byh-kWbdSXez12xQCiSbW7l8GuqWqULYDuSDm7QdjRd6JMdux8xp$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OGM4ZENPWTTGXF43RTXC3G23ANCNFSM4E3YDEQQ__;!!Mih3wA!EK4UZCw2mW4x-rDQhgv4Vz5ewyyKxazyLD-2Byh-kWbdSXez12xQCiSbW7l8GuqWqULYDuSDm7QdjRd6JPmqjHmE$ . You are receiving this because you were mentioned.Message ID: @.***>

--

• Ranjit.