是否有可能对haskell类型变量设置不等式约束？

Question

是否有可能对函数的类型变量设置不等式约束,foo :: (a ~ b) => a -> b如GHC类型族文档中那样,除了不等式而不是相等？

我意识到可能没有直接的方法来做到这一点(因为ghc文档没有列出任何我的知识),但如果根据所有异国情调的类型,这在某种程度上是不可能的,我会感到困惑 - 我已经接触过了.

Answer 1

首先,请记住,不同的类型变量在其范围内已经是不可统一的 - 例如,如果你有\x y -> x,给它类型签名a -> b -> c将产生一个关于无法匹配刚性类型变量的错误.因此,这仅适用于调用该函数的任何内容,从而阻止它以一种使两种类型相等的方式使用其他简单的多态函数.它会像这样工作,我假设:

const' :: (a ~/~ b) => a -> b -> a
const' x _ = x

foo :: Bool
foo = const' True False -- this would be a type error

我个人怀疑这真的很有用 - 类型变量的独立性已经阻止泛型函数崩溃到一些微不足道的事情,知道两种类型是不相等的,实际上并没有让你做任何有趣的事情(不像相等,它让你在两者之间强制执行)类型),这样的事情是声明而不是条件意味着你不能用它来区分等于/不等于某种专业化技术的一部分.

所以,如果你想要一些特定的用途,我建议尝试不同的方法.

另一方面,如果你只是想玩荒谬的类型hackery ...

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}

-- The following code is my own hacked modifications to Oleg's original TypeEq. Note
-- that his TypeCast class is no longer needed, being basically equivalent to ~.

data Yes = Yes deriving (Show)
data No = No deriving (Show)

class (TypeEq x y No) => (:/~) x y
instance (TypeEq x y No) => (:/~) x y

class (TypeEq' () x y b) => TypeEq x y b where
    typeEq :: x -> y -> b
    maybeCast :: x -> Maybe y

instance (TypeEq' () x y b) => TypeEq x y b where
    typeEq x y = typeEq' () x y
    maybeCast x = maybeCast' () x

class TypeEq' q x y b | q x y -> b where
    typeEq' :: q -> x -> y -> b
    maybeCast' :: q -> x -> Maybe y

instance (b ~ Yes) => TypeEq' () x x b where
    typeEq' () _ _ = Yes
    maybeCast' _ x = Just x

instance (b ~ No) => TypeEq' q x y b where
    typeEq' _ _ _ = No
    maybeCast' _ _ = Nothing

const' :: (a :/~ b) => a -> b -> a
const' x _ = x

嗯,这太令人难以置信了.但是工作:

> const' True ()
True
> const' True False

<interactive>:0:1:
    Couldn't match type `No' with `Yes'
    (...)

Answer 2

来自GHC 7.8.1.封闭式家庭可用.解决方案更加简单:

data True
data False

type family TypeEqF a b where
  TypeEqF a a = True
  TypeEqF a b = False

type TypeNeq a b = TypeEqF a b ~ False