Language/Symantic/Lib/Data/Bool.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE TypeFamilies #-}
   4 module Language.Symantic.Lib.Data.Bool where
   5
   6 -- * Type 'SBool'
   7 -- | Singleton for 'Bool'.
   8 data SBool b where
   9         STrue  :: SBool 'True
  10         SFalse :: SBool 'False
  11
  12 -- * Class 'IBool'
  13 -- | Implicitely construct a 'SBool' from a type of kind 'Bool'.
  14 class    IBool b      where iBool :: SBool b
  15 instance IBool 'True  where iBool = STrue
  16 instance IBool 'False where iBool = SFalse
  17
  18 -- * Type family 'HEq'
  19 -- | Host-type equality.
  20 type family HEq x y :: Bool where
  21         HEq x x = 'True
  22         HEq x y = 'False