Можно ли установить ограничения неравенства на переменные типа haskell?

Можно ли установить ограничение неравенства на typevariables для функции, la foo :: (a ~ b) => a -> b, как в GHC тип docs, за исключением неравенство, а не равенство?

Я понимаю, что, возможно, нет прямого способа сделать это (поскольку документы ghc не перечисляют никаких моих знаний), но я был бы почти озадачен, если бы это не было возможно каким-либо образом в свете всех экзотический тип-фу, к которому я был подвергнут.

Ответы

Ответ 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 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'
    (...)