Better support for wrapping Haskell modules via postulate

[HeinrichApfelmus]

Problem statement

The mission statement of Adga2hs is to carve out a sublanguage of Agda that translates directly to Haskell, so that we can prove properties about Haskell-in-Agda programs in Agda. This is highly useful for producing high assurance Haskell code. Personally, I think of Agda2hs as "the missing proof assistant for Haskell".

I particularly enjoy that Agda2hs allows me to develop proofs about Haskell programs in an incremental fashion: I can write and prove selected parts of my program in Haskell-in-Agda, export them to Haskell, and use the result together with existing Haskell code that was only tested, not proven.

However, I feel that this incremental approach would become even more powerful if Agda2hs better supported the import of Haskell code. Here, I don't mean a syntactic import of Haskell code (that would be amenable to proof), but an import of Haskell functions and "tested" properties via Agda's postulate mechanism. Let me call this "wrapping a Haskell module".

Put differently, at the moment, Agda2hs implements a translation from .agda to .hs files where the .agda file is the "source of truth". I would like to see a translation from .agda to .hs where the .hs file acts as a "source of truth".

Proposed solution: COMPILE … IMPORT pragma

Agda2hs has made a design decision to translate .agda files to .hs files. In particular, it does not attempt to parse Haskell files. This design works particularly well for using Agda2hs as a preprocessor for Haskell. In order to explore this point in the design space properly, we need to take it to its logical extreme before changing it. Hence, I'll leave the Haskell to the Haskell compiler.

Consider the following module, which is legal Adga2hs today:

module Haskell.Cardano.Crypto.Wallet where

{-# FOREIGN AGDA2HS
{-# LANGUAGE UnicodeSyntax #-}
import qualified Cardano.Crypto.Wallet as CC
#-}

postulate
  XPub : Set  -- plaintext public key
  XPrv : Set  -- plaintext private key

  toXPub : XPrv → XPub

{-# FOREIGN AGDA2HS
type XPub = CC.XPub
type XPrv = CC.XPrv

toXPub :: XPrv → XPub
toXPub = CC.toXPub
#-}

(This is a real world example.) This module defines two data types XPub and XPrv and a function toXPub. However, instead of giving an actual definition, this module simply postulates the identifiers and emits Haskell code that imports the identifiers from the Haskell module Cardano.Crypto.Wallet.

This module does what I want: I can use the Haskell Cardano.Crypto.Wallet in my Haskell-in-Agda code. By postulating properties, I can also do proofs (while assuming that the properties hold).

However, this module would benefit from native support in Agda2hs. In particular, the following would be an improved version:

module Haskell.Cardano.Crypto.Wallet where

postulate
  XPub : Set  -- plaintext public key
  XPrv : Set  -- plaintext private key

  toXPub : XPrv → XPub

{-# COMPILE AGDA2HS XPub IMPORT #-}
{-# COMPILE AGDA2HS XPrv IMPORT #-}
{-# COMPILE AGDA2HS toXPub IMPORT #-}

Here, the intention is that the new compiler pragma

{-# COMPILE AGDA2HS toXPub IMPORT #-}

compiles to a type signature and equation of identifiers

toXPub :: XPrv -> XPub
toXPub = Cardano.Crypto.Wallet.toXPub

For types such as XPub and XPrv, instead of defining a type synonym, the identifiers would be added to the export list.

The name of the imported Haskell module is obtained by stripping the Haskell prefix from the Agda module name. For the purpose of disambiguation, the generated module keeps the Haskell prefix.

This level of native support in Agda2hs has the following advantages over the version using FOREIGN AGDA2HS:

• It avoids duplication — I no longer have to write down the type of toXPub twice.
• The Haskell compiler will type-check that the imported Haskell identifier has the same type as the postulate. This is the most important advantage.
• Type synonyms are almost, but not fully interchangeable with the original types — there is ambiguity when importing from different modules. This is a minor thing.

It's worth repeating that the decision to only emit Haskell code, but to never parse Haskell code is preserved.

What do you think?

[jespercockx]

Could you explain how this would be different from the existing support for declaring agda2hs rewrite rules in a separate file? (see https://agda.github.io/agda2hs/features.html#rewrite-rules-and-prelude-imports) I think the idea here is solid, but I'd prefer to avoid reinventing the wheel.

[HeinrichApfelmus]

Could you explain how this would be different from the existing support for declaring agda2hs rewrite rules in a separate file?

Sure.

First, the intended use case is different. According to the documentation, Rewrite rules and Prelude imports, are "particularly useful if you have a project depending on a large library which is not agda2hs-compatible (e.g the standard library)." That's not the intended use case here — instead of making Agda data types that have concrete definitions, e.g. ℕ, interoperable in the transpiled Haskell (which may have different concrete definitions), I want to import identifiers from Haskell that have no a-priori definition in Agda.

But a difference of use cases does not yet imply that the feature is not suitable for the other use case as well. However, I believe that the following differences are good reasons to add a {-# COMPILE … IMPORT #-}-like mechanism:

• Static type check — The rewrite rules do not include a direct check whether the rewritten identifier and the Agda identifier have the same types; we only get a scope check and follow-up errors in the event of a type mismatch.

• Syntax, modularity — Rewrite rules are listed in a separate configuration file, not in a valid Agda module. The one-to-one relation between an .agda module and its corresponding .hs module is lost.

• Syntax, duplication — I would have to write

    from: "Haskell.Data.Map.lookup"
    to: "lookup"
    importing: "Data.Map"

  for each identifier — forcing me to duplicate the module name. (I have to duplicate the identifier when using {-# COMPILE … #-}, but not the module name.)

Now that you mention it, there is some overlap, though. 🤔 Specifically, consider the following example:

postulate
    empty   : Map k a
    insert  : k → a → Map k a → Map k a

singleton : k → a → Map k a
singleton = λ k x → insert k x empty

The functions empty and insert are postulates and to be imported from Haskell. However, singleton is defined in Agda here, even though a definition exists in the Data.Map Haskell module. In this case, we want to rewrite — the reason that I have added a definition for singleton instead of postulate-ing it is that this definition simplifies proofs; it's not meant to be the actual definition at runtime. But even in this case, I believe that the type check and modularity are worth adding a pragma-based import/rewrite mechanism as opposed to a configuration-file one.