Release agda2hs 1.3

[jespercockx]

It seems like we're long overdue for a new release (as indicated by the comment by @HeinrichApfelmus in #361 (comment)_).

One thing that might be worth doing is to investigate some lower/upper bounds on the dependencies (see e.g. #347 and #350 (comment)).

[jespercockx]

I've uploaded a release candidate to https://hackage.haskell.org/package/agda2hs-1.3/candidate

It would be great if people could give it a test run (perhaps @omelkonian @HeinrichApfelmus @anka-213). If there are no complaints I'll do a proper release next week.

[HeinrichApfelmus]

It would be great if people could give it a test run

Do you have a git commit (hash) that this release corresponds to?

I need to test the combination of agda2hs executable and agda2hs.agda-lib Agda library. If I understand correctly, only the executable is released on Hackage? 🤔 I'm asking for a git commit, because that would allow me to get the combination as presented in a specific flake.nix.

[jespercockx]

It should correspond to 770f209

[jespercockx]

If I understand correctly, only the executable is released on Hackage?

I think that's the case, indeed. I'm not sure if there's an easy way to release the library also on Hackage, do you think it's worth investigating or is it fine to just distribute it via github?

[HeinrichApfelmus]

do you think it's worth investigating or is it fine to just distribute it via github?

Distribution via Github, specifically the flake.nix works for me.

For a "proper" release that is accessible to a larger audience than just me, I think that investing time into creating release artifacts is unavoidable. I suppose that

• adding the library to the data-files: in agda2hs.cabal
• having the executable agda2hs use the bundled library by default, with a command-line option to instead use the traditional (if clumsy) AGDA_LIB way of specifying package dependencies.

would do the trick.

More generally, in order to make agda2hs "the missing proof assistant for Haskell", there is probably no way around integrating with .cabal.

[jespercockx]

I can definitely add the library to the data-files field. However, I'm not sure if I understand how the second point would work. I don't think it would be a good idea to let agda2hs silently override what's in the user's configuration in their libraries file or in the agda-lib file of their project.

Perhaps an alternative would be to provide a simple executable that sets up a new agda2hs project that automatically includes the agda2hs library that was installed through Cabal?

[omelkonian]

It would be great if people could give it a test run

I installed locally (using cabal) and everything works fine, including using the agda2hs executable interactively in Emacs.

[HeinrichApfelmus]

I don't think it would be a good idea to let agda2hs silently override what's in the user's configuration in their libraries file or in the agda-lib file of their project.

Fair enough, I agree. Though, since agda2hs is not agda, doing that does not necessarily count as "silent".

Perhaps an alternative would be to provide a simple executable that sets up a new agda2hs project that automatically includes the agda2hs library that was installed through Cabal?

The main difficulty is to bring the agda2hs library in scope — only cabal install knows where it is going to install the data-files.

But the agda2hs will be told about the location, so the simplest solution may be to add a command to agda2hs that print outs the location of the library?

I personally don't like generated project templates, it's not modular enough for my taste. I would use it to find the location of the library, and then delete the rest of the generated project. 😅

[jespercockx]

But the agda2hs will be told about the location, so the simplest solution may be to add a command to agda2hs that print outs the location of the library?

That also seems a lot more feasible, so I'm all in favor.

[HeinrichApfelmus]

In order to test out agda2hs-1.3, I have attempted to update the codebase cardano-wallet-agda to use the new version.

However, I ran into an unexpected issue:

I have a type PairMap consisting of two Data.Map and an invariant that they both contain the same data, albeit in different order. Specifically,

record PairMap (a b v : Set) {{orda : Ord a}} {{ordb : Ord b}} : Set where
  field
    mab : Map a (Map b v)
    mba : Map b (Map a v)

    @0 invariant-equal
      : ∀ (x : a) (y : b)
      → lookup2 x y mab ≡ lookup2 y x mba

In order to formulate the invariant, I needed to constrain the type parameters a and b to have Ord instances, otherwise I cannot use the lookup2 function.

However, agda2hs version 1.3 now gives me an error message when compiling:

…/lib/customer-deposit-wallet-pure/agda/Haskell/Data/Maps/PairMap.agda:400,8-15
Constraint in type parameter not supported: (orda : Ord a)

How to proceed?

I have tried moving the instance arguments to the definition of invariant-equal, but then I get the following error when trying to check a proof:

No instance of type Monad _m_2920 was found in scope.
- iMonadMaybe was ruled out because
  /Users/hgz/Documents/MeineDokumente/Programmierung/Haskell/Work/cardano-wallet-agda/lib/customer-deposit-wallet-pure/agda/Haskell/Data/Maps/PairMap.agda:425,15-60
  Cannot instantiate the metavariable _2870 to solution ordb
  since it contains the variable ordb
  which is not in scope of the metavariable
  when checking that the inferred type of an application
    (iMonadMaybe Monad.>>= Map.lookup y Map.empty)
    (λ v₁ → Map.lookup x v₁)
    ≡ (iMonadMaybe Monad.>>= Nothing) (λ v₁ → Map.lookup x v₁)
  matches the expected type
    (iMonadMaybe Monad.>>= Map.lookup y Map.empty) (Map.lookup x) ≡
    (_r_2921 Monad.>>= Nothing) (Map.lookup x)

[jespercockx]

@HeinrichApfelmus The instance constraints Ord a and Ord b are not supposed to show up in the generated Haskell code, are they? In other words, did you really want to write the following Haskell type?

data (Ord a, Ord b) => PairMap a b v = PairMap { mab :: Map a (Map b v)); mba :: (Map b (Map a v)) }

Note that this is only valid with the deprecated -XDatatypeContexts flag (see https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/datatype_contexts.html), and currently not supported by agda2hs.

In previous versions of agda2hs, the constraints on the datatype would instead be dropped, even though they did not have an erasure annotation. If you want to restore this old behavior, all you have to do is to add the erasure annotations:

record PairMap (a b v : Set) {{@0 orda : Ord a}} {{@0 ordb : Ord b}} : Set where ...

[HeinrichApfelmus]

The instance constraints Ord a and Ord b are not supposed to show up in the generated Haskell code, are they?
[…] If you want to restore this old behavior, all you have to do is to add the erasure annotations:

Thank you, the erasure annotations are exactly what I need, indeed. 🙏

The use case is worth keeping in mind: Even though the computational parts of the data type do not depend on the type class, the (erased) invariants can only be expressed with the type class constraints.

[HeinrichApfelmus]

I have another issue: The following module

module Test where

open import Haskell.Prelude

test : Integer
test = fromMaybe 0 (Just 12)

{-# COMPILE AGDA2HS test #-}

is transpiled to

module Test where

test :: Integer
test = fromMaybe 0 (Just 12)

but this module does not compile — it's missing a line

import Data.Maybe (fromMaybe)

In other words, the function fromMaybe happens to not be a part of the Haskell Prelude.

[HeinrichApfelmus]

I also have an issue where a type class is transpiled as an ordinary argument. 🤔

Specifically, consider the following definition:

Byron = ⊤

postulate
  IsEra : Set → Set
  instance
    iIsEraByron : IsEra Byron

The intention is that the class IsEra is defined in a Haskell module, and imported via a postulate. It's essentially a singleton class.

In agda2hs-1.2, the definition

-- adga2hs-1.2
utxoFromTxOutputs : ∀{era} → {{IsEra era}} → Read.Tx era → UTxO
utxoFromTxOutputs = utxoFromEraTx

was happily transpiled to

-- adga2hs-1.3
utxoFromTxOutputs :: IsEra era => Tx era -> UTxO
utxoFromTxOutputs = utxoFromEraTx

However, in agda2hs-1.3, this definition is transpiled to

utxoFromTxOutputs :: IsEra era -> Tx era -> UTxO
utxoFromTxOutputs x = utxoFromEraTx x

which the Haskell compiler will not accept, because IsEra is a type class, not a data type.

EDIT: It looks like defining IsEra as a data type does not change the transpilation output.

[flupe]

The use case is worth keeping in mind: Even though the computational parts of the data type do not depend on the type class, the (erased) invariants can only be expressed with the type class constraints.

Indeed, it's actually a design pattern that shows up in the very first example in the documentation!

data BST (a : Set) {{@0 _ : Ord a}} (@0 lower upper : a) : Set where
  Leaf : (@0 pf : lower ≤ upper) → BST a lower upper
  Node : (x : a) (l : BST a lower x) (r : BST a x upper) → BST a lower upper

In other words, the function fromMaybe happens to not be a part of the Haskell Prelude.

Good catch, related issue to #245.

I also have an issue where a type class is transpiled as an ordinary argument.

Also a good catch! Since #284 we do check if the type of the instance argument is compiled to a class or not, and if not it is added as a regular argument. Maybe we should then add a specific compile pragma for postulated type formers that says "this is actually a Haskell class". Will open an issue for that.

[HeinrichApfelmus]

Maybe we should then add a specific compile pragma for postulated type formers that says "this is actually a Haskell class". Will open an issue for that.

Yes, please. This issue is currently preventing me from upgrading my codebase to agda2hs-1.3. 😅

[flupe]

Wait, now that I think about it we already have the following pragma:

{-# COMPILE AGDA2HS IsEra existing-class #-}

used extensively in the prelude to avoid compiling the records.
So it definitely works on records, could you please check if this also works in your codebase for postulated typeclasses?

[HeinrichApfelmus]

So it definitely works on records, could you please check if this also works in your codebase for postulated typeclasses?

Unfortunately, it does not appear to work on postulate. 🤔 Fortunately, converting my singleton type class to a record is worth the duplication, so at least this issue is not blocking me.

[HeinrichApfelmus]

One last thing that I noticed:

I have two definitions

member
    : ∀ {time} {{_ : Ord time}}
    → time → RollbackWindow time → Bool
member time w = (finality w <= time) && (time <= tip w)

prune
    : ∀ {time} {{_ : Ord time}}
    → time → RollbackWindow time → Maybe (RollbackWindow time)
prune newFinality w =
  if member newFinality w
    then (λ {{cond}} → Just (record
      { tip = tip w
      ; finality = newFinality
      ; invariant = projr (prop-&&-⋀ cond)
      }))
    else Nothing

in my codebase. Strangely, the definition of prune is transpiled to

prune newFinality w =
    if finality w <= newFinality && newFinality <= tip w
        then Just (RollbackWindowC newFinality (tip w))
        else Nothing

instead of

prune newFinality w =
    if member newFinality w
        then Just (RollbackWindowC newFinality (tip w))
        else Nothing

In other words, the application of member is inlined in the transpilation output. 😲 This is fine from a correctness perspective, but unfortunately undesirable as far as transpilation goes, where we would like to preserve the original code as much as possible. Inlining a top-level definition is certainly something one would not want to do in transpilation.

[flupe]

Unfortunately, it does not appear to work on postulate.

Right, the culprit here seems to be this line:

agda2hs/src/Agda2Hs/Compile/Utils.hs

Line 170 in 0412c42

Right Defn{defName = r, theDef = Record{}} ->

Where we require Records for class candidates. I think it should be fine to allow Axioms too specifically for ExistingClass, provided we check somewhere that the postulate is indeed a good class type former.

One last thing that I noticed: [...]

Could you show the compile pragmas you used for prune and member? I find it surprising that member would be treated as inline, though it wouldn't be the first time. Do you think you could find a minimal standalone example?

[jespercockx]

Could you show the compile pragmas you used for prune and member? I find it surprising that member would be treated as inline, though it wouldn't be the first time. Do you think you could find a minimal standalone example?

Assuming that you didn't use a {-# COMPILE AGDA2HS member inline #-} pragma, the other potential culprit could be that you have the --auto-inline flag enabled or an {-# INLINE member #-} pragma.

[HeinrichApfelmus]

I didn't enable any pragmas.

The following appears to be a minimal test case:

./agda/Test.agda

{-# OPTIONS --erasure #-}

module Test where

open import Haskell.Prelude

{-----------------------------------------------------------------------------
    RollbackWindow
------------------------------------------------------------------------------}
record RollbackWindow (time : Set) : Set where
  constructor RollbackWindowC
  field
    finality : time
    tip : time

open RollbackWindow public

member
    : ∀ {time} {{_ : Ord time}}
    → time → RollbackWindow time → Bool
member time w = (finality w <= time) && (time <= tip w)

prune
    : ∀ {time} {{_ : Ord time}}
    → time → RollbackWindow time → Maybe (RollbackWindow time)
prune newFinality w =
  if member newFinality w
    then (λ {{cond}} → Just (record
      { tip = tip w
      ; finality = newFinality
      }))
    else Nothing

{-# COMPILE AGDA2HS RollbackWindow #-}
{-# COMPILE AGDA2HS member #-}
{-# COMPILE AGDA2HS prune #-}

./mylib.agda-lib

name: mylib
include: agda
depend:
  agda2hs
flags: -W noUnsupportedIndexedMatch --erasure

and then the invocation

$ agda2hs ./agda/Test.agda
Writing […]/agda/Test.hs

will produce the file

./agda/Test.hs

module Test where

data RollbackWindow time = RollbackWindowC{finality :: time,
                                           tip :: time}

member :: Ord time => time -> RollbackWindow time -> Bool
member time w = finality w <= time && time <= tip w

prune ::
        Ord time =>
        time -> RollbackWindow time -> Maybe (RollbackWindow time)
prune newFinality w
  = if finality w <= newFinality && newFinality <= tip w then
      Just (RollbackWindowC newFinality (tip w)) else Nothing

where the function member has been inlined in the definition of prune.

---

I noticed that removing the type variable time and using a concrete type Time = Integer everywhere will not produce the unexpected inlining.

[jespercockx]

Thank you for the report, I've investigated it and created a new issue in #376. For now, it can be worked around by disabling the projection-likeness optimization with the --no-projection-like flag.

[jespercockx]

I've updated the release candidate at https://hackage.haskell.org/package/agda2hs-1.3/candidate to correspond to the current master (afb5392). Since none of the remaining issues are critical, I plan to release this version tomorrow.

[HeinrichApfelmus]

Since none of the remaining issues are critical, I plan to release this version tomorrow.

Sounds good to me, thank you!

[jespercockx]

Agda2hs 1.3 has now been officially released! https://hackage.haskell.org/package/agda2hs-1.3