search

agda / agda2hs

Compiling Agda code to readable Haskell
https://agda.github.io/agda2hs
MIT License
178 stars 37 forks source link

Add support for custom tuples #342

Closed jespercockx closed 4 months ago

jespercockx commented 4 months ago

This PR addresses the first point in #105 by adding support for compiling an Agda record type to a Haskell tuple. The feature is designed to be pretty flexible, so you can compile any record type and agda2hs will just take the (compiled) field types as the tuple components. It also allows defining unboxed tuples, which was previously not supported by agda2hs. However, there are no checks in place that the rules for unboxed tuples are followed, so it might generate invalid Haskell code if used improperly.

jespercockx commented 4 months ago

At the moment, tuple projections are not yet supported, and I'm not sure what's the best way to handle them. Here are two options:

  1. Generate projection functions for each projection of the record type (but then there will be many redundant copies of the projections if you have a lot of tuple types)
  2. Compile projections to built-in functions fst and snd (but what to do about tuples with more than 2 components?)

A hybrid (2 for binary tuples, 1 for everything else) is also possible in theory.

jespercockx commented 4 months ago

One more option I just thought of: take option 1 except that for binary tuple types, we check that the projections are called fst and snd, and we don't generate any code in that case.

EDIT: actually, record projections are not compiled unless they have their own COMPILE pragma, so perhaps there is nothing that really needs to be changed. If users want to define their own record types that use Haskell's built-in fst and snd projections, they can do so by declaring rewrite rules for the projections.