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 'Type2'
  23 -- | A type of kind @(* -> * -> *)@.
  24 data Type2 px (root:: * -> *) h where
  25         Type2 :: px -> root a -> root b
  26               -> Type2 px root ((Host2_of px) a b)
  27
  28 type instance Root_of_Type      (Type2 px root) = root
  29 type instance Error_of_Type ast (Type2 px root) = No_Error_Type
  30
  31 instance -- Type0_Eq
  32  Type0_Eq root =>
  33  Type0_Eq (Type2 (Proxy h2) root) where
  34         type0_eq
  35          (Type2 _ arg1 res1)
  36          (Type2 _ arg2 res2)
  37          | Just Refl <- arg1 `type0_eq` arg2
  38          , Just Refl <- res1 `type0_eq` res2
  39          = Just Refl
  40         type0_eq _ _ = Nothing
  41 instance -- Type0_Eq
  42  Type0_Eq root =>
  43  Type0_Eq (Type2 EPeano root) where
  44         type0_eq (Type2 p1 arg1 res1)
  45                 (Type2 p2 arg2 res2)
  46          | p1 == p2
  47          , Just Refl <- arg1 `type0_eq` arg2
  48          , Just Refl <- res1 `type0_eq` res2
  49          = Just Refl
  50         type0_eq _ _ = Nothing
  51 instance -- Eq
  52  Type0_Eq root =>
  53  Eq (Type2 (Proxy h2) root h) where
  54         x == y = isJust $ x `type0_eq` y
  55 instance -- Eq
  56  Type0_Eq root =>
  57  Eq (Type2 EPeano root h) where
  58         x == y = isJust $ x `type0_eq` y
  59 instance -- Show
  60  ( String_from_Type root
  61  , String_from_Type (Type2 px root)
  62  ) => Show (Type2 px root h) where
  63         show = string_from_type
  64
  65 -- | Inject a 'Type2' within a root type.
  66 type2
  67  :: forall root h2 a b.
  68  Type_Root_Lift (Type2 (Proxy h2)) root
  69  => root a -> root b -> root (h2 a b)
  70 type2 a b = type_root_lift $ 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