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 -- ** Type 'HBool'
  12 -- | Boolean singleton.
  13 data HBool b where
  14         HTrue  :: HBool 'True
  15         HFalse :: HBool 'False
  16 -- ** Class 'Implicit_HBool'
  17 -- | Construct a host-term boolean singleton from a host-type boolean.
  18 class    Implicit_HBool b      where hbool :: HBool b
  19 instance Implicit_HBool 'True  where hbool = HTrue
  20 instance Implicit_HBool 'False where hbool = HFalse