Language/Symantic/Type/IO.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.IO where
   8
   9 import qualified Data.MonoTraversable as MT
  10 import Data.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import qualified System.IO as IO
  13
  14 import Language.Symantic.Type.Root
  15 import Language.Symantic.Type.Type0
  16 import Language.Symantic.Type.Type1
  17 import Language.Symantic.Type.Constraint
  18 import Language.Symantic.Type.Family
  19
  20 -- * Type 'Type_IO'
  21 -- | The list type.
  22 type Type_IO          = Type1 (Proxy IO)
  23 type Type_IO_Handle   = Type0 (Proxy IO.Handle)
  24 type Type_IO_FilePath = Type0 (Proxy IO.FilePath)
  25 type Type_IO_Mode     = Type0 (Proxy IO.IOMode)
  26
  27 pattern Type_IO :: root a -> Type_IO root (IO a)
  28 pattern Type_IO a = Type1 Proxy a
  29
  30 instance Type0_Constraint Eq (Type_IO root)
  31 instance Type0_Constraint Ord (Type_IO root)
  32 instance Type0_Constraint Monoid (Type_IO root)
  33 instance Type0_Constraint Num (Type_IO root)
  34 instance Type0_Constraint Integral (Type_IO root)
  35 instance Type0_Constraint MT.MonoFunctor (Type_IO root) where
  36         type0_constraint _c Type1{} = Just Dict
  37 instance Type1_Constraint Functor (Type_IO root) where
  38         type1_constraint _c Type1{} = Just Dict
  39 instance Type1_Constraint Applicative (Type_IO root) where
  40         type1_constraint _c Type1{} = Just Dict
  41 instance Type1_Constraint Monad (Type_IO root) where
  42         type1_constraint _c Type1{} = Just Dict
  43 instance Type0_Family Type_Family_MonoElement (Type_IO root) where
  44         type0_family _at (Type1 _px a) = Just a
  45 instance -- Type0_Eq
  46  Type0_Eq root =>
  47  Type0_Eq (Type_IO root) where
  48         type0_eq (Type1 _px1 a1) (Type1 _px2 a2)
  49          | Just Refl <- a1 `type0_eq` a2
  50          = Just Refl
  51         type0_eq _ _ = Nothing
  52 instance -- Type1_Eq
  53  Type1_Eq (Type_IO root) where
  54         type1_eq Type1{} Type1{}
  55          = Just Refl
  56 instance -- String_from_Type
  57  String_from_Type root =>
  58  String_from_Type (Type_IO root) where
  59         string_from_type (Type1 _f a) =
  60                 "[" ++ string_from_type a ++ "]"
  61
  62 -- | Inject 'Type_IO' within a root type.
  63 type_io :: Type_Root_Lift Type_IO root => root h_a -> root (IO h_a)
  64 type_io = type1
  65
  66 -- | Inject 'Type_IO_Handle' within a root type.
  67 type_io_handle
  68  :: Type_Root_Lift Type_IO_Handle root
  69  => root IO.Handle
  70 type_io_handle = type_root_lift $ Type0 (Proxy::Proxy IO.Handle)
  71
  72 -- | Inject 'Type_IO_FilePath' within a root type.
  73 type_io_filepath
  74  :: Type_Root_Lift Type_IO_FilePath root
  75  => root IO.FilePath
  76 type_io_filepath = type_root_lift $ Type0 (Proxy::Proxy IO.FilePath)
  77
  78 -- | Inject 'Type_IO_Mode' within a root type.
  79 type_io_mode
  80  :: Type_Root_Lift Type_IO_Mode root
  81  => root IO.IOMode
  82 type_io_mode = type_root_lift $ Type0 (Proxy::Proxy IO.IOMode)