Language/Symantic/Type/Maybe.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE Rank2Types #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# LANGUAGE UndecidableInstances #-}
   8 {-# OPTIONS_GHC -fno-warn-orphans #-}
   9 module Language.Symantic.Type.Maybe where
  10
  11 import Data.Proxy
  12
  13 import Language.Symantic.Type.Common
  14
  15 -- * Type 'Type_Maybe'
  16 -- | The 'Maybe' type.
  17 type Type_Maybe = Type_Type1 Maybe
  18
  19 instance -- String_from_Type
  20  String_from_Type root =>
  21  String_from_Type (Type_Maybe root) where
  22         string_from_type (Type_Type1 _f a) =
  23                 "Maybe" ++ " (" ++ string_from_type a ++ ")"
  24
  25 -- | Inject a 'Type_Maybe' within a root type.
  26 type_maybe
  27  :: Lift_Type_Root Type_Maybe root
  28  => root h_a
  29  -> root (Maybe h_a)
  30 type_maybe = lift_type_root . Type_Type1 (Proxy::Proxy Maybe)
  31
  32 is_type_maybe
  33  :: forall tys (root:: * -> *) h.
  34  Unlift_Type Type_Maybe tys =>
  35  tys root h -> Maybe (Type_Maybe root h)
  36 is_type_maybe = unlift_type
  37
  38 instance
  39  ( Lift_Type_Root Type_Maybe root
  40  , Unlift_Type Type_Maybe root'
  41  , Lift_Error_Type (Error_Type (Type_Root root' h)) (Error_of_Type (Type_Root root' h) root)
  42  , Implicit_HBool (Is_Last_Type (Type_Maybe root) root)
  43  ) => Type1_from (Type_Root root' h) (Type_Maybe root) where
  44         type1_from ty root_x k =
  45                 case is_type_maybe $ unType_Root root_x of
  46                  Just _ty_a -> k (Proxy::Proxy Maybe) type_maybe
  47                  Nothing -> Left $ error_type_unsupported ty root_x