Language/Symantic/Type/Type2.hs

   1 {-# LANGUAGE FlexibleInstances #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE ScopedTypeVariables #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7 module Language.Symantic.Type.Type2 where
   8
   9 import Data.Maybe (isJust)
  10 import Data.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import GHC.Prim (Constraint)
  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          :: (Constraint2_of px) a b
  26          => px -> root a -> root b
  27          -> Type_Type2 px root ((Host2_of px) a b)
  28 class Constraint2_Empty a b
  29 instance Constraint2_Empty a b
  30
  31 type instance Root_of_Type      (Type_Type2 px root) = root
  32 type instance Error_of_Type ast (Type_Type2 px root) = No_Error_Type
  33
  34 instance -- Eq_Type
  35  Eq_Type root =>
  36  Eq_Type (Type_Type2 (Proxy h2) root) where
  37         eq_type
  38          (Type_Type2 _ arg1 res1)
  39          (Type_Type2 _ arg2 res2)
  40          | Just Refl <- arg1 `eq_type` arg2
  41          , Just Refl <- res1 `eq_type` res2
  42          = Just Refl
  43         eq_type _ _ = Nothing
  44 instance -- Eq_Type
  45  Eq_Type root =>
  46  Eq_Type (Type_Type2 EPeano root) where
  47         eq_type (Type_Type2 p1 arg1 res1)
  48                 (Type_Type2 p2 arg2 res2)
  49          | p1 == p2
  50          , Just Refl <- arg1 `eq_type` arg2
  51          , Just Refl <- res1 `eq_type` res2
  52          = Just Refl
  53         eq_type _ _ = Nothing
  54 instance -- Eq
  55  Eq_Type root =>
  56  Eq (Type_Type2 (Proxy h2) root h) where
  57         x == y = isJust $ x `eq_type` y
  58 instance -- Eq
  59  Eq_Type root =>
  60  Eq (Type_Type2 EPeano root h) where
  61         x == y = isJust $ x `eq_type` y
  62 instance -- Show
  63  ( String_from_Type root
  64  , String_from_Type (Type_Type2 px root)
  65  ) => Show (Type_Type2 px root h) where
  66         show = string_from_type
  67 instance Constraint_Type Eq  (Type_Type2 px root)
  68 instance Constraint_Type Ord (Type_Type2 px root)
  69 -- instance Unlift_Type1 (Type_Type2 px)  -- NOTE: done case by case
  70 instance Eq_Type1 (Type_Type2 px root) -- FIXME: should be doable
  71
  72 -- ** Type 'Host2_of'
  73 type family Host2_of px :: * -> * -> *
  74 type instance Host2_of (Proxy h2) = h2
  75
  76 -- ** Type 'Constraint2_of'
  77 type family Constraint2_of px :: (* -> * -> Constraint)