在Haskell中只允许不同的“any”类型

Question

假设我们有一个带有签名的函数

foo :: a -> b -> Int

是否有可能实施一个约束来确保a和b是不同的？那就是

foo :: Int -> String -> Int -- ok
foo :: Int -> Int    -> Int -- not ok

这个问题的目的是了解更多关于Haskell的信息，并可能解决我面临的一个设计问题。如果a==b，我的特殊情况是没有意义的，所以我想在编译器级别禁止这样做。我可能会用一个完全不同的设计来解决这个问题，但这不仅仅是现在的重点--潘多拉盒子已经打开，我想知道类型级别上的等式约束是否可能。

Answer 1

这是阿图尔版本的一个即兴片段。它使用为trivial-constraints包开发的机制。

{-# LANGUAGE DataKinds, KindSignatures, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables, ExplicitNamespaces, TypeOperators, UndecidableSuperClasses, UndecidableInstances #-}


import Data.Type.Equality (type (==))
import GHC.TypeLits
import GHC.Exts (Any)

-- The Any constraint prevents malicious/ignorant
-- instantiation with no = undefined. The only
-- way to produce an instance of this class is in a local context
-- using something deeply unsafe like unsafeCoerce, magicDict, or unsafePerformIO.
class Any => Bottom where
  no :: a

-- Why not just put the `no` method in this class?
-- Because then `no` will need to be applied to the type argument `e`, which is
-- very annoying and unnecessary.
class (TypeError e, Bottom) => Oops e

class Foo a b (eq :: Bool) where
  foo' :: a -> b -> Int

foo :: forall a b. Foo a b (a == b) => a -> b -> Int
foo = foo' @a @b @(a == b)

instance Oops ('Text "NAUGHTY!") => Foo a b 'True where
  foo' = no

instance Foo a b 'False where
  foo' _ _ = 42