Language/Symantic/Type/Type0.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   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 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12 module Language.Symantic.Type.Type0 where
  13
  14 import Data.Maybe (isJust)
  15 import Data.Proxy
  16 import Data.Type.Equality ((:~:)(Refl))
  17 import GHC.Prim (Constraint)
  18
  19 import Language.Symantic.Lib.Data.Peano
  20 import Language.Symantic.Type.Root
  21 import Language.Symantic.Type.Alt
  22 import Language.Symantic.Type.Error
  23
  24 -- * Type 'Dict'
  25 -- | 'Dict' captures the dictionary of a 'Constraint':
  26 -- pattern matching on the 'Dict' constructor
  27 -- brings the 'Constraint' into scope.
  28 data Dict :: Constraint -> * where
  29         Dict :: c => Dict c
  30
  31 -- * Type 'No_Type'
  32 -- | A discarded type.
  33 data No_Type (root:: * -> *) h
  34  =   No_Type (root h)
  35  deriving (Eq, Show)
  36
  37 -- * Class 'Eq_Type'
  38 -- | Test two types for equality,
  39 -- returning an Haskell type-level proof
  40 -- of the equality when it holds.
  41 class Eq_Type (ty:: * -> *) where
  42         eq_type :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
  43 instance -- Type_Root
  44  Eq_Type (ty (Type_Root ty)) =>
  45  Eq_Type (Type_Root ty) where
  46         eq_type (Type_Root x) (Type_Root y) = x `eq_type` y
  47 instance -- Eq Type_Root
  48  Eq_Type (Type_Root ty) =>
  49  Eq (Type_Root ty h) where
  50         x == y = isJust $ x `eq_type` y
  51 instance -- Type_Alt
  52  ( Eq_Type (curr root)
  53  , Eq_Type (next root)
  54  ) => Eq_Type (Type_Alt curr next root) where
  55         eq_type (Type_Alt_Curr x) (Type_Alt_Curr y) = x `eq_type` y
  56         eq_type (Type_Alt_Next x) (Type_Alt_Next y) = x `eq_type` y
  57         eq_type _ _ = Nothing
  58 instance -- Eq Type_Alt
  59  ( Eq_Type (curr root)
  60  , Eq_Type (next root)
  61  ) => Eq (Type_Alt curr next root h) where
  62         x == y = isJust $ x `eq_type` y
  63
  64 -- * Type 'Host_of_TypeFamily'
  65 type family Host_of_TypeFamily ta h0 :: *
  66
  67 -- * Class 'TypeFamily'
  68 class TypeFamily (ta:: *) (ty:: * -> *) where
  69         typeFamily
  70          :: forall h0. Proxy ta -> ty h0
  71          -> Maybe (Root_of_Type ty (Host_of_TypeFamily ta h0))
  72         typeFamily _tf _ty = Nothing
  73 instance -- Type_Root
  74  ( TypeFamily ta (ty (Type_Root ty))
  75  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
  76  ) => TypeFamily ta (Type_Root ty) where
  77         typeFamily ta (Type_Root ty) = typeFamily ta ty
  78 instance -- Type_Alt
  79  ( TypeFamily ta (curr root)
  80  , TypeFamily ta (next root)
  81  , Root_of_Type (curr root) ~ root
  82  , Root_of_Type (next root) ~ root
  83  ) => TypeFamily ta (Type_Alt curr next root) where
  84         typeFamily ta (Type_Alt_Curr ty) = typeFamily ta ty
  85         typeFamily ta (Type_Alt_Next ty) = typeFamily ta ty
  86
  87 -- | Parsing utility to check that an associated type is supported,
  88 -- or raise 'Error_Type_Type_Associated_missing'.
  89 check_type_family
  90  :: forall ast ty ta h ret.
  91  ( Lift_Error_Type (Error_Type ast) (Error_of_Type ast ty)
  92  , TypeFamily ta ty
  93  , Root_of_Type ty ~ ty
  94  ) => Proxy ta -> ast -> ty h
  95  -> (ty (Host_of_TypeFamily ta h) -> Either (Error_of_Type ast ty) ret)
  96  -> Either (Error_of_Type ast ty) ret
  97 check_type_family ta ast ty k =
  98         case typeFamily ta ty of
  99          Just t -> k t
 100          Nothing -> Left $ lift_error_type $
 101                 Error_Type_No_TypeFamily ast -- (Exists_Type ty)
 102
 103 -- * Class 'Constraint_Type'
 104 -- | Test if a type satisfies a given 'Constraint',
 105 -- returning an Haskell type-level proof
 106 -- of that satisfaction when it holds.
 107 class Constraint_Type (c:: * -> Constraint) (ty:: * -> *) where
 108         constraint_type :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
 109         constraint_type _c _ = Nothing
 110 instance -- Type_Root
 111  Constraint_Type c (ty (Type_Root ty)) =>
 112  Constraint_Type c (Type_Root ty) where
 113         constraint_type c (Type_Root ty) = constraint_type c ty
 114 instance -- Type_Alt
 115  ( Constraint_Type c (curr root)
 116  , Constraint_Type c (next root)
 117  ) => Constraint_Type c (Type_Alt curr next root) where
 118         constraint_type c (Type_Alt_Curr ty) = constraint_type c ty
 119         constraint_type c (Type_Alt_Next ty) = constraint_type c ty
 120
 121 -- | Parsing utility to check that a type is an instance of a given 'Constraint',
 122 -- or raise 'Error_Type_Constraint_missing'.
 123 check_type_constraint
 124  :: forall ast c root ty h ret.
 125  ( root ~ Root_of_Type ty
 126  , Lift_Error_Type (Error_Type ast) (Error_of_Type ast root)
 127  , Constraint_Type c ty
 128  ) => Proxy c -> ast -> ty h
 129  -> (Dict (c h) -> Either (Error_of_Type ast root) ret)
 130  -> Either (Error_of_Type ast root) ret
 131 check_type_constraint c ast ty k =
 132         case constraint_type c ty of
 133          Just Dict -> k Dict
 134          Nothing -> Left $ lift_error_type $
 135                 Error_Type_Constraint_missing ast -- (Exists_Type ty_k)
 136
 137 -- * Class 'Type_from'
 138 -- | Parse given @ast@ into a 'Root_of_Type',
 139 -- or return an 'Error_of_Type'.
 140 --
 141 -- NOTE: making a distinction between @ty@ and 'Root_of_Type'@ ty@,
 142 -- instead of having only a @root@ variable
 143 -- is what enables to define many instances, one per type.
 144 class Type_from ast (ty:: * -> *) where
 145         type_from
 146          :: Proxy ty
 147          -> ast
 148          -> (forall h. Root_of_Type ty h
 149                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
 150          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
 151 instance -- Type_Root
 152  ( Eq_Type (Type_Root ty)
 153  , Type_from ast (ty (Type_Root ty))
 154  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 155  ) => Type_from ast (Type_Root ty) where
 156         type_from _ty = type_from (Proxy::Proxy (ty (Type_Root ty)))
 157 instance -- Type_Alt
 158  ( Eq_Type (curr root)
 159  , Type_from ast (curr root)
 160  , Type_from ast (next root)
 161  , Root_of_Type (curr root) ~ root
 162  , Root_of_Type (next root) ~ root
 163  , Unlift_Error_Type (Error_Type ast) (Error_of_Type ast root)
 164  ) => Type_from ast (Type_Alt curr next root) where
 165         type_from _ty ast k =
 166                 case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
 167                  Right ret -> ret
 168                  Left err ->
 169                         case unlift_error_type err of
 170                          Just (Error_Type_Unsupported_here (_::ast)) ->
 171                                 type_from (Proxy::Proxy (next root)) ast k
 172                          _ -> Left err
 173
 174 -- * Class 'String_from_Type'
 175 -- | Return a 'String' from a type.
 176 class String_from_Type ty where
 177         string_from_type :: ty h -> String
 178 instance -- Type_Root
 179  String_from_Type (ty (Type_Root ty)) =>
 180  String_from_Type (Type_Root ty) where
 181         string_from_type (Type_Root ty) = string_from_type ty
 182 instance -- Show Type_Root
 183  String_from_Type (Type_Root ty) =>
 184  Show (Type_Root ty h) where
 185         show = string_from_type
 186 instance -- Type_Alt
 187  ( String_from_Type (curr root)
 188  , String_from_Type (next root)
 189  ) => String_from_Type (Type_Alt curr next root) where
 190         string_from_type (Type_Alt_Curr t) = string_from_type t
 191         string_from_type (Type_Alt_Next t) = string_from_type t
 192
 193 -- * Type 'Type_Type0'
 194 -- | A type of kind @*@.
 195 data Type_Type0 px (root:: * -> *) h where
 196         Type_Type0 :: px -> Type_Type0 px root (Host0_of px)
 197
 198 type instance Root_of_Type      (Type_Type0 px root) = root
 199 type instance Error_of_Type ast (Type_Type0 px root) = No_Error_Type
 200
 201 instance -- Eq_Type
 202  Eq_Type (Type_Type0 (Proxy h0) root) where
 203         eq_type Type_Type0{} Type_Type0{} = Just Refl
 204 instance -- Eq_Type
 205  Eq_Type (Type_Type0 EPeano root) where
 206         eq_type (Type_Type0 p1)
 207                 (Type_Type0 p2)
 208          | p1 == p2
 209          = Just Refl
 210         eq_type _ _ = Nothing
 211 instance -- Eq
 212  Eq_Type (Type_Type0 px root) =>
 213  Eq (Type_Type0 px root h) where
 214         x == y = isJust $ x `eq_type` y
 215 instance -- Show
 216  String_from_Type (Type_Type0 (Proxy h0) root) =>
 217  Show (Type_Type0 (Proxy h0) root h0) where
 218         show = string_from_type
 219
 220 -- | Inject a 'Type_Type0' within a root type.
 221 type_type0 :: Lift_Type_Root (Type_Type0 (Proxy h0)) root => root h0
 222 type_type0 = lift_type_root (Type_Type0 (Proxy::Proxy h0))
 223
 224 -- ** Type family 'Host0_of'
 225 type family Host0_of px :: *
 226 type instance Host0_of (Proxy h0) = h0
 227
 228 -- ** Type 'Lift_Type'
 229 -- | Apply 'Peano_of_Type' on 'Lift_TypeP'.
 230 type Lift_Type ty tys
 231  =   Lift_TypeP (Peano_of_Type ty tys) ty tys
 232 instance
 233  Lift_Type ty root =>
 234  Lift_Type_Root ty (Type_Root root) where
 235         lift_type_root = Type_Root . lift_type
 236
 237 -- *** Type 'Peano_of_Type'
 238 -- | Return a 'Peano' number derived from the location
 239 -- of a given type within a given type stack,
 240 -- which is used to avoid @OverlappingInstances@.
 241 type family Peano_of_Type
 242  (ty::  (* -> *) -> * -> *)
 243  (tys:: (* -> *) -> * -> *) :: * where
 244         Peano_of_Type ty    ty                   = Zero
 245         Peano_of_Type ty    (Type_Alt ty   next) = Zero
 246         Peano_of_Type other (Type_Alt curr next) = Succ (Peano_of_Type other next)
 247
 248 -- *** Class 'Lift_TypeP'
 249 -- | Lift a given type to the top of a given type stack including it,
 250 -- by constructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 251 class Lift_TypeP (p:: *) ty tys where
 252         lift_typeP :: forall (root:: * -> *) h. Proxy p -> ty root h -> tys root h
 253 instance Lift_TypeP Zero curr curr where
 254         lift_typeP _ = id
 255 instance Lift_TypeP Zero curr (Type_Alt curr next) where
 256         lift_typeP _ = Type_Alt_Curr
 257 instance
 258  Lift_TypeP p other next =>
 259  Lift_TypeP (Succ p) other (Type_Alt curr next) where
 260         lift_typeP _ = Type_Alt_Next . lift_typeP (Proxy::Proxy p)
 261
 262 -- | Convenient wrapper around 'lift_typeP',
 263 -- passing it the 'Peano' number from 'Peano_of_Type'.
 264 lift_type
 265  :: forall ty tys (root:: * -> *) h.
 266  Lift_Type ty tys =>
 267  ty root h -> tys root h
 268 lift_type = lift_typeP (Proxy::Proxy (Peano_of_Type ty tys))
 269
 270 -- ** Type 'Unlift_Type'
 271 -- | Apply 'Peano_of_Type' on 'Unlift_TypeP'.
 272 type Unlift_Type ty tys
 273  =   Unlift_TypeP (Peano_of_Type ty tys) ty tys
 274
 275 -- *** Class 'Unlift_TypeP'
 276 -- | Try to unlift a given type out of a given type stack including it,
 277 -- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 278 class Unlift_TypeP (p:: *) ty tys where
 279         type_unliftN :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
 280 instance Unlift_TypeP Zero curr curr where
 281         type_unliftN _ = Just
 282 instance Unlift_TypeP Zero curr (Type_Alt curr next) where
 283         type_unliftN _ (Type_Alt_Curr x) = Just x
 284         type_unliftN _ (Type_Alt_Next _) = Nothing
 285 instance
 286  Unlift_TypeP p other next =>
 287  Unlift_TypeP (Succ p) other (Type_Alt curr next) where
 288         type_unliftN _ (Type_Alt_Next x) = type_unliftN (Proxy::Proxy p) x
 289         type_unliftN _ (Type_Alt_Curr _) = Nothing
 290
 291 -- | Convenient wrapper around 'type_unliftN',
 292 -- passing it the 'Peano' number from 'Peano_of_Type'.
 293 unlift_type
 294  :: forall ty tys (root:: * -> *) h.
 295  Unlift_Type ty tys =>
 296  tys root h -> Maybe (ty root h)
 297 unlift_type = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 298
 299 -- * Type 'Exists_Type'
 300 -- | Existential data type wrapping the index of a type.
 301 data Exists_Type ty
 302  = forall h. Exists_Type (ty h)
 303 instance -- Eq
 304  Eq_Type ty =>
 305  Eq (Exists_Type ty) where
 306         Exists_Type xh == Exists_Type yh =
 307                 isJust $ xh `eq_type` yh
 308 instance -- Show
 309  String_from_Type ty =>
 310  Show (Exists_Type ty) where
 311         show (Exists_Type ty) = string_from_type ty
 312
 313 -- * Type 'Exists_Type_and_Repr'
 314 data Exists_Type_and_Repr ty repr
 315  =   forall h.
 316      Exists_Type_and_Repr (ty h) (repr h)