'idiomatic' Haskell type inequality

Question

(edited from previous question where I thought code below doesn't work)

I wish to implement a haskell function f that has a restriction such that its 2 parameters must not have the same type. I have used the following code:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, FlexibleInstances, FlexibleContexts, TypeFamilies, IncoherentInstances #-}
data HTrue = HTrue
data HFalse = HFalse

class HEq x y b | x y -> b
instance (b ~ HTrue) => HEq x x b
instance (b ~ HFalse) => HEq x y b


g :: (HEq a b HFalse) => a -> b -> ()
g x y = ()

Now the function g only accepts a and b if they have different types. Is this the 'idiomiatic' way to code type inequality in haskell? If not, what are the problems with it?

i think you are missing a `)` in your type declaration for `g`. Have you tried `g (2 :: Int) (3 :: Int)` ? — DiegoNolan, Jul 19 '13 at 15:26
Oops, you are right, I keep forgetting the ambiguity for integer literals. I just tried `g 'a' "b"` and it works. Are there any problems with the code that I wrote (I'm new to advanced haskell). — tohava, Jul 19 '13 at 15:29
You don't need `IncoherentInstances`. `OverlappingInstances` is enough. — is7s, Jul 19 '13 at 15:43
Just out of curiosity, what kind of problem needs that kind of restriction? — Ankur, Jul 19 '13 at 16:13
For now, no problem, I'm just curious regarding how well some C++ features translate to haskell. In C++ these kind of things can be more useful though, since they can be used to prevent implicit type cast, which haskell almost never does. — tohava, Jul 19 '13 at 16:19
Haskell actually *never* does a typecast. Caveat: I'm not sure if I know enough Haskell to say that's always true, but I'm not aware of the language allowing typecasts, only that in GHC various `unsafe*` functions will let you do things like cast a float to a double to a pointer. The result will be nonsense, but that'll be your fault, and it's not so much a cast as telling the compiler to break all of its rules as you say, "Trust me, I know what I'm doing." The compiler will be suspicious of your motivations but believe you. — Aaron Friel, Jul 19 '13 at 18:11
[I asked a potentially related question some months ago and got good answers](http://stackoverflow.com/questions/14273235/can-gadts-be-used-to-prove-type-inequalities-in-ghc). — Luis Casillas, Jul 19 '13 at 18:51
@AaronFriel - I am not sure if this counts as a typecast, but features like OverloadedStrings cause implicit cast of literals. Also, there can be implicit cast of number literals to either int or integer. Maybe cast is not the right word here, but what I am saying is that just the literal itself doesn't always have the same type. — tohava, Jul 19 '13 at 22:22
Cast is definitely the wrong word, but yes, literals are overloaded. But there are no typecasts or implicit conversions between types. `5 :: Integer` will always, always be an `Integer`. And `"Hello!" :: ByteString` won't ever suddenly become not a `ByteString` merely by how you use it. — Aaron Friel, Jul 19 '13 at 22:43

cdk · Accepted Answer · 2013-07-19T23:12:16.070

8

With new features being added to GHC, you'll be able to write:

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-}

type family Equal (a :: k) (b :: k) :: Bool
type instance where
   Equal a a = True
   Equal a b = False

edited Jul 19 '13 at 23:12

answered Jul 19 '13 at 22:56

cdk

6,698
24
51

The syntax they ultimately chose was different. Now you'd write `type family Equal (a :: k) (b :: k) :: Bool where { Equal a a = 'True; Equal a b = 'False }`. The braces, of course, wouldn't be necessary if I could write a multi-line comment. – dfeuer May 23 '16 at 16:38

score 2 · Answer 2 · answered Jul 22 '13 at 18:12

This is how it is done in the HList library

{-# LANGUAGE FlexibleInstances, 
    MultiParamTypeClasses, 
    FunctionalDependencies, 
    UndecidableInstances ,
    IncoherentInstances
 #-}

data HTrue; data HFalse;

class TypeCast a b | a -> b
instance TypeCast a a

class TypeEq a b c | a b -> c
instance TypeEq x x HTrue
instance (TypeCast HFalse b) => TypeEq x y b
-- instance TypeEq x y HFalse -- would violate functional dependency

You can fully infer type equality now:

typeEq :: TypeEq a b c => a -> b -> c
typeEq _ _ = undefined

Note that typeEq 0 1 == HFalse since 0 :: Num a => a and 1 :: Num b => b.

Note that until the new features defined in the other answer are rolled out, this is basically _the_ way to do it. — sclv, Jul 23 '13 at 01:06

'idiomatic' Haskell type inequality

2 Answers2

Linked