[Haskell-cafe] Type union

[Arnaud Bailly]

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 at 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 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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140915/b75c504d/attachment.html>