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