Hello,
I have a somewhat similar problem, trying to achieve union types but for the purpose of defining the set of allowable outcomes of a function. I have tried naively to define a type operator a :| b and I would like to be able to define a function like :

f :: Int -> Int :| String :| Bool
f 1 = in 1 1
f 2 = in 2 "foo"
f 3 = in 3 True

e.g. the codomain type is indexed by integers. I think this should be possible, even without full dependent typing given that I only expect to use literals

My type-level-fu is really lacking so help would be appreciated.

Regards,

--
Arnaud Bailly
FoldLabs Associate: http://foldlabs.com

On Mon, Sep 15, 2014 at 2:56 PM, Richard Eisenberg <eir@cis.upenn.edu> wrote:
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@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@gnu.org>,
> Free Software supporter, esperantisto and netiquette guardian.
> GPG: 54B7F00D
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe