search

agda / agda2hs

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

Add support for Data.Dynamic #207

Open jespercockx opened 1 year ago

jespercockx commented 1 year ago

Haskell's Data.Dynamic library (https://hackage.haskell.org/package/base-prelude-1.6.1.1/docs/BasePrelude.html#v:Dynamic) allows dynamic typing in Haskell for all values of Typeable types. It could be possible to add support for a COMPILE AGDA2HS DYNAMIC pragma that compiles an Agda type to Dynamic in Haskell, as long as all the possible concrete types this value could compute to are instances of Typeable.

The main use case for this that I see would be to more easily support compiling existing Agda functions that do not necessarily fall into the fragment accepted by agda2hs. In particular, types that are defined through large elimination, i.e. functions into Set, could be compiled into Dynamic which would enable compiling functions that use them. But there might be other use cases too.

jespercockx commented 1 year ago

I just realize that this would not really work for the use case that I described, unless all the possible types returned by the function are also compiled to Dynamic. However, it would still be interesting to have support for Data.Dynamic in general, so I'm keeping this issue open for that.

jespercockx commented 4 months ago

I just happened to think about this feature again. One possibility would be to have the Agda version of Dynamic take an erased parameter of type Set , so it would still be possible to reason about the static type of Dynamic values on the Agda side. In particular this erased type could make free use of type-level functions.