Is it possible to define a purely imaginary type in Haskell?-CodePudding

I'm going to use C as an example here to show what I'm after. For complex arithmetic it has both comlex and imaginary types:

https://en.cppreference.com/w/c/language/arithmetic_types#Imaginary_floating_types

These e.g. have the property that multiplying two numbers with type double imaginary will have the type double. This is almost but not quite the same as using complex numbers with the real part being 0.0 but not quite. Imaginary types don't explicitly store automatically eliminates unneeded computations with and storage of 0.0.

Additionally it prevents some problems with signed zeros. E.g. the computation (0.0 i*a)*(0.0 i*b) results in (-a*b-i*0.0) if a and b are negative and (-a*b i*0.0) otherwise. This can be surprising if the result is fed into a function with a branch cut. An imaginary type avoids this unwanted negation of the zero.

My question is can you define a similar imaginary type in Haskell (in addition to a complex type) and also the operations ( ), (-), (*), and (/) for it such that they behave like in C ? It seems that at least with the current definition of the Num and Fractional classes it's not possible because ( ), (-), (*), and (/) have a -> a -> a as type signature so e.g. multiplying two imaginary numbers can't have a different type as a result. Could one, however, a different definition for these classes so that what I'm after would be possible?

I'm not asking this for a practical purpose. I just want to better understand what Haskell's type system is capable of.

CodePudding user response：

Yes, of course you can define such a type. You just won't be able to use the Num interface for all its operations; but you are free to define whatever other functions you want with other types, perhaps even making them infix operators if desired.

Here's an example of a type that tracks at the type level whether it's imaginary or real, and supports addition and multiplication with an alternative name (subtraction and division don't require any new ideas not shown here):

{-# Language DataKinds #-}
{-# Language KindSignatures #-}
{-# Language TypeFamilies #-}

-- hide the Mindful data constructor
module Mindful (Mindful, real, iTimes, ( .), (*.), EqBool, KnownReality(isReal)) where

newtype Mindful (reality :: Bool) a = Mindful a deriving (Eq, Ord, Read, Show)

real :: a -> Mindful True a
real = Mindful

iTimes :: a -> Mindful False a
iTimes = Mindful

( .) :: Num a => Mindful r a -> Mindful r a -> Mindful r a
Mindful x  . Mindful y = Mindful (x   y)

(*.) :: (KnownReality r, KnownReality r', Num a)
     => Mindful r a -> Mindful r' a -> Mindful (EqBool r r') a
xm@(Mindful x) *. ym@(Mindful y) = Mindful (iSquared * x * y) where
    iSquared = if isReal xm || isReal ym then 1 else -1

type family EqBool a b where
    EqBool False False = True
    EqBool False True = False
    EqBool True False = False
    EqBool True True = True

class KnownReality r where isReal :: Mindful r a -> Bool
instance KnownReality False where isReal _ = False
instance KnownReality True where isReal _ = True

If you must have the names be exactly etc. for some reason (I do not recommend this, it will be a big pain), you could take a look at another answer of mine on controlling namespacing.