Initial commit

.envrc

@@ -0,0 +1 @@
+use flake gitlab:mangoiv/adhoc-ghc-shell

.gitignore

@@ -0,0 +1,2 @@
+dist-newstyle
+.direnv

CHANGELOG.md

@@ -0,0 +1,5 @@
+# Revision history for dependent-if
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

LICENSE

@@ -0,0 +1,20 @@
+Copyright (c) 2022 mangoiv
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

dependent-if.cabal

@@ -0,0 +1,47 @@
+cabal-version:      3.4
+name:               dependent-if
+version:            0.1.0.0
+-- synopsis:
+-- description:
+homepage:           https://sr.ht/~mangoiv/dependent-if
+license:            MIT
+license-file:       LICENSE
+author:             mangoiv
+maintainer:         contact@mangoiv.com
+-- copyright:
+category:           Data
+build-type:         Simple
+extra-doc-files:    CHANGELOG.md
+-- extra-source-files:
+
+common warnings
+    ghc-options: -Wall
+
+common extensions 
+    default-extensions: 
+      DataKinds
+      DerivingStrategies
+      GADTs
+      TypeFamilies 
+
+library
+    import:           
+      , warnings
+      , extensions
+    exposed-modules:  Data.Bool.IfThenElse
+    build-depends:    base ^>=4.16.3.0
+    hs-source-dirs:   src
+    default-language: GHC2021
+
+test-suite dependent-if-test
+    import:           
+      , warnings
+      , extensions
+    default-language: GHC2021
+    type:             exitcode-stdio-1.0
+    hs-source-dirs:   test
+    main-is:          Main.hs
+    build-depends:
+      , base ^>=4.16.3.0
+      , dependent-if
+      , HUnit

src/Data/Bool/IfThenElse.hs

@@ -0,0 +1,40 @@
+-- | Dependent If in Haskell, use this with `-XRebindableSyntax`
+module Data.Bool.IfThenElse (
+    SBool (..),
+    SomeBool (..),
+    ifThenElse,
+    IfThenElse,
+) where
+
+import Data.Kind (Type)
+
+-- | Singleton for Bool
+type SBool :: Bool -> Type
+data SBool b where
+    STrue :: SBool 'True
+    SFalse :: SBool 'False
+
+deriving stock instance (Show (SBool b))
+
+-- | Existential SBool
+type SomeBool :: Type
+data SomeBool = forall b. SomeBool (SBool b)
+
+deriving stock instance (Show SomeBool)
+
+-- | ifThenElse as type family, total
+type IfThenElse :: Bool -> Type -> Type -> Type
+type family IfThenElse b x y where
+    IfThenElse 'True x _ = x
+    IfThenElse 'False _ y = y
+
+-- | dependent if to be used with `-XRebindableSyntax`
+--
+-- /Examples/
+--
+-- > {\-# LANGUAGE RebindableSyntax #-\}
+-- > x :: SBool b -> IfThenElse b Integer String
+-- > x b = if b then 1 else "False"
+ifThenElse :: forall (b :: Bool) x y. SBool b -> x -> y -> IfThenElse b x y
+ifThenElse STrue x _ = x
+ifThenElse SFalse _ y = y

test/Main.hs

@@ -0,0 +1,19 @@
+{-# LANGUAGE RebindableSyntax #-}
+
+module Main (main) where
+
+import Control.Monad ((<=<))
+import Data.Bool.IfThenElse (IfThenElse, SBool (SFalse, STrue), ifThenElse)
+import Test.HUnit (Test (TestList), runTestTT, (~:), (~=?))
+import Prelude (IO, Integer, String, fromInteger, print, ($))
+
+example :: SBool b -> IfThenElse b Integer String
+example b = if b then (1 :: Integer) else "False"
+
+main :: IO ()
+main =
+    print <=< runTestTT $
+        TestList
+            [ "test true" ~: 1 ~=? example STrue
+            , "test false" ~: "False" ~=? example SFalse
+            ]