Language/Symantic/Type/Type2.hs

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