haskelltypesghctype-equivalence

'idiomatic' Haskell type inequality


(edited from previous question where I thought code below doesn't work)

I wish to implement a haskell function f that has a restriction such that its 2 parameters must not have the same type. I have used the following code:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, FlexibleInstances, FlexibleContexts, TypeFamilies, IncoherentInstances #-}
data HTrue = HTrue
data HFalse = HFalse

class HEq x y b | x y -> b
instance (b ~ HTrue) => HEq x x b
instance (b ~ HFalse) => HEq x y b


g :: (HEq a b HFalse) => a -> b -> ()
g x y = ()

Now the function g only accepts a and b if they have different types. Is this the 'idiomiatic' way to code type inequality in haskell? If not, what are the problems with it?


Solution

  • With new features being added to GHC, you'll be able to write:

    {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-}
    
    type family Equal (a :: k) (b :: k) :: Bool
    type instance where
       Equal a a = True
       Equal a b = False