Language/Symantic/Type/Unit.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE TypeFamilies #-}
   5 module Language.Symantic.Type.Unit where
   6
   7 import Data.Maybe (isJust)
   8 import Data.Type.Equality ((:~:)(Refl))
   9
  10 import Language.Symantic.Type.Common
  11
  12 -- * Type 'Type_Unit'
  13 -- | The unit type.
  14 data Type_Unit (root:: * -> *) h where
  15         Type_Unit :: Type_Unit root ()
  16 type instance Root_of_Type      (Type_Unit root) = root
  17 type instance Error_of_Type ast (Type_Unit root) = No_Error_Type
  18
  19 instance -- Type_Eq
  20  Type_Eq (Type_Unit root) where
  21         type_eq Type_Unit Type_Unit = Just Refl
  22 instance -- Eq
  23  Eq (Type_Unit root h) where
  24         x == y = isJust $ x `type_eq` y
  25 instance -- String_from_Type
  26  String_from_Type (Type_Unit root) where
  27         string_from_type Type_Unit = "Unit"
  28 instance -- Show
  29  Show (Type_Unit root h) where
  30         show = string_from_type
  31 instance Type_Constraint Eq (Type_Unit root) where
  32         type_constraint _c Type_Unit = Just Dict
  33 instance Type_Constraint Ord (Type_Unit root) where
  34         type_constraint _c Type_Unit = Just Dict
  35
  36 -- | Convenient alias to include a 'Type_Unit' within a type.
  37 type_unit :: Type_Root_Lift Type_Unit root => root ()
  38 type_unit = type_root_lift Type_Unit