rebind ifThenElse

Interlude.cabal

@@ -13,13 +13,13 @@ cabal-version:       >=1.10
 
 library
   exposed-modules:     Relation.Equality, Data.TypeClass,
-                       Data.Bool, Data.Nat, Data.Integer
+                       Data.Bool, Data.Nat, Data.Fin, Data.Integer
                        Data.Function, Data.Vec
   other-extensions:    GADTs, DataKinds, TypeFamilies, TypeOperators,
                        StandaloneDeriving, ScopedTypeVariables,
                        UndecidableInstances, NoImplicitPrelude,
                        TemplateHaskell, QuasiQuotes, PolyKinds,
-                       UnicodeSyntax
-  build-depends:       base ==4.*, singletons, integer-gmp
+                       UnicodeSyntax, RebindableSyntax
+  build-depends:       base ==4.*, singletons, integer-gmp, ghc-prim
   hs-source-dirs:      src
   default-language:    Haskell2010

src/Data/Bool.hs

@@ -9,16 +9,23 @@
 {-# LANGUAGE QuasiQuotes           #-}
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE UnicodeSyntax         #-}
+{-# LANGUAGE RebindableSyntax      #-}
 
 -- | Defines the boolean type and logical operators
 module Data.Bool where
 
+
 import Data.Kind      (Type)
-import Data.TypeClass (Eq, Enum, Show)
+import Data.TypeClass (Eq(..), Enum, Show)
+import GHC.Types      (Bool(..))
 import Data.Singletons.TH
 import Data.Singletons.Prelude.Enum
 
 
+class IfThenElse b where
+  ifThenElse ∷ b -> a -> a -> a
+
+
 singletons [d|
 
   -- | Boolean Type
@@ -49,3 +56,13 @@ singletons [d|
 
   |]
 
+-- | Values equality
+(≡) ∷ Eq a ⇒ a → a → 𝔹
+x ≡ y = case x == y of
+  True  → T
+  False → F
+
+instance IfThenElse 𝔹 where
+  ifThenElse T x y = x
+  ifThenElse F x y = y
+