haskell - “惯用的” haskell 型不等式

Question

(从上一个问题编辑，我认为下面的代码不起作用)

我希望实现一个 haskell 函数 f，它有一个限制，即它的 2 个参数不得具有相同的类型。我使用了以下代码:

{-# 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 = ()

现在函数 g 只接受 a 和 b 如果它们具有不同的类型。这是在 haskell 中编码类型不等式的“惯用”方式吗？如果没有的话，它有什么问题？

Answer 1

与 new features添加到 GHC 后，您将能够编写:

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-}

type family Equal (a :: k) (b :: k) :: Bool
type instance where
   Equal a a = True
   Equal a b = False