¿Es posible colocar restricciones de desigualdad en las variables de tipo haskell?

Question

¿Es posible colocar una restricción de desigualdad en las variables tipo de una función, à la foo :: (a ~ b) => a -> b como en GHC type family docs, excepto la desigualdad en lugar de la igualdad?

Me doy cuenta de que posiblemente no haya una manera directa de hacerlo (ya que ghc docs no enumera ninguno que yo sepa), pero estaría casi perplejo si esto no fuera de alguna manera posible a la luz de todo el exótico tipo-fu al que he estado expuesto.

Answer 1

Primero, tenga en cuenta que las distintas variables de tipo ya no son unifilables dentro de su alcance; por ejemplo, si tiene \x y -> x, dándole el tipo de firma a -> b -> c producirá un error acerca de no poder hacer coincidir las variables de tipo rígidas. De modo que esto solo se aplicaría a cualquier cosa que llame a la función, evitando que use una función polimórfica que de otro modo sería sencilla de manera que dos tipos sean iguales. Que funcionaría algo así, supongo:

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

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

Personalmente dudo que esto sería realmente útil - la independencia de las variables de tipo ya impide funciones genéricas se colapse a algo trivial, sabiendo dos tipos son desiguales no De hecho, te permite hacer algo interesante (a diferencia de la igualdad, que te permite coaccionar entre los dos tipos), y ser declarativo en lugar de condicional significa que no podrías usarlo para distinguir entre igual/desigual como parte de algún tipo de técnica de especialización .

Por lo tanto, si tiene en mente un uso específico en donde desea esto, le sugiero que pruebe un enfoque diferente.

Por otro lado, si lo que desea es jugar con ridícula tipo 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 

Bueno, eso fue increíblemente tonta. Funciona, sin embargo:

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

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

Answer 2

De GHC 7.8.1. closed type families are available. La solución es mucho más simple con ellos:

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