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 -- * Class 'Constraint_Type'
  65 -- | Test if a type satisfies a given 'Constraint',
  66 -- returning an Haskell type-level proof
  67 -- of that satisfaction when it holds.
  68 class Constraint_Type (c:: * -> Constraint) (ty:: * -> *) where
  69         constraint_type :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
  70         constraint_type _c _ = Nothing
  71 instance -- Type_Root
  72  Constraint_Type c (ty (Type_Root ty)) =>
  73  Constraint_Type c (Type_Root ty) where
  74         constraint_type c (Type_Root ty) = constraint_type c ty
  75 instance -- Type_Alt
  76  ( Constraint_Type c (curr root)
  77  , Constraint_Type c (next root)
  78  ) => Constraint_Type c (Type_Alt curr next root) where
  79         constraint_type c (Type_Alt_Curr ty) = constraint_type c ty
  80         constraint_type c (Type_Alt_Next ty) = constraint_type c ty
  81
  82 -- * Class 'Type_from'
  83 -- | Parse given @ast@ into a 'Root_of_Type',
  84 -- or return an 'Error_of_Type'.
  85 --
  86 -- NOTE: making a distinction between @ty@ and 'Root_of_Type'@ ty@,
  87 -- instead of having only a @root@ variable
  88 -- is what enables to define many instances, one per type.
  89 class Type_from ast (ty:: * -> *) where
  90         type_from
  91          :: Proxy ty
  92          -> ast
  93          -> (forall h. Root_of_Type ty h
  94                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
  95          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
  96 instance -- Type_Root
  97  ( Eq_Type (Type_Root ty)
  98  , Type_from ast (ty (Type_Root ty))
  99  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 100  ) => Type_from ast (Type_Root ty) where
 101         type_from _ty = type_from (Proxy::Proxy (ty (Type_Root ty)))
 102 instance -- Type_Alt
 103  ( Eq_Type (curr root)
 104  , Type_from ast (curr root)
 105  , Type_from ast (next root)
 106  , Root_of_Type (curr root) ~ root
 107  , Root_of_Type (next root) ~ root
 108  , Unlift_Error_Type (Error_Type ast) (Error_of_Type ast root)
 109  ) => Type_from ast (Type_Alt curr next root) where
 110         type_from _ty ast k =
 111                 case type_from (Proxy::Proxy (curr root)) ast (Right . k) of
 112                  Right ret -> ret
 113                  Left err ->
 114                         case unlift_error_type err of
 115                          Just (Error_Type_Unsupported_here (_::ast)) ->
 116                                 type_from (Proxy::Proxy (next root)) ast k
 117                          _ -> Left err
 118
 119 -- * Class 'String_from_Type'
 120 -- | Return a 'String' from a type.
 121 class String_from_Type ty where
 122         string_from_type :: ty h -> String
 123 instance -- Type_Root
 124  String_from_Type (ty (Type_Root ty)) =>
 125  String_from_Type (Type_Root ty) where
 126         string_from_type (Type_Root ty) = string_from_type ty
 127 instance -- Show Type_Root
 128  String_from_Type (Type_Root ty) =>
 129  Show (Type_Root ty h) where
 130         show = string_from_type
 131 instance -- Type_Alt
 132  ( String_from_Type (curr root)
 133  , String_from_Type (next root)
 134  ) => String_from_Type (Type_Alt curr next root) where
 135         string_from_type (Type_Alt_Curr t) = string_from_type t
 136         string_from_type (Type_Alt_Next t) = string_from_type t
 137
 138 -- * Type 'Type_Type0'
 139 -- | A type of kind @*@.
 140 data Type_Type0 px (root:: * -> *) h where
 141         Type_Type0 :: px -> Type_Type0 px root (Host0_of px)
 142
 143 type instance Root_of_Type      (Type_Type0 px root) = root
 144 type instance Error_of_Type ast (Type_Type0 px root) = No_Error_Type
 145
 146 instance -- Eq_Type
 147  Eq_Type (Type_Type0 (Proxy h0) root) where
 148         eq_type Type_Type0{} Type_Type0{} = Just Refl
 149 instance -- Eq_Type
 150  Eq_Type (Type_Type0 EPeano root) where
 151         eq_type (Type_Type0 p1)
 152                 (Type_Type0 p2)
 153          | p1 == p2
 154          = Just Refl
 155         eq_type _ _ = Nothing
 156 instance -- Eq
 157  Eq_Type (Type_Type0 px root) =>
 158  Eq (Type_Type0 px root h) where
 159         x == y = isJust $ x `eq_type` y
 160 instance -- Show
 161  String_from_Type (Type_Type0 (Proxy h0) root) =>
 162  Show (Type_Type0 (Proxy h0) root h0) where
 163         show = string_from_type
 164 instance Eq h0 => Constraint_Type Eq (Type_Type0 (Proxy h0) root) where
 165         constraint_type _c Type_Type0{} = Just Dict
 166 instance Ord h0 => Constraint_Type Ord (Type_Type0 (Proxy h0) root) where
 167         constraint_type _c Type_Type0{} = Just Dict
 168
 169 -- | Convenient alias to include a 'Type_Type0' within a type.
 170 type_type0 :: forall root h0. Lift_Type_Root (Type_Type0 (Proxy h0)) root => root h0
 171 type_type0 = lift_type_root (Type_Type0 (Proxy::Proxy h0))
 172
 173 -- ** Type family 'Host0_of'
 174 type family Host0_of px :: *
 175 type instance Host0_of (Proxy h0) = h0
 176
 177 -- ** Type 'Lift_Type'
 178 -- | Apply 'Peano_of_Type' on 'Lift_TypeP'.
 179 type Lift_Type ty tys
 180  =   Lift_TypeP (Peano_of_Type ty tys) ty tys
 181 instance
 182  Lift_Type ty root =>
 183  Lift_Type_Root ty (Type_Root root) where
 184         lift_type_root = Type_Root . lift_type
 185
 186 -- *** Type 'Peano_of_Type'
 187 -- | Return a 'Peano' number derived from the location
 188 -- of a given type within a given type stack,
 189 -- which is used to avoid @OverlappingInstances@.
 190 type family Peano_of_Type
 191  (ty::  (* -> *) -> * -> *)
 192  (tys:: (* -> *) -> * -> *) :: * where
 193         Peano_of_Type ty    ty                   = Zero
 194         Peano_of_Type ty    (Type_Alt ty   next) = Zero
 195         Peano_of_Type other (Type_Alt curr next) = Succ (Peano_of_Type other next)
 196
 197 -- *** Class 'Lift_TypeP'
 198 -- | Lift a given type to the top of a given type stack including it,
 199 -- by constructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 200 class Lift_TypeP (p:: *) ty tys where
 201         lift_typeP :: forall (root:: * -> *) h. Proxy p -> ty root h -> tys root h
 202 instance Lift_TypeP Zero curr curr where
 203         lift_typeP _ = id
 204 instance Lift_TypeP Zero curr (Type_Alt curr next) where
 205         lift_typeP _ = Type_Alt_Curr
 206 instance
 207  Lift_TypeP p other next =>
 208  Lift_TypeP (Succ p) other (Type_Alt curr next) where
 209         lift_typeP _ = Type_Alt_Next . lift_typeP (Proxy::Proxy p)
 210
 211 -- | Convenient wrapper around 'lift_typeP',
 212 -- passing it the 'Peano' number from 'Peano_of_Type'.
 213 lift_type
 214  :: forall ty tys (root:: * -> *) h.
 215  Lift_Type ty tys =>
 216  ty root h -> tys root h
 217 lift_type = lift_typeP (Proxy::Proxy (Peano_of_Type ty tys))
 218
 219 -- ** Type 'Unlift_Type'
 220 -- | Apply 'Peano_of_Type' on 'Unlift_TypeP'.
 221 type Unlift_Type ty tys
 222  =   Unlift_TypeP (Peano_of_Type ty tys) ty tys
 223
 224 -- *** Class 'Unlift_TypeP'
 225 -- | Try to unlift a given type out of a given type stack including it,
 226 -- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 227 class Unlift_TypeP (p:: *) ty tys where
 228         type_unliftN :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
 229 instance Unlift_TypeP Zero curr curr where
 230         type_unliftN _ = Just
 231 instance Unlift_TypeP Zero curr (Type_Alt curr next) where
 232         type_unliftN _ (Type_Alt_Curr x) = Just x
 233         type_unliftN _ (Type_Alt_Next _) = Nothing
 234 instance
 235  Unlift_TypeP p other next =>
 236  Unlift_TypeP (Succ p) other (Type_Alt curr next) where
 237         type_unliftN _ (Type_Alt_Next x) = type_unliftN (Proxy::Proxy p) x
 238         type_unliftN _ (Type_Alt_Curr _) = Nothing
 239
 240 -- | Convenient wrapper around 'type_unliftN',
 241 -- passing it the 'Peano' number from 'Peano_of_Type'.
 242 unlift_type
 243  :: forall ty tys (root:: * -> *) h.
 244  Unlift_Type ty tys =>
 245  tys root h -> Maybe (ty root h)
 246 unlift_type = type_unliftN (Proxy::Proxy (Peano_of_Type ty tys))
 247
 248 -- * Type 'Exists_Type'
 249 -- | Existential data type wrapping the index of a type.
 250 data Exists_Type ty
 251  = forall h. Exists_Type (ty h)
 252 instance -- Eq
 253  Eq_Type ty =>
 254  Eq (Exists_Type ty) where
 255         Exists_Type xh == Exists_Type yh =
 256                 isJust $ xh `eq_type` yh
 257 instance -- Show
 258  String_from_Type ty =>
 259  Show (Exists_Type ty) where
 260         show (Exists_Type ty) = string_from_type ty
 261
 262 -- * Type 'Exists_Type_and_Repr'
 263 data Exists_Type_and_Repr ty repr
 264  =   forall h.
 265      Exists_Type_and_Repr (ty h) (repr h)