Modela la representación de expresiones booleanas y posee una función que dice si una expresión es una tautología o no. Esta es la visión como un coalgebra del problema, no utiliza recursión. Tiene la ventaja sobre la visión como un algebra de permitir extender el código sin modificar el original, de este modo se pueden agregar extensiones.

tautologia.hs

{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Rank2Types #-}

import Data.List         (nub, subsequences)
import Data.List.Unicode ((∈))
import Data.Functor      ((<$>))

infixr 3 ∧
infixr 2 ∨
class FPropSym repr where
  false, true ∷ repr
  neg         ∷ repr → repr
  (∧), (∨)    ∷ repr → repr → repr

infixr 3 `y`
infixr 2 `o`
y, o ∷ FPropSym repr ⇒ repr → repr → repr
y = (∧)
o = (∨)

instance FPropSym String where
  false = "false"
  true  = "true"
  neg f = "neg (" ++ f ++ ")"
  a ∧ b = "(" ++ a ++ ") ∧ (" ++ b ++ ")"
  a ∨ b = "(" ++ a ++ ") ∨ (" ++ b ++ ")"

showFProp ∷ (∀ repr. FPropSym repr ⇒ repr) → String
showFProp f = f

instance FPropSym Bool where
  false = False
  true  = True
  neg   = not
  (∧)   = (&&)
  (∨)   = (||)

evalFProp ∷ (∀ repr. FPropSym repr ⇒ repr) → Bool
evalFProp f = f

----------------------------------------------------------
infixr 1 ==>
class FPropSym repr ⇒ ImplicaSym repr where
  (==>) ∷ repr → repr → repr

instance ImplicaSym String where
  a ==> b = "(" ++ a ++ ") ==> (" ++ b ++ ")"

showImplica ∷ (∀ repr. ImplicaSym repr ⇒ repr) → String
showImplica f = f

instance ImplicaSym Bool where
  a ==> b = (neg a) ∨ b

evalImplica ∷ (∀ repr. ImplicaSym repr ⇒ repr) → Bool
evalImplica f = f

------------------------------------------------------------
class ImplicaSym repr ⇒ VariableSym repr where
  var ∷ String → repr

type FPropV = ∀ repr. VariableSym repr ⇒ repr

instance VariableSym String where
  var nombre = nombre

showVariable ∷ FPropV → String
showVariable f = f

instance FPropSym [String] where
  false = []
  true  = []
  neg   = id
  (∧)   = (++)
  (∨)   = (++)

instance ImplicaSym [String] where
  a ==> b = a ++ b

instance VariableSym [String] where
  var nombre = [nombre]

vars ∷ FPropV → [String]
vars f = nub f

instance FPropSym ((String → Bool) → Bool) where
  false = const false
  true  = const true
  neg   = (neg .)
  l ∧ r = \ asignación → l asignación ∧ r asignación
  l ∨ r = \ asignación → l asignación ∨ r asignación

instance ImplicaSym ((String → Bool) → Bool) where
  a ==> b = \ asignación → a asignación ==> b asignación

instance VariableSym ((String → Bool) → Bool) where
  var nombre = \ asignación → asignación nombre

evalVariable ∷ FPropV → [String] → Bool
evalVariable f l = f (∈ l)


isTautology ∷ FPropV → Bool
isTautology f = and (evalVariable f <$> subsequences (vars f))