[Haskell-cafe] Type union

[Richard Eisenberg]

Have you tried using closed type families with the type-level (==) operator from GHC 7.8's Data.Type.Equality? That's how I've done unions before. The key step is to use a closed type family to write a type family equation that triggers when two types do *not* equal.

Let me know if you need more info...

Richard

On Sep 14, 2014, at 10:32 AM, Dmitry Bogatov <KAction at gnu.org> wrote:

> Hello!
> 
> I am trying to create type safe boolean formula representation.  Main
> operation is substion of particular value, to get another formula, and
> function that accept formula to calculate it's value.
> 
> So target is:
> 
> a = Conjunction (Var X) (Var Y) is 2 variable formula
> value (apply (X, True) . apply (Y, True) $ a) -- True
> 
> and neither
> 
> value a
> apply (X, True) . apply (X, False) $ a
> 
> typechecks.
> 
> How can I archive it?
> 
> 	class Union a b c
> 	instance (a ~ b) => Union a b b
> 	instance Union a b (a, b)
> 
> 	data P = P deriving Show
> 	data Q = Q deriving Show
> 	class (Show a) => Variable a
> 	instance Variable P
> 	instance Variable Q
> 
> 	data Formula t where
> 	  Prop :: (Variable b) => b -> Formula b
> 	  Conjunction :: (Union t1 t2 t3) =>
> 		Formula t1 -> Formula t2 -> Formula t3
> 
> 	deriving instance Show (Formula t)
> 	main = print (Conjunction (Prop P) (Prop Q) :: Int)
> 
> This complains on ambitious t3.
> 
> Attempt by typefamilies fails, since
> 
> 	type family Union t1 t2 :: *
> 	data Void
> 	type instance Union a a = a
> 	type instance Union (a, b) a = (a, b)
> 	type instance Union (a, b) b = (a, b)
> 	type instance Union (a, b) c = (a, b, c)
> 	type instance Union a (a, b)  = (a, b)
> 	type instance Union b (a, b)  = (a, b)
> 	type instance Union c (a, b) = (a, b, c)
> 	type instance Union (a, b, c) a = (a, b, c)
> 	type instance Union (a, b, c) b = (a, b, c)
> 	type instance Union (a, b, c) c = (a, b, c)
> 	type instance Union (a, b, c) d = Void
> 	type instance Union a (a, b, c) = (a, b, c)
> 	type instance Union b (a, b, c) = (a, b, c)
> 	type instance Union c (a, b, c) = (a, b, c)
> 	type instance Union d (a, b, c) = Void
> 
> this is somewhy conflicting instances. I am out of ideas.
> 
> --
> Best regards, Dmitry Bogatov <KAction at gnu.org>,
> Free Software supporter, esperantisto and netiquette guardian.
> GPG: 54B7F00D
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe