Hi, I am looking for a solution to get rid of this silly boilerplate: eval :: Ord var => Map var Bool -> Proposition var -> Bool eval ctx prop = evalP $ fmap (ctx Map.!) prop where evalP = \case Var b -> b Not q -> not $ evalP q And p q -> evalP p && evalP q Or p q -> evalP p || evalP q If p q -> evalP p ==> evalP q Iff p q -> evalP p == evalP q What I would like to do in essence is to replace the data constructors like so: -- Not valid Haskell!! Can't pattern match on constructor only... magic = \case Var -> id Not -> not And -> (&&) Or -> (||) If -> (==>) Iff -> (==) compile = transformAST magic $ fmap (\case 'P' -> False; 'Q' -> True) >>> compile (Iff (Not (And (Var 'P') (Var 'Q'))) (Or (Not (Var 'P')) (Not (Var 'Q')))) ((==) (not ((&&) (id True) (id False))) ((||) (not (id True)) (not (id False)))) Note how the compiled expression exactly mirrors the AST, so there should be some meta programming technique for this. Does anyone have an idea how I can achieve this? The full source code is here: https://gist.github.com/vimuel/7dcb8a9f1d2b7b72f020d66ec4157d7b I am happy to take any other comments relating to my code... Best, Vilem _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
On 2018-02-12 03:30, Vilem-Benjamin Liepelt wrote:
> I am looking for a solution to get rid of this silly boilerplate: > > eval :: Ord var => Map var Bool -> Proposition var -> Bool > eval ctx prop = evalP $ fmap (ctx Map.!) prop > where > evalP = \case > Var b -> b > Not q -> not $ evalP q > And p q -> evalP p && evalP q > Or p q -> evalP p || evalP q > If p q -> evalP p ==> evalP q > Iff p q -> evalP p == evalP q [..] You might benefit from the 'catamorphism' package: https://hackage.haskell.org/package/catamorphism-0.5.1.0/docs/Data-Morphism-Cata.html It provides a template Haskell function which, given a data type, produces a function which reduces (folds) that data type. -- Frerich Raabe - [hidden email] www.froglogic.com - Multi-Platform GUI Testing _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by Vilem-Benjamin Liepelt-2
Hi Vilem,
One possible solution here is to define a fold function that captures the relationship between constructors and functions to substitute instead (please see the Logic.hs attachment). But it may be a bit error-prone to use because the relationship is captured implicitly by corresponding argument of the 'foldProposition' function. Another approach with a bit more upfront boilerplate, but hopefully less code later, would be recursion schemes. Please refer to LogicRecSchemes.hs for a sample. In order to learn more you can either read https://github.com/willtim/recursion-schemes/raw/master/slides-final.pdf or https://github.com/sergv/kievfprog-2017-november/blob/master/Talk.pdf or listen to any recent talk on the topic. Regards, Sergey On 02/12/2018 02:30 AM, Vilem-Benjamin Liepelt wrote: > Hi, > > I am looking for a solution to get rid of this silly boilerplate: > > eval :: Ord var => Map var Bool -> Proposition var -> Bool > eval ctx prop = evalP $ fmap (ctx Map.!) prop > where > evalP = \case > Var b -> b > Not q -> not $ evalP q > And p q -> evalP p && evalP q > Or p q -> evalP p || evalP q > If p q -> evalP p ==> evalP q > Iff p q -> evalP p == evalP q > > What I would like to do in essence is to replace the data constructors > like so: > > -- Not valid Haskell!! Can't pattern match on constructor only... > magic = \case > Var -> id > Not -> not > And -> (&&) > Or -> (||) > If -> (==>) > Iff -> (==) > > compile = transformAST magic $ fmap (\case 'P' -> False; 'Q' -> True) > >>>> compile (Iff (Not (And (Var 'P') (Var 'Q'))) (Or (Not (Var 'P')) > (Not (Var 'Q')))) > ((==) (not ((&&) (id True) (id False))) ((||) (not (id > True)) (not (id False)))) > > Note how the compiled expression exactly mirrors the AST, so there > should be some meta programming technique for this. > > Does anyone have an idea how I can achieve this? > > The full source code is here: > https://gist.github.com/vimuel/7dcb8a9f1d2b7b72f020d66ec4157d7b > > I am happy to take any other comments relating to my code... > > Best, > > Vilem > > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post. > _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. Logic.hs (1K) Download Attachment LogicRecSchemes.hs (1K) Download Attachment signature.asc (235 bytes) Download Attachment |
In reply to this post by Frerich Raabe
Frerich Raabe <[hidden email]> writes:
> You might benefit from the 'catamorphism' package: > > https://hackage.haskell.org/package/catamorphism-0.5.1.0/docs/Data-Morphism-Cata.html catamorphism would be a great solution to this kind of problem, but unfortunately it does not work with any 8.x version of GHC: https://github.com/frerich/catamorphism/issues/5 That makes its use impractical for most purposes, IMHO. Best regards, Peter _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
On 2018-02-12 10:38, Peter Simons wrote:
> Frerich Raabe <[hidden email]> writes: > >> You might benefit from the 'catamorphism' package: >> >> >> https://hackage.haskell.org/package/catamorphism-0.5.1.0/docs/Data-Morphism-Cata.html > > catamorphism would be a great solution to this kind of problem, but > unfortunately it does not work with any 8.x version of GHC: > > https://github.com/frerich/catamorphism/issues/5 > > That makes its use impractical for most purposes, IMHO. Oh, drat. I forgot about that issue (I'm still not on GHC 8.x, ahem). :-( -- Frerich Raabe - [hidden email] www.froglogic.com - Multi-Platform GUI Testing _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by Vilem-Benjamin Liepelt-2
One option, inspired by the Syntactic package, is to factor out
application from Proposition. I pasted an example here: http://lpaste.net/362410 `evalSym` is quite close to your `magic` function: evalSym :: Map Name Bool -> Sym a -> a evalSym ctx (Var v) = ctx ! v evalSym _ Not = not evalSym _ And = (&&) / Emil Den 2018-02-12 kl. 02:30, skrev Vilem-Benjamin Liepelt: > Hi, > > I am looking for a solution to get rid of this silly boilerplate: > > eval :: Ord var => Map var Bool -> Proposition var -> Bool > eval ctx prop = evalP $ fmap (ctx Map.!) prop > where > evalP = \case > Var b -> b > Not q -> not $ evalP q > And p q -> evalP p && evalP q > Or p q -> evalP p || evalP q > If p q -> evalP p ==> evalP q > Iff p q -> evalP p == evalP q > > What I would like to do in essence is to replace the data constructors like so: > > -- Not valid Haskell!! Can't pattern match on constructor only... > magic = \case > Var -> id > Not -> not > And -> (&&) > Or -> (||) > If -> (==>) > Iff -> (==) > > compile = transformAST magic $ fmap (\case 'P' -> False; 'Q' -> True) > >>>> compile (Iff (Not (And (Var 'P') (Var 'Q'))) (Or (Not (Var 'P')) (Not (Var 'Q')))) > ((==) (not ((&&) (id True) (id False))) ((||) (not (id True)) (not (id False)))) > > Note how the compiled expression exactly mirrors the AST, so there should be some meta programming technique for this. > > Does anyone have an idea how I can achieve this? > > The full source code is here: https://gist.github.com/vimuel/7dcb8a9f1d2b7b72f020d66ec4157d7b > > I am happy to take any other comments relating to my code... > > Best, > > Vilem > > > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post. > Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by Vilem-Benjamin Liepelt-2
Hello,
Here's a quick demo of the finally-tagless style for this kind of problem. It is an alternative to defining a data type to represent the syntax, with a fold function (or "catamorphism") to deconstruct it. For more information: http://okmij.org/ftp/tagless-final/index.html Note that although you can't redefine constructors, you can rebind variables like "not", "(&&)"... The idea is that users can construct terms using these functions abstractly, and to evaluate those terms is to provide a definition of those functions. data PropSyntax v prop = PropSyntax { var :: v -> prop, (&&) :: prop -> prop -> prop, not :: prop -> prop -- etc } propSyntax :: PropSyntax v (Proposition v) propSyntax = PropSyntax Var And Not -- etc That is boilerplate that we can derive from the Proposition data type, or we can conversely derive the Proposition type from the record definition. (A Proposition is a "free object".) An evaluator is given by another record value. boolSyntax :: Ord v => Map v Bool -> PropSyntax v Bool boolSyntax m = PropSyntax (m Map.!) (Prelude.&&) Prelude.not -- etc We represent PropSyntax with a record instead of a type class in order to define implementations that depend on other values, such as boolSyntax depending on a map. It may be possible to use type classes at the same time to make it easier to construct propositions; for simple definitions, using RecordWildCards seems sufficiently discreet. example :: PropSyntax Bool prop -> prop example PropSyntax{..} = ((==) (not ((&&) (id True) (id False))) ((||) (not (id True)) (not (id False)))) -- All variables here assumed to be bound by PropSyntax{..} An evaluator is a record, an expression is a function, evaluation is function application. evalWith :: PropSyntax v prop -> (PropSyntax v prop -> r) -> r evalWith x f = f x exampleBool :: Bool exampleBool = evalWith boolSyntax example Li-yao On 02/11/2018 09:30 PM, Vilem-Benjamin Liepelt wrote: > Hi, > > I am looking for a solution to get rid of this silly boilerplate: > > eval :: Ord var => Map var Bool -> Proposition var -> Bool > eval ctx prop = evalP $ fmap (ctx Map.!) prop > where > evalP = \case > Var b -> b > Not q -> not $ evalP q > And p q -> evalP p && evalP q > Or p q -> evalP p || evalP q > If p q -> evalP p ==> evalP q > Iff p q -> evalP p == evalP q > > What I would like to do in essence is to replace the data constructors > like so: > > -- Not valid Haskell!! Can't pattern match on constructor only... > magic = \case > Var -> id > Not -> not > And -> (&&) > Or -> (||) > If -> (==>) > Iff -> (==) > > compile = transformAST magic $ fmap (\case 'P' -> False; 'Q' -> True) > > >>> compile (Iff (Not (And (Var 'P') (Var 'Q'))) (Or (Not (Var 'P')) > (Not (Var 'Q')))) > ((==) (not ((&&) (id True) (id False))) ((||) (not (id > True)) (not (id False)))) > > Note how the compiled expression exactly mirrors the AST, so there > should be some meta programming technique for this. > > Does anyone have an idea how I can achieve this? > > The full source code is here: > https://gist.github.com/vimuel/7dcb8a9f1d2b7b72f020d66ec4157d7b > > I am happy to take any other comments relating to my code... > > Best, > > Vilem > > > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post. > Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by Peter Simons-2
On 2018-02-12 10:38, Peter Simons wrote:
> Frerich Raabe <[hidden email]> writes: > >> You might benefit from the 'catamorphism' package: >> >> >> https://hackage.haskell.org/package/catamorphism-0.5.1.0/docs/Data-Morphism-Cata.html > > catamorphism would be a great solution to this kind of problem, but > unfortunately it does not work with any 8.x version of GHC: > > https://github.com/frerich/catamorphism/issues/5 > > That makes its use impractical for most purposes, IMHO. Thanks for the prodding - I now finally got my act together and updated the package to work with GHC 8.x (and setup Travis CI while I was at it to try different GHC versions). -- Frerich Raabe - [hidden email] www.froglogic.com - Multi-Platform GUI Testing _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by Vilem-Benjamin Liepelt-2
Vilem,
I suggest to use free monads. They reduce boilerplate a little. First, separate the variable form the rest of the syntax: data Prop v = Not v | And v v | Or v v | If v v | Iff v v -- maybe GHC can derive this instance for you, given the appropriate language extension flag. instance Functor Prop where fmap f (Not p) = Not (f p) fmap f (And p q) = And (f p) (f q) fmap f (Or p q) = Or (f p) (f q) fmap f (If p q) = If (f p) (f q) fmap f (Iff p q) = Iff (f p) (f q) Then use Control.Monad.Free from the package 'free'. It also has a template Haskell part. The function you want is called 'iter' there, and applying a context of type var -> Bool is simply fmap. Note that a Map from var to Bool does not always yield a total reduction, since your formula might contain variables that are not in the Map. data Free f var = Pure var | Free (f (Free f var)) instance Functor f => Monad (Free f) where return = Pure Pure a >>= f = f a Free m >>= f = Free (fmap ((=<<) f) m) type Proposition var = Free Prop var type Predicate = Free Prop Bool -- F-algebras for functor f class Functor f => FAlg f a where alg :: f a -> a instance FAlg Prop Bool where alg (Not b) = not b alg (And p q) = p && q alg (Or p q) = p || q alg (If p q) = not p || q alg (Iff p q) = p == q eval = iter alg :: Predicate -> Bool map_and_eval ctx = iter alg . fmap ctx If feasible, remove If and Iff from the Prop type and make them binary functions on type Proposition var instead. That reduces the boilerplate further. -- Olaf _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by Frerich Raabe
Thank you for your great suggestions.
The type-foo looks very cool and I will have to dig more into the different options. Generating a catamorphism using the library of the same name works like a charm and integrates well with my existing code—once I managed to get it to install (thank you Stack LTS!) it just worked out of the box and let me write a one-line evaluator and a one-line pretty-printer. Woohoo! Unfortunately It's not really viable to use this "for real" at the moment because it requires such an old version of GHC. Something I miss is the clear correspondence between data constructors and "substitutions" (like in my `magic` example), since they become entirely positional, leading to potentially brittle code (imagine reordering the data constructors). I think some of the other solutions might be better in this respect. It's a shame that the catamorphism package doesn't work for a more up-to-date version of GHC, because I think I would use this quite often. I suppose the fold that Sergey proposed is essentially what the catamorphism package generates. Although I want to avoid having to write functions by hand when really the computer should be doing them for me, I think I will use this for now as it integrates nicely with my existing code and leads to quite idiomatic Haskell. I will definitely check out the other suggestions as well though, thank you again. Best, Vilem > On 2018-02-12, at 09:08, Frerich Raabe <[hidden email]> wrote: > > On 2018-02-12 03:30, Vilem-Benjamin Liepelt wrote: >> I am looking for a solution to get rid of this silly boilerplate: >> eval :: Ord var => Map var Bool -> Proposition var -> Bool >> eval ctx prop = evalP $ fmap (ctx Map.!) prop >> where >> evalP = \case >> Var b -> b >> Not q -> not $ evalP q >> And p q -> evalP p && evalP q >> Or p q -> evalP p || evalP q >> If p q -> evalP p ==> evalP q >> Iff p q -> evalP p == evalP q > > [..] > > You might benefit from the 'catamorphism' package: > > https://hackage.haskell.org/package/catamorphism-0.5.1.0/docs/Data-Morphism-Cata.html > > It provides a template Haskell function which, given a data type, produces a function which reduces (folds) that data type. > > -- > Frerich Raabe - [hidden email] > www.froglogic.com - Multi-Platform GUI Testing _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Vilem, you may have missed the post from the catamorphisms author where he updated the library in response to this thread? :) On Feb 12, 2018 3:58 PM, "Vilem-Benjamin Liepelt" <[hidden email]> wrote: Thank you for your great suggestions. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Oh, indeed I wasn't aware of this. That's great news—thank you, Frerich!
This actually leads me to another question: what are the tradeoffs between implementing this via Template Haskell as in the case of this package vs the `deriving` mechanism as for the foldable instance? V
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by Vilem-Benjamin Liepelt-2
You actually can pattern match on constructor only: magic = \case Var {} -> id Not {}-> not And {} -> (&&) Or {} -> (||) If {} -> (==>) Iff {} -> (==) On Sun, Feb 11, 2018 at 6:30 PM, Vilem-Benjamin Liepelt <[hidden email]> wrote:
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Hi David,
I don't think this is well-typed. GHC seems to infer `Proposition a -> Bool -> Bool` (by majority vote?) but obviously then complains about the cases `id` and `not`. I believe that there is a way to do this with dependent types, but not sure whether this is possible in Haskell. Best, Vilem
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
PS: I meant cases `Var {}` and `Not {}`.
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
True, but my point about pattern matching constructors stands. On Thu, Feb 15, 2018 at 6:17 AM, Vilem-Benjamin Liepelt <[hidden email]> wrote:
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
In reply to this post by Vilem-Benjamin Liepelt-2
> -- Not valid Haskell!! Can't pattern match on constructor only... > magic = \case > Var -> id > Not -> not > And -> (&&) > Or -> (||) > If -> (==>) > Iff -> (==) This has often seemed to me to be a natural extension of case syntax. There is a short analysis in the following Reddit post: https://www.reddit.com/r/haskell/comments/7s0ski/lambdacase_in_the_wild/dt1zzyy/ I would be strongly in favour of adding an extension to do this (unless someone can find a reason that it couldn't work). Tom _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Just to cheerlead Tom, as I have nothing to add but wouldn't want it to seem like no one agreed, I also think this is a great idea. The objection on the Reddit thread about dependent functions isn't prohibitive: both of these features will be GHC extensions anyway. They can be exclusive. On Feb 18, 2018 05:11, "Tom Ellis" <[hidden email]> wrote:
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Free forum by Nabble | Edit this page |