Draft for add bindings for numeric typeclasses

[ndcroos]

See #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.

[jespercockx]

I think there's some confusion here: Real, Integral, etc in Haskell are not types but type classes, so they should be modeled as such in agda2hs. See for example how the Num typeclass is implemented in https://github.com/agda/agda2hs/blob/master/lib/Haskell/Prim/Num.agda as a record type with all the methods (as well as invariants, if necessary). So for example, since Real just has a single method toRational, its definition should be something like

record Real (a : Set) : Set where
  field
    toRational : a -> Rational
open Real ⦃...⦄ public

{-# COMPILE AGDA2HS Real existing-class #-}

However, this first requires the addition of the Rational type, which we don't yet have in agda2hs either. So perhaps a first goal would be to implement the Rational module for agda2hs.

[ndcroos]

Thanks for your helpful feedback, @jespercockx.

I am trying to define Rational:

{-# OPTIONS --no-auto-inline #-}

module Haskell.Prim.Rational where

open import Haskell.Prim.Integer

--------------------------------------------------
-- Definition

-- | Rational numbers, with numerator and denominator of some 'Integral' type.
data Ratio (a : Set) : Set where
  :% : a → a → Ratio a
  numerator : Ratio a → a
  denominator : Ratio a → a

-- | Arbitrary-precision rational numbers, represented as a ratio of
-- two 'Integer' values.  A rational number may be constructed using
-- the '%' operator.
Rational : Set
Rational = Ratio Integer

But I get the error:

C:\Users\Documenten\agda2hs\lib\Haskell\Prim\Rational.agda:18,18-25
Not in scope:
  Integer
  at C:\Users\Documenten\agda2hs\lib\Haskell\Prim\Rational.agda:18,18-25
    (did you mean
       'Haskell.Prim.Integer.eqInteger' or
       'Haskell.Prim.Integer.ltInteger' or
       'eqInteger' or
       'ltInteger'?)
when scope checking Integer

It seems like the type checker expects that there should be a Integer datatype, which is missing in Prim/Integer.agda.

Another problem I encountered is that I don't know how to define instances of Integral. For example:

  iIntegralInt : Integral Int
  iIntegralInt._quot_ n d = ?
  iIntegralInt._rem_ n d = ?
  iIntegralInt._div_ n d = ?
  iIntegralInt.quotRem n d = ?
  iIntegralInt.toInteger x = toInteger x

This seems to require arithmetic operations that are lacking in Int.

[jespercockx]

It seems like Integer is exported by Haskell.Prim (and transitively by Haskell.Prelude) but not by Haskell.Prim.Integer. You could just import Haskell.Prim, or you could add a re-export of the Integer to Haskell.Prim.Integer.

Also note that Ratio should be defined as a record type, and numerator and denominator should be fields, not constructors.

[jespercockx]

This seems to require arithmetic operations that are lacking in Int.

Quotient and remainder are defined in the standard library at https://github.com/agda/agda-stdlib/blob/d3c50376c14a20604940c5f6694a5bb2602d34a7/src/Data/Integer/Base.agda#L283-L294, so you could try to port the definitions from there to the agda2hs library.