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 type Type_Maybe = Type_Type1 Maybe
  17 instance -- String_from_Type
  18  String_from_Type root =>
  19  String_from_Type (Type_Maybe root) where
  20         string_from_type (Type_Type1 _f a) =
  21                 "Maybe" ++ " (" ++ string_from_type a ++ ")"
  22
  23 -- | Inject a 'Type_Maybe' within a root type.
  24 type_maybe
  25  :: Type_Root_Lift Type_Maybe root
  26  => root h_a
  27  -> root (Maybe h_a)
  28 type_maybe = type_root_lift . Type_Type1 (Proxy::Proxy Maybe)
  29
  30 is_type_maybe
  31  :: forall tys (root:: * -> *) h.
  32  Type_Unlift Type_Maybe tys =>
  33  tys root h -> Maybe (Type_Maybe root h)
  34 is_type_maybe = type_unlift
  35
  36 instance
  37  ( Type_Root_Lift Type_Maybe root
  38  , Type_Unlift Type_Maybe root'
  39  , Error_Type_Lift (Error_Type (Type_Root root' h)) (Error_of_Type (Type_Root root' h) root)
  40  , Implicit_HBool (Is_Last_Type (Type_Maybe root) root)
  41  ) => Type1_from (Type_Root root' h) (Type_Maybe root) where
  42         type1_from ty root_x k =
  43                 case is_type_maybe $ unType_Root root_x of
  44                  Just _ty_a -> k (Proxy::Proxy Maybe) type_maybe
  45                  Nothing -> Left $ error_type_unsupported ty root_x