是否可以对 haskell 类型变量进行不等式约束？答案

【问题标题】：Is it possible to place inequality constraints on haskell type variables?是否可以对 haskell 类型变量进行不等式约束？
【发布时间】：2011-08-04 09:30:00
【问题描述】：

是否可以在函数的类型变量上放置不等式约束，就像GHC type family docs 中的foo :: (a ~ b) => a -> b，除了不等式而不是等式？

我意识到可能没有直接的方法可以做到这一点（因为据我所知，ghc 文档没有列出任何内容），但鉴于所有我接触过的异国情调。

【问题讨论】：

您认为不等式约束对哪些用例有用？
具体来说，我正在尝试对商品数量进行建模，即带有标签的数字，例如，使您能够表达拥有 10 个苹果和 2 个梨的概念，并在需要时引发类型错误添加梨和苹果。这本身就很简单。然而，当我试图用另一种商品来定义一种商品的价格时，我的不足之处是，例如每个梨 2 个苹果。当然，只有在出售的商品类型与购买的商品类型不同时，价格才有意义。（至少在我的脑海中）。所以，出于好奇，我只是想知道是否真的可以表达这一点:)
我的怀疑是，虽然它可能傻，但价格是明确定义的（显然是 1 比 1），因此可能不值得尝试对不同的类型提出静态要求。
我有一个用例:) 我正在尝试对两种交替类型[a,b,a,b,a] 的列表进行建模，其中最后一个元素的类型是静态已知的。这允许在第一个和最后一个元素具有相同类型的列表上编写类型安全的 last 函数，因为编译器可以排除 Nil 情况为具有不兼容的类型，仅当类型为 a和b 不同.

标签： haskell type-inference type-systems

【解决方案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

我个人怀疑这是否真的有用——类型变量的独立性已经防止泛型函数崩溃为微不足道的东西，知道两种类型不相等实际上并不能让你做任何有趣的事情（不像平等，它可以让你强制在这两种类型之间），并且这些东西是声明性的而不是条件性的，这意味着您不能使用它来区分相等/不等作为某种专业化技术的一部分。

所以，如果你有一些特定的用途，我建议你尝试不同的方法。

另一方面，如果你只是想玩可笑的类型黑客......

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

【讨论】：

感谢您提供了一个非常详尽的答案-正是满足我好奇心的那种东西:-) ..很抱歉没有激发我的问题-我在评论中详细阐述了我的想法问题:-)
读者注意：类函数（typeEq、maybeCast等）与示例无关，可以忽略/删除。
你确定这有效吗？虽然const' True () 似乎工作正常，但const' 2 () 和const' 'a' 8 正在返回错误。我正在使用 ghc 7.4.1
@tohava：它确实适用于我当时使用的任何 GHC 版本，可能是 7.0 版本，像这种在较新的 GHC 上打破的废话一点也不会让我感到惊讶。也就是说，它肯定会在数字文字等多态参数上失败。请改用const' (2 :: Int) ()。这就是为什么这种愚蠢的技巧不值得努力的（众多）原因之一。

【解决方案2】：

从 GHC 7.8.1 开始。 closed type families are available。使用它们的解决方案要简单得多：

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

【讨论】：

我正在尝试使用这种技术来消除重叠类型类实例的歧义，但似乎无法让它发挥作用。见stackoverflow.com/questions/38549174/…

【解决方案3】：

现在可以使用来自 Data.Type.Equality（或来自单例库）的 == 和 DataKinds 扩展：

  foo :: (a == b) ~ 'False => a -> b

【讨论】：

【解决方案4】：

改进 Boldizsar 的答案，这本身就是对已接受答案的改进：

{-# language DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}

import Data.Kind (Constraint)
import GHC.TypeLits (TypeError, ErrorMessage(..))

data Foo = Foo

data Bar = Bar

notBar :: Neq Bar a => a -> ()
notBar _ = ()

type family Neq a b :: Constraint where
  Neq a a = TypeError
    ( 'Text "Expected a type that wasn't "
    ':<>: 'ShowType a
    ':<>: 'Text "!"
    )
  Neq _ _ = ()

*Main> notBar Foo
()
*Main> notBar Bar

<interactive>:12:1: error:
    • Expected a type that wasn't Bar!
    • In the expression: notBar Bar
      In an equation for ‘it’: it = notBar Bar

这个的类型错误很好，而且可读性很好。

【讨论】：