Language/Symantic/Type/Type1.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE GADTs #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE Rank2Types #-}
   7 {-# LANGUAGE ScopedTypeVariables #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# LANGUAGE TypeOperators #-}
  10 {-# LANGUAGE UndecidableInstances #-}
  11 module Language.Symantic.Type.Type1 where
  12
  13 import Data.Maybe (isJust, fromMaybe)
  14 import Data.Proxy
  15 import Data.Type.Equality ((:~:)(Refl))
  16 import GHC.Prim (Constraint)
  17
  18 import Language.Symantic.Lib.Data.Peano
  19 import Language.Symantic.Lib.Data.Bool
  20 import Language.Symantic.Type.Root
  21 import Language.Symantic.Type.Alt
  22 import Language.Symantic.Type.Error
  23 import Language.Symantic.Type.Type0
  24
  25 -- * Type 'Type_Type1'
  26 -- | A type of kind @(k -> *)@.
  27 data Type_Type1 px (root:: * -> *) h where
  28         Type_Type1 :: px -> root a -> Type_Type1 px root ((Host1_of px) a)
  29 type instance Root_of_Type      (Type_Type1 px root) = root
  30 type instance Error_of_Type ast (Type_Type1 px root) = No_Error_Type
  31
  32 -- instance Constraint_Type Eq  (Type_Type1 (Proxy h1) root)
  33 instance Constraint_Type Ord (Type_Type1 (Proxy h1) root)
  34
  35 instance -- Eq_Type
  36  Eq_Type root =>
  37  Eq_Type (Type_Type1 (Proxy h1) root) where
  38         eq_type (Type_Type1 _px1 a1) (Type_Type1 _px2 a2)
  39          | Just Refl <- a1 `eq_type` a2
  40          = Just Refl
  41         eq_type _ _ = Nothing
  42 instance -- Eq_Type
  43  Eq_Type root =>
  44  Eq_Type (Type_Type1 EPeano root) where
  45         eq_type (Type_Type1 p1 a1)
  46                 (Type_Type1 p2 a2)
  47          | p1 == p2
  48          , Just Refl <- a1 `eq_type` a2
  49          = Just Refl
  50         eq_type _ _ = Nothing
  51 instance -- Eq
  52  Eq_Type root =>
  53  Eq (Type_Type1 (Proxy h1) root h) where
  54         x == y = isJust $ eq_type x y
  55 instance -- Eq
  56  Eq_Type root =>
  57  Eq (Type_Type1 EPeano root h) where
  58         x == y = isJust $ eq_type x y
  59 instance -- Eq_Type1
  60  Eq_Type1 (Type_Type1 (Proxy t1) root) where
  61         eq_type1 Type_Type1{} Type_Type1{}
  62          = Just Refl
  63 instance -- Show
  64  String_from_Type (Type_Type1 px root) =>
  65  Show (Type_Type1 px root h) where
  66         show = string_from_type
  67
  68 -- ** Type family 'Host1_of'
  69 type family Host1_of px :: * -> *
  70 type instance Host1_of (Proxy h1) = h1
  71
  72 -- * Class 'Eq_Type1'
  73 -- | Test two type constructors for equality,
  74 -- returning an Haskell type-level proof
  75 -- of the equality when it holds.
  76 class Eq_Type1 (ty:: * -> *) where
  77         eq_type1 :: forall h1 h2 a1 a2. ty (h1 a1) -> ty (h2 a2) -> Maybe (h1 :~: h2)
  78         eq_type1 = error "eq_type1"
  79 instance -- Type_Root
  80  Eq_Type1 (ty (Type_Root ty)) =>
  81  Eq_Type1 (Type_Root ty) where
  82         eq_type1 (Type_Root x) (Type_Root y) = x `eq_type1` y
  83 instance -- Type_Alt
  84  ( Eq_Type1 (curr root)
  85  , Eq_Type1 (next root)
  86  ) => Eq_Type1 (Type_Alt curr next root) where
  87         eq_type1 (Type_Alt_Curr x) (Type_Alt_Curr y) = x `eq_type1` y
  88         eq_type1 (Type_Alt_Next x) (Type_Alt_Next y) = x `eq_type1` y
  89         eq_type1 _ _ = Nothing
  90 instance -- Type_Type0 (Proxy h0)
  91  Eq_Type1 (Type_Type0 (Proxy h0) root)
  92
  93 -- * Class 'Constraint_Type1'
  94 -- | Test if a type constructor satisfies a given 'Constraint',
  95 -- returning an Haskell type-level proof
  96 -- of that satisfaction when it holds.
  97 class Constraint_Type1 (c:: (* -> *) -> Constraint) (ty:: * -> *) where
  98         constraint_type1 :: forall h1 h. Proxy c -> ty (h1 h) -> Maybe (Dict (c h1))
  99         constraint_type1 _c _ = Nothing
 100 instance -- Type_Root
 101  Constraint_Type1 c (ty (Type_Root ty)) =>
 102  Constraint_Type1 c (Type_Root ty) where
 103         constraint_type1 c (Type_Root ty) = constraint_type1 c ty
 104 instance -- Type_Alt
 105  ( Constraint_Type1 c (curr root)
 106  , Constraint_Type1 c (next root)
 107  ) => Constraint_Type1 c (Type_Alt curr next root) where
 108         constraint_type1 c (Type_Alt_Curr ty) = constraint_type1 c ty
 109         constraint_type1 c (Type_Alt_Next ty) = constraint_type1 c ty
 110 instance Constraint_Type1 c (Type_Type0 px root)
 111
 112 -- * Class 'Type1_from'
 113 -- | Parse given @ast@ into a 'Root_of_Type' constructor,
 114 -- or return an 'Error_of_Type'.
 115 class Type1_from ast (ty:: * -> *) where
 116         type1_from
 117          :: Proxy ty
 118          -> ast
 119          -> (forall (h1:: * -> *). Proxy h1
 120                     -> (forall h. Root_of_Type ty h -> Root_of_Type ty (h1 h))
 121                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
 122          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
 123         default type1_from ::
 124          ( Lift_Error_Type (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 125          , IBool (Is_Last_Type ty (Root_of_Type ty))
 126          ) => Proxy ty
 127          -> ast
 128          -> (forall (h1:: * -> *). Proxy h1
 129                     -> (forall h. Root_of_Type ty h -> Root_of_Type ty (h1 h))
 130                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
 131          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
 132         type1_from ty ast _k =
 133                 Left $ error_type_unsupported ty ast
 134 instance -- Type_Root
 135  ( Eq_Type (Type_Root ty)
 136  , Type1_from ast (ty (Type_Root ty))
 137  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 138  ) => Type1_from ast (Type_Root ty) where
 139         type1_from _ty = type1_from (Proxy::Proxy (ty (Type_Root ty)))
 140
 141 instance -- Type_Alt
 142  ( Eq_Type (curr root)
 143  , Type1_from ast (curr root)
 144  , Type1_from ast (next root)
 145  , Root_of_Type (curr root) ~ root
 146  , Root_of_Type (next root) ~ root
 147  , Unlift_Error_Type (Error_Type ast) (Error_of_Type ast root)
 148  ) => Type1_from ast (Type_Alt curr next root) where
 149         type1_from _ty ast k =
 150                 case type1_from (Proxy::Proxy (curr root)) ast (\f ty -> Right $ k f ty) of
 151                  Right ret -> ret
 152                  Left err ->
 153                         case unlift_error_type err of
 154                          Just (Error_Type_Unsupported_here (_::ast)) ->
 155                                 type1_from (Proxy::Proxy (next root)) ast k
 156                          _ -> Left err
 157
 158 -- ** Type 'Lift_Type1'
 159 data Lift_Type1 px root tys
 160  =   Lift_Type1 ( forall {-(root:: * -> *)-} h
 161                 . Type_Type1 px root h -> tys root h
 162                 )
 163
 164 -- ** Type 'Unlift_Type1'
 165 class Unlift_Type1 ty where
 166         unlift_type1
 167          :: forall (root:: * -> *) ret h.
 168          ty root h
 169          -> (forall (px:: *).
 170              ( Type_Type1 px root h
 171              , Lift_Type1 px root ty
 172              ) -> Maybe ret)
 173          -> Maybe ret
 174         unlift_type1 _ty _k = Nothing
 175 instance Unlift_Type1 (Type_Type1 px) where
 176         unlift_type1 ty k = k (ty, Lift_Type1 id)
 177 instance -- Type_Alt
 178  ( Unlift_Type1 curr
 179  , Unlift_Type1 next
 180  ) => Unlift_Type1 (Type_Alt curr next) where
 181         unlift_type1 (Type_Alt_Curr ty) k =
 182                 fromMaybe Nothing $ unlift_type1 ty $ \(t, Lift_Type1 l) ->
 183                         Just $ k (t, Lift_Type1 $ Type_Alt_Curr . l)
 184         unlift_type1 (Type_Alt_Next ty) k =
 185                 fromMaybe Nothing $ unlift_type1 ty $ \(t, Lift_Type1 l) ->
 186                         Just $ k (t, Lift_Type1 $ Type_Alt_Next . l)
 187 instance -- Type_Type0 px
 188  Unlift_Type1 (Type_Type0 px)
 189
 190 -- * Type 'Exists_Type1'
 191 -- | Existential data type wrapping the index of a type1.
 192 data Exists_Type1 ty
 193  = forall h. Exists_Type1 (ty h -> ty h)