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
 111 -- * Class 'Type1_from'
 112 -- | Parse given @ast@ into a 'Root_of_Type' constructor,
 113 -- or return an 'Error_of_Type'.
 114 class Type1_from ast (ty:: * -> *) where
 115         type1_from
 116          :: Proxy ty
 117          -> ast
 118          -> (forall (h1:: * -> *). Proxy h1
 119                     -> (forall h. Root_of_Type ty h -> Root_of_Type ty (h1 h))
 120                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
 121          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
 122         default type1_from ::
 123          ( Lift_Error_Type (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 124          , Implicit_HBool (Is_Last_Type ty (Root_of_Type ty))
 125          ) => Proxy ty
 126          -> ast
 127          -> (forall (h1:: * -> *). Proxy h1
 128                     -> (forall h. Root_of_Type ty h -> Root_of_Type ty (h1 h))
 129                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
 130          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
 131         type1_from ty ast _k =
 132                 Left $ error_type_unsupported ty ast
 133 instance -- Type_Root
 134  ( Eq_Type (Type_Root ty)
 135  , Type1_from ast (ty (Type_Root ty))
 136  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 137  ) => Type1_from ast (Type_Root ty) where
 138         type1_from _ty = type1_from (Proxy::Proxy (ty (Type_Root ty)))
 139
 140 instance -- Type_Alt
 141  ( Eq_Type (curr root)
 142  , Type1_from ast (curr root)
 143  , Type1_from ast (next root)
 144  , Root_of_Type (curr root) ~ root
 145  , Root_of_Type (next root) ~ root
 146  , Unlift_Error_Type (Error_Type ast) (Error_of_Type ast root)
 147  ) => Type1_from ast (Type_Alt curr next root) where
 148         type1_from _ty ast k =
 149                 case type1_from (Proxy::Proxy (curr root)) ast (\f ty -> Right $ k f ty) of
 150                  Right ret -> ret
 151                  Left err ->
 152                         case unlift_error_type err of
 153                          Just (Error_Type_Unsupported_here (_::ast)) ->
 154                                 type1_from (Proxy::Proxy (next root)) ast k
 155                          _ -> Left err
 156
 157 -- ** Type 'Lift_Type1'
 158 data Lift_Type1 px tys
 159  =   Lift_Type1 ( forall (root:: * -> *) h
 160                 . Type_Type1 px root h -> tys root h
 161                 )
 162
 163 -- ** Type 'Unlift_Type1'
 164 class Unlift_Type1 ty where
 165         unlift_type1
 166          :: forall (root:: * -> *) ret h.
 167          ty root h
 168          -> (forall (px:: *).
 169              ( Type_Type1 px root h
 170              , Lift_Type1 px ty
 171              ) -> Maybe ret)
 172          -> Maybe ret
 173         unlift_type1 _ty _k = Nothing
 174 instance Unlift_Type1 (Type_Type1 px) where
 175         unlift_type1 ty k = k (ty, Lift_Type1 id)
 176 instance -- Type_Alt
 177  ( Unlift_Type1 curr
 178  , Unlift_Type1 next
 179  ) => Unlift_Type1 (Type_Alt curr next) where
 180         unlift_type1 (Type_Alt_Curr ty) k =
 181                 fromMaybe Nothing $ unlift_type1 ty $ \(t, Lift_Type1 l) ->
 182                         Just $ k (t, Lift_Type1 $ Type_Alt_Curr . l)
 183         unlift_type1 (Type_Alt_Next ty) k =
 184                 fromMaybe Nothing $ unlift_type1 ty $ \(t, Lift_Type1 l) ->
 185                         Just $ k (t, Lift_Type1 $ Type_Alt_Next . l)
 186 instance -- Type_Type0 px
 187  Unlift_Type1 (Type_Type0 px)
 188
 189 -- * Type 'Exists_Type1'
 190 -- | Existential data type wrapping the index of a type1.
 191 data Exists_Type1 ty
 192  = forall h. Exists_Type1 (ty h -> ty h)