I am currently writing some code to wrangle logical forms in a particular way. In pursuit of this, I have written the following code, which makes use of lenses:
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE Rank2Types #-}
module Logic.Internal.Formula where
import BasicPrelude hiding (empty, negate)
import qualified Data.Set as Set
import Control.Lens
data Atom = Pos { i :: Integer}
| Neg { i :: Integer}
deriving (Eq, Ord, Show, Read)
negatingAtom :: Iso' Atom Atom
negatingAtom = iso go go
where go (Pos x) = Neg x
go (Neg x) = Pos x
newtype Conjunction a = Conjunction (Set a)
deriving (Eq, Ord, Read, Show)
conjuncts :: Conjunction a -> [a]
conjuncts (Conjunction x) = Set.toList x
newtype Disjunction a = Disjunction (Set a)
deriving (Eq, Ord, Read, Show)
disjuncts :: Disjunction a -> [a]
disjuncts (Disjunction x) = Set.toList x
negatingClause :: Iso' (Conjunction Atom) (Disjunction Atom)
negatingClause = liftClause negatingAtom
type CNF = Conjunction (Disjunction Atom)
type DNF = Disjunction (Conjunction Atom)
-- Helper stuff
liftClause :: (Ord a) => Iso' a a -> Iso' (Conjunction a) (Disjunction a)
liftClause x = let pipeline = Set.fromList . fmap (view x) in
iso (Disjunction . pipeline . conjuncts) (Conjunction . pipeline . disjuncts)
Then, I attempted to write the following in (what I believed was) the natural way:
type CNF = Conjunction (Disjunction Atom)
type DNF = Disjunction (Conjunction Atom)
negatingForm :: Iso' CNF DNF
negatingForm = liftClause negatingClause
However, the typechecker was definitely not happy with this, and I'm not at all sure why. The exact output is below:
Couldn't match type ‘Conjunction Atom’ with ‘Disjunction Atom’
Expected type: p1 (Disjunction Atom) (f1 (Disjunction Atom))
-> p1 (Disjunction Atom) (f1 (Disjunction Atom))
Actual type: p1 (Disjunction Atom) (f1 (Disjunction Atom))
-> p1 (Conjunction Atom) (f1 (Conjunction Atom))
In the first argument of ‘liftClause’, namely ‘negatingClause’
In the expression: liftClause negatingClause
I'm a bit new to lenses, and would really like to understand what I misunderstood here, as well as how I would implement the required Iso.
(Answer also posted to http://lpaste.net/164691)
Here is a solution using TypeFamilies.
First we'll simplify the set up:
{-# LANGUAGE TypeFamilies #-}
import Control.Lens
data Atom = Pos Int | Neg Int deriving (Show)
newtype And a = And [a] deriving (Show)
newtype Or a = Or [a] deriving (Show)
The goal is create the following sequence of functions:
f0 :: Atom -> Atom g0 :: Atom -> Atom
f1 :: And Atom -> Or Atom g1 :: Or Atom -> And Atom
f2 :: And (Or Atom) -> Or (And Atom) g1 :: Or (And Atom) -> And (Or Atom)
...
The f's and g's are inverses of each other. From these functions we can
create the Iso' lenses:
iso0 = iso f0 g0 :: Iso' Atom Atom
iso1 = iso f1 g1 :: Iso' (And Atom) (Or Atom)
iso2 = iso f2 g2 :: Iso' (And (Or Atom)) (Or (And Atom))
We start by creating the type family Negated which acts as a type function.
Negated a is the type that an f-function (or g-function) maps a to.
type family Negated a
type instance Negated Atom = Atom
type instance Negated (And a) = Or (Negated a)
type instance Negated (Or a) = And (Negated a)
For instance, Negated (And (Or Atom)) is the type Or (And Atom)).
Next, we define a type class to perform the inverting operation:
class Invertible a where
invert :: a -> Negated a
instance Invertible Atom where
invert (Pos a) = Neg a
invert (Neg a) = Pos a
instance Invertible a => Invertible (And a) where
invert (And clauses) = Or (map invert clauses)
instance Invertible a => Invertible (Or a) where
invert (Or clauses) = And (map invert clauses)
The definitions of the isomorphisms are now trivial:
iso0 :: Iso' Atom Atom
iso0 = iso invert invert
iso1 :: Iso' (And Atom) (Or Atom)
iso1 = iso invert invert
iso2 :: Iso' (And (Or Atom)) (Or (And Atom))
iso2 = iso invert invert
Examples:
and1 = And [ Pos 1, Neg 2, Pos 3 ]
or1 = Or [and1]
test1 = invert and1 -- Or [Neg 1,Pos 2,Neg 3]
test2 = invert or1 -- And [Or [Neg 1,Pos 2,Neg 3]]
Note that one limitation of this approach to modeling logical predicates is that all the Atoms must be at the same depth in the expression tree.
E.g., you can't represent this tree (here x, y and z are Atoms):
and
/ \
x or
/ \
y z