interface FromNat a where
fromNat : Nat -> aPréludeChargé par défaut — aucun
import nécessaire.FromNat — numeric literal overloading
Synopsis
interface FromNat a wheredata Rational = Rat Int Intinterface FromDecimal a whereinterface Additive a whereinterface Multiplicative a whereinterface Additive a => AdditiveGroup a whereinterface Abs a whereinterface Additive a => Multiplicative a => Semiring a where {}interface Semiring a => EuclideanDiv a whereinterface Semiring a => AdditiveGroup a => Ring a where {}interface Ring a => CommutativeRing a where {}interface CommutativeRing a => EuclideanDiv a => EuclideanRing a where {}interface Ring a => DivisionRing a wherepi : Doubleinterface Floating a where
Rational — exact rational numbers
data Rational = Rat Int IntFromDecimal — decimal literal overloading
interface FromDecimal a where
fromDecimal : Rational -> aLets decimal literals (3.14, 0.5, ...) work for any type with a FromDecimal instance — Double, Rational, and your own types.
Additive — addition and zero
interface Additive a where
(+) : a -> a -> a
zero : aA type with addition and a zero element.
Multiplicative — multiplication and one
interface Multiplicative a where
(*) : a -> a -> a
one : aA type with multiplication and a one element.
AdditiveGroup — subtraction and negation
interface Additive a => AdditiveGroup a where
negate : a -> a
(-) : a -> a -> aSubtraction and negation. Only for types that support negative values (Int, Double). Nat does not have an AdditiveGroup — use checkedSub or monus.
interface Abs a where
abs : a -> aAbsolute value: drops the sign. A CLASS, so each signed type provides its own (a user type can too). abs (-5) = 5, abs 5 = 5. (Nat is always non-negative, so it is not an instance.)
Semiring — addition and multiplication with distribution
interface Additive a => Multiplicative a => Semiring a where {}A type with both addition and multiplication, where multiplication distributes over addition. A marker interface (no new methods).
EuclideanDiv — integer division and modulo
interface Semiring a => EuclideanDiv a where
div : a -> a -> a
mod : a -> a -> aInteger division with Euclidean semantics. On Semiring (not Ring), so Nat has div/mod too — the same div/mod as Int. The remainder is always non-negative. div (-7) 3 = -3, mod (-7) 3 = 2 (not -1 as in C). Law: div x y * y + mod x y = x
Ring — a semiring with subtraction
interface Semiring a => AdditiveGroup a => Ring a where {}A ring: a semiring that is also an additive group. Marker interface. Nat is NOT a Ring (it has no negate).
CommutativeRing — commutative multiplication
interface Ring a => CommutativeRing a where {}A ring whose multiplication commutes (a b == b a). Marker interface.
EuclideanRing — a Euclidean domain
interface CommutativeRing a => EuclideanDiv a => EuclideanRing a where {}A commutative ring with Euclidean division. Marker interface (= CommutativeRing + EuclideanDiv). Nat is not one (no negate), though it still has EuclideanDiv. Note: Double is intentionally NOT EuclideanDiv/EuclideanRing/Field yet — whether Double's div/mod should be truncated or the trivial field structure (div = /, mod = zero) is still open.
DivisionRing — reciprocal and real division
interface Ring a => DivisionRing a where
recip : a -> a
(/) : a -> a -> aReal division and reciprocal. Extends Ring. For continuous types (Double). Not for integer division.
Floating-point functions on Double
pi : Doubleπ, to double precision.
interface Floating a where
sqrt : a -> a
exp : a -> a
ln : a -> a
sin : a -> a
cos : a -> a
tan : a -> aFloating collects the transcendental FUNCTIONS. Double is the only instance so far; the CLASS makes them generic so other floating types (a future arbitrary-precision float, …) can join. ln is undefined for non-positive inputs; sin/cos/tan take radians.
Instances : Double