agda
Add support for ornamented datatypes and functions
When defining a fancy version of an existing datatype (e.g. All as a fancy version of List), it would be nice to be able to mark it as the ornamented version of that datatype in agda2hs, so they can both be compiled to the same Haskell datatype. The condition here would be that compiling the ornamented version should result in the exact same Haskell code as the base type (modulo naming of the type).
Similarly, we could allow marking functions (e.g. map on the All type) as an ornamented version of an existing function, and compile calls to it to calls to that existing function. Again, this would require both versions of the function to compile down to the precise same Haskell code (modulo naming of the function).
I think my comment on the Agda issue here could be useful in this context.
I also think this would obviate the need for agda2hs' "boxed" pragma right? As you could just define types to compile to some simpler type and thus not need to stick to ornament-esque "boxed" types with data + proof in a sigma type.
You mean the unboxed pragma? I'm not sure if it would be subsumed by this feature: basically, this feature would allow you to drop constructor arguments and datatype indices, while unboxed allows you to drop the constructor itself (if there is a single constructor with a single non-erased argument). But perhaps it's possible to design a feature that encompasses both.
I'm not sure if the example of All over List is actually an example of an ornament according to the definition that I found & could comprehend in the literature, so I think a first question to ask would be if we want to support ornaments, or rather a more general or just different relationship between datatypes.
Ah, I thought these would also be ornaments but perhaps I was mistaken. I've thought about this problem more since creating this issue and I agree that a sensible implementation of this would basically be to allow compiling one datatype to another one if their compiled Haskell versions are identical (up to renaming of the type), and similarly for functions.
Is it correct that the underlying goal would be to:
- reduce the proliferation of Haskell definitions,
- optimize (e.g. compile certain functions to the identity)?
I think that's one way to frame it, yes. The other way would be to see it as making it much easier to define Agda datatypes and functions with different invariants and pre/postconditions without creating new Haskell-side code. The hope would be that once you have this ability you would be more likely to introduce these new types in the first place (as opposed to taking an extrinsic verification approach).