'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?

回答1:

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

回答2:

This is how it is done in the HList library

{-# LANGUAGE FlexibleInstances, 
    MultiParamTypeClasses, 
    FunctionalDependencies, 
    UndecidableInstances ,
    IncoherentInstances
 #-}

data HTrue; data HFalse;

class TypeCast a b | a -> b
instance TypeCast a a

class TypeEq a b c | a b -> c
instance TypeEq x x HTrue
instance (TypeCast HFalse b) => TypeEq x y b
-- instance TypeEq x y HFalse -- would violate functional dependency

You can fully infer type equality now:

typeEq :: TypeEq a b c => a -> b -> c
typeEq _ _ = undefined

Note that typeEq 0 1 == HFalse since 0 :: Num a => a and 1 :: Num b => b.