Language/Symantic/Type/Maybe.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE PatternSynonyms #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# OPTIONS_GHC -fno-warn-orphans #-}
   7 module Language.Symantic.Type.Maybe where
   8
   9 import qualified Data.MonoTraversable as MT
  10 import Data.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12
  13 import Language.Symantic.Type.Root
  14 import Language.Symantic.Type.Type0
  15 import Language.Symantic.Type.Type1
  16 import Language.Symantic.Type.Constraint
  17 import Language.Symantic.Type.Family
  18
  19 -- * Type 'Type_Maybe'
  20 -- | The 'Maybe' type.
  21 type Type_Maybe = Type1 (Proxy Maybe)
  22
  23 pattern Type_Maybe :: root a -> Type_Maybe root (Maybe a)
  24 pattern Type_Maybe a = Type1 Proxy a
  25
  26 instance Type0_Constraint Eq root => Type0_Constraint Eq (Type_Maybe root) where
  27         type0_constraint c (Type1 _ a)
  28          | Just Dict <- type0_constraint c a
  29          = Just Dict
  30         type0_constraint _c _ = Nothing
  31 instance Type0_Constraint Ord root => Type0_Constraint Ord (Type_Maybe root) where
  32         type0_constraint c (Type1 _ a)
  33          | Just Dict <- type0_constraint c a
  34          = Just Dict
  35         type0_constraint _c _ = Nothing
  36 instance Type0_Constraint Monoid root => Type0_Constraint Monoid (Type_Maybe root) where
  37         type0_constraint c (Type1 _ a)
  38          | Just Dict <- type0_constraint c a
  39          = Just Dict
  40         type0_constraint _c _ = Nothing
  41 instance Type0_Constraint Num (Type_Maybe root)
  42 instance Type0_Constraint Integral (Type_Maybe root)
  43 instance Type0_Constraint MT.MonoFunctor (Type_Maybe root) where
  44         type0_constraint _c Type1{} = Just Dict
  45 instance Type1_Constraint Functor (Type_Maybe root) where
  46         type1_constraint _c (Type1 _ _) = Just Dict
  47 instance Type1_Constraint Applicative (Type_Maybe root) where
  48         type1_constraint _c (Type1 _ _) = Just Dict
  49 instance Type1_Constraint Foldable (Type_Maybe root) where
  50         type1_constraint _c (Type1 _ _) = Just Dict
  51 instance Type1_Constraint Traversable (Type_Maybe root) where
  52         type1_constraint _c (Type1 _ _) = Just Dict
  53 instance Type1_Constraint Monad (Type_Maybe root) where
  54         type1_constraint _c Type1{} = Just Dict
  55 instance Type0_Family Type_Family_MonoElement (Type_Maybe root) where
  56         type0_family _at (Type1 _px a) = Just a
  57 instance -- Type0_Eq
  58  Type0_Eq root =>
  59  Type0_Eq (Type_Maybe root) where
  60         type0_eq (Type1 _px1 a1) (Type1 _px2 a2)
  61          | Just Refl <- a1 `type0_eq` a2
  62          = Just Refl
  63         type0_eq _ _ = Nothing
  64 instance -- Type1_Eq
  65  Type1_Eq (Type_Maybe root) where
  66         type1_eq Type1{} Type1{}
  67          = Just Refl
  68 instance -- String_from_Type
  69  String_from_Type root =>
  70  String_from_Type (Type_Maybe root) where
  71         string_from_type (Type1 _f a) =
  72                 "Maybe" ++ " (" ++ string_from_type a ++ ")"
  73
  74 -- | Inject 'Type_Maybe' within a root type.
  75 type_maybe :: Type_Root_Lift Type_Maybe root => root h_a -> root (Maybe h_a)
  76 type_maybe = type1