Language/Symantic/Type/Maybe.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE OverloadedStrings #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# LANGUAGE TypeOperators #-}
   8 module Language.Symantic.Type.Maybe where
   9
  10 import Data.Maybe (isJust)
  11 import Data.Type.Equality ((:~:)(Refl))
  12
  13 import Language.Symantic.Type.Common
  14
  15 -- * Type 'Type_Maybe'
  16 -- | The 'Maybe' type.
  17 data Type_Maybe root h where
  18         Type_Maybe :: root h_a
  19                    -> Type_Maybe root (Maybe h_a)
  20
  21 type instance Root_of_Type      (Type_Maybe root) = root
  22 type instance Error_of_Type ast (Type_Maybe root) = No_Error_Type
  23
  24 instance -- Eq_Type
  25  Eq_Type root =>
  26  Eq_Type (Type_Maybe root) where
  27         eq_type (Type_Maybe a1) (Type_Maybe a2)
  28          | Just Refl <- a1 `eq_type` a2
  29          = Just Refl
  30         eq_type _ _ = Nothing
  31 instance -- Eq
  32  Eq_Type root =>
  33  Eq (Type_Maybe root h) where
  34         x == y = isJust $ eq_type x y
  35 instance -- String_from_Type
  36  String_from_Type root =>
  37  String_from_Type (Type_Maybe root) where
  38         string_from_type (Type_Maybe a) =
  39                 "Maybe (" ++ string_from_type a ++ ")"
  40 instance -- Show
  41  String_from_Type root =>
  42  Show (Type_Maybe root h) where
  43         show = string_from_type
  44
  45 -- | Convenient alias to include a 'Type_Maybe' within a type.
  46 type_maybe
  47  :: Type_Root_Lift Type_Maybe root
  48  => root h_a
  49  -> root (Maybe h_a)
  50 type_maybe a = type_root_lift (Type_Maybe a)