[Haskell-cafe] Replace data constructors via meta programming

[Li-yao Xia]

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.
>