Type union

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
9 messages Options
Reply | Threaded
Open this post in threaded view
|

Type union

Dmitry Bogatov
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 <[hidden email]>,
Free Software supporter, esperantisto and netiquette guardian.
GPG: 54B7F00D

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

attachment0 (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Type union

Richard Eisenberg-2
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 <[hidden email]> 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 <[hidden email]>,
> Free Software supporter, esperantisto and netiquette guardian.
> GPG: 54B7F00D
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type union

Arnaud Bailly-2
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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]>,
> Free Software supporter, esperantisto and netiquette guardian.
> GPG: 54B7F00D
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type union

Richard Eisenberg-2
On Sep 15, 2014, at 9:14 AM, Arnaud Bailly <[hidden email]> wrote:

> 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

How is this different from `Either Int (Either String Bool)`?

Richard
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type union

Arnaud Bailly-2
Technically it is not different but it allows one to write things in a much more compact way. And I would like the :|  types to be of arbitrary size, meaning each `in x y` invocation would inject a value at the right position in the sum type without having to declare all the possible sizes of coproducts. But maybe I could simply do that for some arbitrarily large number of types....

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

On Mon, Sep 15, 2014 at 3:38 PM, Richard Eisenberg <[hidden email]> wrote:
On Sep 15, 2014, at 9:14 AM, Arnaud Bailly <[hidden email]> wrote:

> 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

How is this different from `Either Int (Either String Bool)`?

Richard


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type union

Dmitry Bogatov
In reply to this post by Richard Eisenberg-2
* Richard Eisenberg <[hidden email]> [2014-09-15 08:56:05-0400]
> 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...
Thanks. I will take a look for my education, but
I am on Debian, so no more, then ghc 7.6.3.

I found type-settheory package, but it fails to build.

--
Best regards, Dmitry Bogatov <[hidden email]>,
Free Software supporter, esperantisto and netiquette guardian.
GPG: 54B7F00D

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

attachment0 (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Type union

Carter Schonwald
i should point out the HList package has a lot of tooling for things like this, and the author Adam says that its quite usable (aside from the dearth of docs beyond the crazy typeful haddocks :) )


On Mon, Sep 15, 2014 at 12:58 PM, Dmitry Bogatov <[hidden email]> wrote:
* Richard Eisenberg <[hidden email]> [2014-09-15 08:56:05-0400]
> 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...
Thanks. I will take a look for my education, but
I am on Debian, so no more, then ghc 7.6.3.

I found type-settheory package, but it fails to build.

--
Best regards, Dmitry Bogatov <[hidden email]>,
Free Software supporter, esperantisto and netiquette guardian.
GPG: 54B7F00D

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type union

Adam Gundry-2
In reply to this post by Arnaud Bailly-2
Hi Arnaud,

You can't quite write what you asked for, but you can get pretty close,
as long as you don't mind Peano naturals rather than integer literals,
and an extra (partially-defined) element:

{-# LANGUAGE GADTs, TypeOperators #-}

type (:|) = Either
infixr 5 :|

data In x xs where
  Zero :: In x (x :| xs)
  Suc  :: In x xs -> In x (y :| xs)

inj :: In x xs -> x -> xs
inj Zero    = Left
inj (Suc n) = Right . inj n

data Void

f :: Int -> Int :| String :| Bool :| Void
f 0 = inj Zero             1
f 1 = inj (Suc Zero)       "foo"
f 2 = inj (Suc (Suc Zero)) True

I'm not sure how useful this is in practice, however.

Hope this helps,

Adam


On 15/09/14 14:14, Arnaud Bailly wrote:

> 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

--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type union

oleg-30
In reply to this post by Dmitry Bogatov

Type unions are also necessary for extensible effects. In fact, they
are the foundation of extensible effects. One implementation

        http://okmij.org/ftp/Haskell/extensible/TList.hs

uses only common and uncontroversial extensions (No Typeable). It
could be converted to closed type families. The other, more optimal
implementation, relies on Typeable, so that injection and projection
become constant time, regardless of the size of the union. The
Typeable constraint can be dispensed with; see the HList
implementation of type-indexed coproducts (TIC), which are essentially
open unions.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe