on f88a377 help sign in
Idris-dev/libs/base/Data/Complex.idr
75 lines 1.9 kB history raw
1{-
2 (c) 2012 Copyright Mekeor Melire
3-}
6module Data.Complex
8------------------------------ Rectangular form
10infix 6 :+
11data Complex a = (:+) a a
13realPart : Complex a -> a
14realPart (r:+i) = r
16imagPart : Complex a -> a
17imagPart (r:+i) = i
19instance Eq a => Eq (Complex a) where
20 (==) a b = realPart a == realPart b && imagPart a == imagPart b
22instance Show a => Show (Complex a) where
23 showPrec d (r :+ i) = showParens (d >= plus_i) $ showPrec plus_i r ++ " :+ " ++ showPrec plus_i i
24 where plus_i : Prec
25 plus_i = User 6
28-- when we have a type class 'Fractional' (which contains Float and Double),
29-- we can do:
30{-
31instance Fractional a => Fractional (Complex a) where
32 (/) (a:+b) (c:+d) = let
33 real = (a*c+b*d)/(c*c+d*d)
34 imag = (b*c-a*d)/(c*c+d*d)
35 in
36 (real:+imag)
37-}
41------------------------------ Polarform
43mkPolar : Float -> Float -> Complex Float
44mkPolar radius angle = radius * cos angle :+ radius * sin angle
46cis : Float -> Complex Float
47cis angle = cos angle :+ sin angle
49magnitude : Complex Float -> Float
50magnitude (r:+i) = sqrt (r*r+i*i)
52phase : Complex Float -> Float
53phase (x:+y) = atan2 y x
56------------------------------ Conjugate
58conjugate : Neg a => Complex a -> Complex a
59conjugate (r:+i) = (r :+ (0-i))
61instance Functor Complex where
62 map f (r :+ i) = f r :+ f i
64-- We can't do "instance Num a => Num (Complex a)" because
65-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float
66instance Num (Complex Float) where
67 (+) (a:+b) (c:+d) = ((a+c):+(b+d))
68 (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))
69 fromInteger x = (fromInteger x:+0)
71instance Neg (Complex Float) where
72 negate = map negate
73 (-) (a:+b) (c:+d) = ((a-c):+(b-d))
74 abs (a:+b) = (magnitude (a:+b):+0)