title: Check whether formula is correct in haskell
body: <p>---- update 2 ----</p>
  
  <p>At last, he told me that is <code>Exists</code>…</p>
  
  <p>thank you all.</p>
  
  <p>---- update ----</p>
  
  <p>Okay, we call it <code>Forsome</code></p>
  
  <p><code>ex3: forsome  x0::[False,True]. forsome x1::[0,1,2]. (x0 || (0 &lt; x1))</code></p>
  
  <p>(whom told me "what is forall" added):</p>
  
  <pre><code>the constructor says "forall x in blah" but it really means "for some x in blah". 
  
  the formula is satisfied for some assignment of variables so it is satisfiable.
  </code></pre>
  
  <p>How can I do it?
  Thanks</p>
  
  <p>---- original ----</p>
  
  <p>Suppose we have a formula ex3</p>
  
  <p><code>ex3: forall x0::[False,True]. forall x1::[0,1,2]. (x0 || (0 &lt; x1))</code>.</p>
  
  <p>At first I think ex3 is <code>False</code>, cause when <code>x0 = False</code> and <code>x1 = 0</code> the formula is <code>(False || (0 &lt; 0))</code>  so ex3 is absolutely false. But I be told that ex3 is <code>True</code>, </p>
  
  <p><code>"satisfiable ex3 is true because there is at least one combination from sets x0 and x1 which returns true. So as long as there is 1 valid solution in Forall, it is true."</code></p>
  
  <p>Assume that is correct…</p>
  
  <p>I think it need to check groups of combination with same level but I am not figure out how to do it. To determine 'Are them same group` seems difficult.</p>
  
  <p>Here is my codes:</p>
  
  <p>File: Formula.hs</p>
  
  <pre><code>{-# LANGUAGE GADTs #-}
  
  module Formula where
  
  -- Datatype of formulas
  -- --------------------
  
  data Formula ts where
    Body   :: Term Bool                     -&gt; Formula ()
    Forall :: Show a 
           =&gt; [a] -&gt; (Term a -&gt; Formula as) -&gt; Formula (a, as)
  
  data Term t where
    Con     :: t         -&gt; Term t
    And     :: Term Bool -&gt; Term Bool -&gt; Term Bool
    Or      :: Term Bool -&gt; Term Bool -&gt; Term Bool
    Smaller :: Term Int  -&gt; Term Int  -&gt; Term Bool
    Plus    :: Term Int  -&gt; Term Int  -&gt; Term Int
    Name    :: String    -&gt; Term t    -- to facilitate pretty printing
  
  -- Pretty printing formulas
  -- ------------------------
  
  instance Show t =&gt; Show (Term t) where
    show (Con v)       = show v
    show (And p q)     = "(" ++ show p ++ " &amp;&amp; " ++ show q ++ ")"
    show (Or p q)      = "(" ++ show p ++ " || " ++ show q ++ ")"
    show (Smaller n m) = "(" ++ show n ++ " &lt; "  ++ show m ++ ")"
    show (Plus n m)    = "(" ++ show n ++ " + "  ++ show m ++ ")"
    show (Name name)   = name
  
  instance Show (Formula ts) where
    show = show' ['x' : show i | i &lt;- [0..]]
      where
        show' :: [String] -&gt; Formula ts' -&gt; String
        show' ns     (Body body)   = show body
        show' (n:ns) (Forall vs p) = "forall " ++ n ++ "::" ++ show vs ++ ". " ++ show' ns (p (Name n))
  
  
  -- Example formulas
  -- ----------------
  
  ex1 :: Formula ()
  ex1 = Body (Con True)
  
  ex2 :: Formula (Int, ())
  ex2 = Forall [1..10] $ \n -&gt;
          Body $ n `Smaller` (n `Plus` Con 1)
  
  ex3 :: Formula (Bool, (Int, ()))
  ex3 = Forall [False, True] $ \p -&gt; 
        Forall [0..2] $ \n -&gt; 
          Body $ p `Or` (Con 0 `Smaller` n)
  
  wrongFormula :: Formula (Int, ())
  wrongFormula = Forall [0..4] $ \n -&gt;
                   Body $ n `Smaller` (Con 0)
  </code></pre>
  
  <p>File: Solver.hs</p>
  
  <pre><code>{-# LANGUAGE GADTs #-}
  
  module Solver where
  
  import Formula
  
  
  -- Evaluating terms
  -- ----------------
  
  eval :: Term t -&gt; t
  eval (Con     v)   = v
  eval (And     p q) = eval p &amp;&amp; eval q
  eval (Or      p q) = eval p || eval q
  eval (Smaller n m) = eval n &lt;  eval m
  eval (Plus    n m) = eval n +  eval m
  eval (Name    _)   = error "eval: Name"
  
  
  -- Checking formulas
  -- -----------------
  
  satisfiable :: Formula ts -&gt; Bool
  satisfiable (Body body)    = eval body
  -- FIXME wrong implement
  --satisfiable (Forall xs f) = helper f xs
  --  where helper :: (Term a -&gt; Formula t) -&gt; [a] -&gt; Bool
  --        helper fn (a:as) = (satisfiable $ (fn . Con) a) &amp;&amp; (helper fn as)
  --        helper _ []     = True
  </code></pre>
  
  <p>Any suggestion will be appreciated.</p>