git.iko.soy/Idris-dev
on cd58dfb help sign in
Idris-dev/libs/base/Data/Complex.idr
75 lines 2.0 kB history raw
1{-
2 (c) 2012 Copyright Mekeor Melire
3-}
6module Data.Complex
8%access public export
10------------------------------ Rectangular form
12infix 6 :+
13data Complex a = (:+) a a
15realPart : Complex a -> a
16realPart (r:+i) = r
18imagPart : Complex a -> a
19imagPart (r:+i) = i
21implementation Eq a => Eq (Complex a) where
22 (==) a b = realPart a == realPart b && imagPart a == imagPart b
24implementation Show a => Show (Complex a) where
25 showPrec d (r :+ i) = showParens (d >= plus_i) $ showPrec plus_i r ++ " :+ " ++ showPrec plus_i i
26 where plus_i : Prec
27 plus_i = User 6
31------------------------------ Polarform
33mkPolar : Double -> Double -> Complex Double
34mkPolar radius angle = radius * cos angle :+ radius * sin angle
36cis : Double -> Complex Double
37cis angle = cos angle :+ sin angle
39magnitude : Complex Double -> Double
40magnitude (r:+i) = sqrt (r*r+i*i)
42phase : Complex Double -> Double
43phase (x:+y) = atan2 y x
46------------------------------ Conjugate
48conjugate : Neg a => Complex a -> Complex a
49conjugate (r:+i) = (r :+ (0-i))
51implementation Functor Complex where
52 map f (r :+ i) = f r :+ f i
54-- We can do "implementation Neg a => Num (Complex a)" because
55-- we don't need "abs", only (-)
56implementation Neg a => Num (Complex a) where
57 (+) (a:+b) (c:+d) = ((a+c):+(b+d))
58 (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))
59 fromInteger x = (fromInteger x:+0)
61implementation Neg a => Neg (Complex a) where
62 negate = map negate
63 (-) (a:+b) (c:+d) = ((a-c):+(b-d))
65-- Specific to Double because `abs` needs `magnitude` which needs `sqrt` which
66-- operates on Double.
67implementation Abs (Complex Double) where
68 abs (a:+b) = (magnitude (a:+b):+0)
70implementation (Neg a, Fractional a) => Fractional (Complex a) where
71 (/) (a:+b) (c:+d) = let
72 real = (a*c+b*d)/(c*c+d*d)
73 imag = (b*c-a*d)/(c*c+d*d)
74 in
75 (real:+imag)