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 |
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 |
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, 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. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 |
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.... 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: _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 |
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] _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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 |
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 |
Free forum by Nabble | Edit this page |