agda2hs
agda2hs copied to clipboard
Draft for add bindings for numeric typeclasses
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.