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 family 'HBool'
   7 -- | Host-type equality.
   8 type family HEq x y :: Bool where
   9         HEq x x = 'True
  10         HEq x y = 'False
  11
  12 -- ** Type 'HBool'
  13 -- | Boolean singleton.
  14 data HBool b where
  15         HTrue  :: HBool 'True
  16         HFalse :: HBool 'False
  17
  18 -- ** Class 'Implicit_HBool'
  19 -- | Construct a host-term boolean singleton from a host-type boolean.
  20 class    Implicit_HBool b      where hbool :: HBool b
  21 instance Implicit_HBool 'True  where hbool = HTrue
  22 instance Implicit_HBool 'False where hbool = HFalse