agda2hs icon indicating copy to clipboard operation
agda2hs copied to clipboard

Draft for add bindings for numeric typeclasses

Open ndcroos opened this issue 7 months ago • 4 comments

See https://github.com/agda/agda2hs/issues/262 cc @jespercockx

This is my first PR to agda2hs. I am also new to Agda in general. This draft is a way of showing what I currently have done.

I tried to follow the templates of other numeric types, but at the moment I don't know how to continue further. I'd like to receive comments on how to improve.

I looked at the following typeclasses in Haskell: https://hackage.haskell.org/package/planet-mitchell-0.0.0/docs/Numeric-Floating.html#t:Floating https://hackage.haskell.org/package/base-4.20.0.1/docs/Prelude.html#t:Fractional https://hackage.haskell.org/package/planet-mitchell-0.0.0/docs/Numeric-RealFrac.html#g:2 https://hackage.haskell.org/package/planet-mitchell-0.0.0/docs/Numeric-RealFloat.html#v:encodeFloat

I have trouble with defining the types for Real, Integral and Fractional. I also don't know how to specify a pair (e.g. (Int, Realfrac) ) as a return type of a function in Agda.

ndcroos avatar Jul 20 '24 14:07 ndcroos