是否可以將不等式約束放在haskell類型變量上？

Question

是否可以在函數的類型變量上放置一個不等式約束，如中的la foo :: (a ~ b) => a -> b，除了不等式而不是等式之外呢？

我意識到有可能沒有直接的方法來做到這一點（因爲ghc文檔沒有列出任何我所知道的），但是如果根據所有這些不可能的話我會感到困惑我曾經接觸過的異國情調。

Answer 1

首先，請記住，不同類型的變量都已經在其範圍內的非unifiable - e.g，如果你有\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' 
    (...) 

Answer 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