Language/Symantic/Type/Type2.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# LANGUAGE UndecidableInstances #-}
   8 module Language.Symantic.Type.Type2 where
   9
  10 import Data.Maybe (isJust)
  11 import Data.Proxy
  12 import Data.Type.Equality ((:~:)(Refl))
  13
  14 import Language.Symantic.Lib.Data.Peano
  15 -- import Language.Symantic.Lib.Data.Bool
  16 import Language.Symantic.Type.Root
  17 -- import Language.Symantic.Type.Alt
  18 import Language.Symantic.Type.Error
  19 import Language.Symantic.Type.Type0
  20 -- import Language.Symantic.Type.Type1
  21
  22 -- * Type 'Type_Type2'
  23 data Type_Type2 px (root:: * -> *) h where
  24         Type_Type2
  25          :: px -> root a -> root b
  26          -> Type_Type2 px root ((Host2_of px) a b)
  27
  28 type instance Root_of_Type      (Type_Type2 px root) = root
  29 type instance Error_of_Type ast (Type_Type2 px root) = No_Error_Type
  30
  31 instance -- Eq_Type
  32  Eq_Type root =>
  33  Eq_Type (Type_Type2 (Proxy h2) root) where
  34         eq_type
  35          (Type_Type2 _ arg1 res1)
  36          (Type_Type2 _ arg2 res2)
  37          | Just Refl <- arg1 `eq_type` arg2
  38          , Just Refl <- res1 `eq_type` res2
  39          = Just Refl
  40         eq_type _ _ = Nothing
  41 instance -- Eq_Type
  42  Eq_Type root =>
  43  Eq_Type (Type_Type2 EPeano root) where
  44         eq_type (Type_Type2 p1 arg1 res1)
  45                 (Type_Type2 p2 arg2 res2)
  46          | p1 == p2
  47          , Just Refl <- arg1 `eq_type` arg2
  48          , Just Refl <- res1 `eq_type` res2
  49          = Just Refl
  50         eq_type _ _ = Nothing
  51 instance -- Eq
  52  Eq_Type root =>
  53  Eq (Type_Type2 (Proxy h2) root h) where
  54         x == y = isJust $ x `eq_type` y
  55 instance -- Eq
  56  Eq_Type root =>
  57  Eq (Type_Type2 EPeano root h) where
  58         x == y = isJust $ x `eq_type` y
  59 instance -- Show
  60  ( String_from_Type root
  61  , String_from_Type (Type_Type2 px root)
  62  ) => Show (Type_Type2 px root h) where
  63         show = string_from_type
  64
  65 -- | Inject a 'Type_Type2' within a root type.
  66 type_type2
  67  :: forall root h2 a b.
  68  Lift_Type_Root (Type_Type2 (Proxy h2)) root
  69  => root a -> root b -> root (h2 a b)
  70 type_type2 a b = lift_type_root $ Type_Type2 (Proxy::Proxy h2) a b
  71
  72 -- ** Type 'Host2_of'
  73 type family Host2_of px :: * -> * -> *
  74 type instance Host2_of (Proxy h2) = h2