use scott encoded booleans as in the Combinator based implementations

Author: Thomas Mahler

src/CCC/Cat.hs

@@ -1,9 +1,12 @@
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-
 {-- This module contains definition of categories that are required for
     modelling Closed Cartesian Categories.
   It re-exports Category from Control.Category and defines Monoidal, Cartesian and Closed.
+
+  Booleans are Scott-encoded as selector morphisms:
+    TRUE  = sndC  (selects second from a pair, like A combinator: λt e. e)
+    FALSE = fstC  (selects first from a pair, like K combinator: λt e. t)
+  Comparison operators return selector morphisms k (b,b) b instead of Bool values.
+  Conditionals are just application of the selector to a pair of alternatives.
     --}
 
 module CCC.Cat
@@ -14,13 +17,8 @@ module CCC.Cat
   , fanC
   , idC
   , NumCat (..)
-  , BoolCat (..)
-  , BoolLike (..)
-  , EqLike (..)
   , EqCat (..)
-  , IfValCat (..)
   , FixCat (..)
-  , Cond (..)
   ) where
 
 import           Control.Category (Category (..))
@@ -51,64 +49,17 @@ class Cartesian k => NumCat k where
   addC :: Num a => k (a, a) a
   subC :: Num a => k (a, a) a
   absC :: Num a => k a a
+  -- Comparison operators return Scott-encoded booleans (selector morphisms)
+  leqC :: Ord a => k (a, a) (k (b, b) b)
+  geqC :: Ord a => k (a, a) (k (b, b) b)
+  lesC :: Ord a => k (a, a) (k (b, b) b)
+  greC :: Ord a => k (a, a) (k (b, b) b)
 
-  --  eqlC :: (Eq a, BoolLike b)  => k (a,a) b
-  leqC :: (Ord a, BoolLike b) => k (a, a) b
-  geqC :: (Ord a, BoolLike b) => k (a, a) b
-  lesC :: (Ord a, BoolLike b) => k (a, a) b
-  greC :: (Ord a, BoolLike b) => k (a, a) b
-
-class Cartesian k => BoolCat k where
-  andC :: BoolLike a => k (a, a) a
-  orC :: BoolLike a => k (a, a) a
-  notC :: BoolLike a => k a a
-  ifTE :: k (Bool, (k b d, k b d)) (k b d)
-
-class BoolLike a where
-  (&&) :: a -> a -> a
-  (||) :: a -> a -> a
-  not :: a -> a
-  true :: a
-  false :: a
-
-instance BoolLike Bool where
-  (&&) = (Prelude.&&)
-  (||) = (Prelude.||)
-  not = Prelude.not
-  true = True
-  false = False
-
-class (BoolLike b) => EqLike a b where
-  (==) :: a -> a -> b
-
-instance EqLike Integer Bool where
-  (==) = (Prelude.==)
-
-instance EqLike Bool Bool where
-  (==) = (Prelude.==)
-
+-- Equality comparison returns a Scott-encoded boolean (selector morphism)
 class Cartesian k => EqCat k where
-  eqlC :: (EqLike a b, BoolLike b) => k (a, a) b
-
--- Value-level conditional: selects between two values based on boolean
-class Cartesian k => IfValCat k where
-  ifValC :: k (Bool, (a, a)) a
+  eqlC :: Eq a => k (a, a) (k (b, b) b)
 
 -- Fixpoint combinator for recursive definitions
 -- Takes a step function (rec, input) -> output and produces the fixed point
 class Closed k => FixCat k where
   fixC :: k (k a b, a) b -> k a b
-
--- Conditional type class for source-level if-then-else
--- Two-parameter class: c is the condition type, a is the branch type
--- This allows CatExpr z Bool as condition for CatExpr z a branches
-class Cond c a where
-  ite :: c -> a -> a -> a
-
-instance Cond Bool Bool where
-  ite True  t _ = t
-  ite False _ e = e
-
-instance Cond Bool Integer where
-  ite True  t _ = t
-  ite False _ e = e

src/CCC/CatExpr.hs

@@ -9,15 +9,19 @@
 {-- | GADT representing categorical expressions that instantiate type classes
     Closed, Cartesian, Category, and others. Serves as the compilation target for toCCC.
 
+    Booleans are Scott-encoded as selector morphisms (CatExpr (a,a) a):
+      TRUE  = Snd  (selects second, like A combinator)
+      FALSE = Fst  (selects first, like K combinator)
+    Conditionals are expressed as: Apply ∘ ⟨selector, ⟨thenVal, elseVal⟩⟩
+
     > toCCC @CatExpr (\(x, y) -> x)
     Comp Fst Id
 --}
 
 module CCC.CatExpr where
 
-import           CCC.Cat     (BoolCat (..), BoolLike (..), Cartesian (..), Cond (..),
-                          Category (..), Closed (..), EqCat (..), EqLike (..),
-                          FixCat (..), IfValCat (..), Monoidal (..), NumCat (..), fanC)
+import           CCC.Cat     (Cartesian (..), Category (..), Closed (..),
+                          EqCat (..), FixCat (..), Monoidal (..), NumCat (..), fanC)
 import           Prelude hiding (id, (.))
 
 data CatExpr a b where
@@ -38,21 +42,15 @@ data CatExpr a b where
   Curry :: CatExpr (a, b) c -> CatExpr a (CatExpr b c)
   Uncurry :: CatExpr a (CatExpr b c) -> CatExpr (a, b) c
   Lift :: (a -> b) -> CatExpr a b
-  Eql :: (EqLike a b, BoolLike b) => CatExpr (a, a) b
-  Leq :: (Ord a, BoolLike b) => CatExpr (a, a) b
-  Geq :: (Ord a, BoolLike b) => CatExpr (a, a) b
-  Les :: (Ord a, BoolLike b) => CatExpr (a, a) b
-  Gre :: (Ord a, BoolLike b) => CatExpr (a, a) b
-  -- Boolean combinators
-  And :: (BoolLike a) => CatExpr (a, a) a
-  Or :: (BoolLike a) => CatExpr (a, a) a
-  Not :: (BoolLike a) => CatExpr a a
-  T :: (BoolLike a) => CatExpr b a
-  F :: (BoolLike a) => CatExpr b a
-  -- Conditional branching: selects between morphisms based on a boolean
-  IfThenElse :: CatExpr (Bool, (CatExpr b c, CatExpr b c)) (CatExpr b c)
-  -- Value-level conditional: selects between values based on a boolean
-  IfVal :: CatExpr (Bool, (a, a)) a
+  -- Comparison operators return Scott-encoded booleans (selector morphisms)
+  -- A selector CatExpr (b,b) b picks one element from a pair:
+  --   Snd = TRUE  (selects second, like A: λt e. e)
+  --   Fst = FALSE (selects first, like K: λt e. t)
+  Eql :: (Eq a) => CatExpr (a, a) (CatExpr (b, b) b)
+  Leq :: (Ord a) => CatExpr (a, a) (CatExpr (b, b) b)
+  Geq :: (Ord a) => CatExpr (a, a) (CatExpr (b, b) b)
+  Les :: (Ord a) => CatExpr (a, a) (CatExpr (b, b) b)
+  Gre :: (Ord a) => CatExpr (a, a) (CatExpr (b, b) b)
   -- Fixpoint combinator for recursive definitions
   Fix :: CatExpr (CatExpr a b, a) b -> CatExpr a b
 
@@ -100,53 +98,16 @@ instance (Num a) => Num (CatExpr z a) where
   signum = error "TODO sig"
   fromInteger i = FromInt . IntConst i
 
-instance BoolCat CatExpr where
-  andC = And
-  orC = Or
-  notC = Not
-
-  ifTE = IfThenElse
-
-instance (BoolLike b) => BoolLike (CatExpr a b) where
-  f && g = And . fanC f g
-  f || g = Or . fanC f g
-  not f = Not . f
-  true = T
-  false = F
-
 instance EqCat CatExpr where
   eqlC = Eql
 
-instance IfValCat CatExpr where
-  ifValC = IfVal
-
 instance FixCat CatExpr where
   fixC = Fix
 
--- Cond instance for CatExpr: combines condition and branches
-instance Cond (CatExpr z Bool) (CatExpr z a) where
-  ite cond thenBranch elseBranch = IfVal . fanC cond (fanC thenBranch elseBranch)
-
 -- Apply a morphism-valued expression to an argument
 applyF :: CatExpr z (CatExpr a b) -> CatExpr z a -> CatExpr z b
 applyF f x = Apply . fanC f x
 
--- Equality comparison with fixed result type (avoids ambiguity)
-eqF :: (EqLike a Bool) => CatExpr z a -> CatExpr z a -> CatExpr z Bool
-eqF f g = Eql . fanC f g
-
--- Conditional with fixed condition type (avoids ambiguity)
-iteF :: CatExpr z Bool -> CatExpr z a -> CatExpr z a -> CatExpr z a
-iteF cond t e = IfVal . fanC cond (fanC t e)
-
--- General instance for comparing categorical morphisms
-instance {-# OVERLAPPABLE #-} (BoolLike b, EqLike a b) => EqLike (CatExpr z a) (CatExpr z b) where
-  f == g = Eql . fanC f g
-
--- Instance for comparing plain values to produce CatExpr (used by toCCC)
-instance {-# OVERLAPPABLE #-} (BoolLike b, EqLike a b) => EqLike a (CatExpr a b) where
-  x == y = Eql . fanC (Lift (const x)) (Lift (const y))
-
 instance Eq (CatExpr a b) where
   f == g = f Prelude.== g