module exports list

[jmchapman]

[UlfNorell]

The naive solution would be to always generate an export list and add all public definitions that we compiled to it. The problem is that you might have FOREIGN blocks with functions that you also want to export, or when you want to reexport things from other modules.

Possible solution:

{-# FOREIGN AGDA2HS export (foo, bar, module Bla) #-}

The question is whether we should populate the export list with public definitions we know about or require the user to be explicit about everything that should be exported. If the former we probably want a

{-# FOREIGN AGDA2HS export all #-}

to say that you don't want an export list.

[gallais]

Is there a use-case where you'd want to not export a function in Haskell but you'd be happy to export it in Agda? Otherwise using private blocks as a way to remove things from the export list seems sensible.

[jespercockx]

You might want to export a lemma about a function to other modules so it can be used for further proofs about that function.

EDIT: I realized these would anyway not be translated to Haskell, so never mind. Using private makes perfect sense.

[dxts]

"whether we should populate the export list with public definitions we know about"

Would this also include known definitions which are being re-exported from other modules?

[jespercockx]

Would this also include known definitions which are being re-exported from other modules?

Only if these are public on the Agda side, presumably.