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?