CODEWITHSUNDEEP
haskelltypespolymorphism
schuelermine
schuelermine

Reputation: 2288

Can the type of (a == b) be derived to be polymorphic?

Since (==) :: Eq a => a -> a -> Bool, I'd expect

a == b :: Eq a => Bool
-- assuming a :: forall a. a
-- derived type

but (according to GHCi :t)

a == b :: Bool

Now of course, this requires TypeApplications, so it shouldn't be enabled by default, but is there a LANGUAGE option that enables this?

NoMonomorphismRestriction doesn't work.

EDIT: Since you may say, "well, GHC(i) already knows the type of a and b in any practical example", no, for example, you could have (5 == 5) :: (Num a, Eq a) => Bool.
EDIT: It seems a :: forall a. a isn't possible, so let's assume something like x = 5 :: Num a => a

EDIT: Explicitly declaring the type works, so the question is really "Can GHC infer this type to be polymorphic", so I'm looking for something like DeriveAmbiguousTypes.

Upvotes: 2

Views: 122

Answers (3)

K. A. Buhr
K. A. Buhr

Reputation: 50864

Note that if you're just asking if the expression 3 == 5 can be made polymorphic in the type of 3 and 5, the answer is yes. The signature must be given explicitly with the help of some language extensions, but the following definition is polymorphic:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module ThreeFive where

eq35 :: forall a . (Num a, Eq a) => Bool
eq35 = (3 :: a) == 5

Alternatively, you could use TypeApplications:

eq35' :: forall a . (Num a, Eq a) => Bool
eq35' = (==) @a 3 5

Now, GHCi reports the type of eq35 as Bool, but that's a lie, as you can see by adding the +v flag:

> :type eq35
eq35 :: Bool
> :type +v eq35
eq35 :: (Num a, Eq a) => Bool

or by proving it:

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

-- Holistic number are all equal
newtype Holistic = Holistic Int deriving (Num)
instance Eq Holistic where
  _ == _ = True

main = do print (eq35 @Int)
          print (eq35 @Holistic)

and running this will print False and True.

I don't see any sort of combination of language extensions that would allow GHC to automatically infer a more general type for 3 == 5 than True in the absence of explicit type signatures. Similarly, however polymorphic x and y might be, x == y will be either defaulted to a monomorphic type or rejected unless you use an explicit signature like the one above.

Upvotes: 1

dfeuer
dfeuer

Reputation: 48591

This is all about the type of (==):

(==) :: forall a. Eq a => a -> a -> Bool

(==) takes four arguments, in order:

  1. A type, a, of kind Type (AKA *),
  2. A dictionary of type Eq a,
  3. A value of type a.
  4. A value of type a.

As usual, partial application only works in order, and dictionary arguments cannot be passed explicitly. Furthermore, type arguments can only be introduced before they're used. So when you write a == b, this actually means

(==) @_ @{dict} a b

The type argument and dictionary argument are inferred, and you get a value of type Bool.

What you're after has a rather different type from (==):

numLitEq
  :: (forall a. (Num a, Eq a) => a)
  -> (forall b. (Num b, Eq b) => b)
  -> forall c. (Num c, Eq c) => Bool
numLitEq a b = (==) @c a b

You can't write exactly this, though, because there's no way to get the c type variable into scope. The best you can do is

numLitEq
  :: forall c.
     (forall a. (Num a, Eq a) => a)
  -> (forall b. (Num b, Eq b) => b)
  -> (Num c, Eq c) => Bool
numLitEq a b = (==) @c a b

which isn't any better than just using (==).

Upvotes: 4

leftaroundabout
leftaroundabout

Reputation: 120711

Actually this just works – in GHC-8.2 and 8.3 at least.

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Prelude> :set -XRank2Types -XUnicodeSyntax
Prelude> let x, y :: ∀ a . a; (x,y) = (undefined,undefined)
Prelude> :set -XAllowAmbiguousTypes 
Prelude> let p :: ∀ a . Eq a => Bool; p = x==y

Prelude> :set -XTypeApplications 

Prelude> p @Int
*** Exception: Prelude.undefined
CallStack (from HasCallStack):
  error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err
  undefined, called at <interactive>:3:36 in interactive:Ghci1

Prelude> p @(String -> Double)
<interactive>:11:1: error:
    • No instance for (Eq (String -> Double)) arising from a use of ‘p’
        (maybe you haven't applied a function to enough arguments?)
    • In the expression: p @(String -> Double)
      In an equation for ‘it’: it = p @(String -> Double)

Upvotes: 1

Related Questions