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
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
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
On Sep 15, 2014, at 9:14 AM, Arnaud Bailly <arnaud.oqube@gmail.com> 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
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 <eir@cis.upenn.edu> wrote:
On Sep 15, 2014, at 9:14 AM, Arnaud Bailly <arnaud.oqube@gmail.com> 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
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/
* Richard Eisenberg <eir@cis.upenn.edu> [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 <KAction@gnu.org>, Free Software supporter, esperantisto and netiquette guardian. GPG: 54B7F00D
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 :) ) https://hackage.haskell.org/package/HList On Mon, Sep 15, 2014 at 12:58 PM, Dmitry Bogatov <KAction@gnu.org> wrote:
* Richard Eisenberg <eir@cis.upenn.edu> [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 <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
participants (5)
-
Adam Gundry -
Arnaud Bailly -
Carter Schonwald -
Dmitry Bogatov -
Richard Eisenberg