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
  18 import Language.Symantic.Lib.Data.Peano
  19 import Language.Symantic.Type.Root
  20 import Language.Symantic.Type.Alt
  21 import Language.Symantic.Type.Error
  22
  23 -- * Type 'Type0'
  24 -- | A type of kind @*@.
  25 data Type0 px (root:: * -> *) h where
  26         Type0 :: px -> Type0 px root (Host0_of px)
  27
  28 type instance Root_of_Type      (Type0 px root) = root
  29 type instance Error_of_Type ast (Type0 px root) = No_Error_Type
  30
  31 instance -- Type0_Eq
  32  Type0_Eq (Type0 (Proxy h0) root) where
  33         type0_eq Type0{} Type0{} = Just Refl
  34 instance -- Type0_Eq
  35  Type0_Eq (Type0 EPeano root) where
  36         type0_eq (Type0 p1) (Type0 p2) | p1 == p2 = Just Refl
  37         type0_eq _ _ = Nothing
  38 instance -- Eq
  39  Type0_Eq (Type0 px root) =>
  40  Eq (Type0 px root h) where
  41         x == y = isJust $ x `type0_eq` y
  42 instance -- Show
  43  String_from_Type (Type0 (Proxy h0) root) =>
  44  Show (Type0 (Proxy h0) root h0) where
  45         show = string_from_type
  46
  47 -- | Inject a 'Type0' within a root type.
  48 type0 :: Type_Root_Lift (Type0 (Proxy h0)) root => root h0
  49 type0 = type_root_lift (Type0 (Proxy::Proxy h0))
  50
  51 -- ** Type family 'Host0_of'
  52 type family Host0_of px :: *
  53 type instance Host0_of (Proxy h0) = h0
  54
  55 -- ** Type 'Type0_Lift'
  56 -- | Apply 'Peano_of_Type' on 'Type0_LiftP'.
  57 type Type0_Lift ty tys
  58  =   Type0_LiftP (Peano_of_Type ty tys) ty tys
  59 instance
  60  Type0_Lift ty root =>
  61  Type_Root_Lift ty (Type_Root root) where
  62         type_root_lift = Type_Root . type0_lift
  63
  64 -- *** Type 'Peano_of_Type'
  65 -- | Return a 'Peano' number derived from the location
  66 -- of a given type within a given type stack,
  67 -- which is used to avoid @OverlappingInstances@.
  68 type family Peano_of_Type
  69  (ty::  (* -> *) -> * -> *)
  70  (tys:: (* -> *) -> * -> *) :: * where
  71         Peano_of_Type ty    ty                   = Zero
  72         Peano_of_Type ty    (Type_Alt ty   next) = Zero
  73         Peano_of_Type other (Type_Alt curr next) = Succ (Peano_of_Type other next)
  74
  75 -- *** Class 'Type0_LiftP'
  76 -- | Lift a given type to the top of a given type stack including it,
  77 -- by constructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
  78 class Type0_LiftP (p:: *) ty tys where
  79         type0_liftP :: forall (root:: * -> *) h. Proxy p -> ty root h -> tys root h
  80 instance Type0_LiftP Zero curr curr where
  81         type0_liftP _ = id
  82 instance Type0_LiftP Zero curr (Type_Alt curr next) where
  83         type0_liftP _ = Type_Alt_Curr
  84 instance
  85  Type0_LiftP p other next =>
  86  Type0_LiftP (Succ p) other (Type_Alt curr next) where
  87         type0_liftP _ = Type_Alt_Next . type0_liftP (Proxy::Proxy p)
  88
  89 -- | Convenient wrapper around 'type0_liftP',
  90 -- passing it the 'Peano' number from 'Peano_of_Type'.
  91 type0_lift
  92  :: forall ty tys (root:: * -> *) h.
  93  Type0_Lift ty tys =>
  94  ty root h -> tys root h
  95 type0_lift = type0_liftP (Proxy::Proxy (Peano_of_Type ty tys))
  96
  97 -- ** Type 'Type0_Unlift'
  98 -- | Apply 'Peano_of_Type' on 'Type0_UnliftP'.
  99 type Type0_Unlift ty tys
 100  =   Type0_UnliftP (Peano_of_Type ty tys) ty tys
 101
 102 -- *** Class 'Type0_UnliftP'
 103 -- | Try to unlift a given type out of a given type stack including it,
 104 -- by deconstructing the appropriate sequence of 'Type_Alt_Curr' and 'Type_Alt_Next'.
 105 class Type0_UnliftP (p:: *) ty tys where
 106         type0_unliftP :: forall (root:: * -> *) h. Proxy p -> tys root h -> Maybe (ty root h)
 107 instance Type0_UnliftP Zero curr curr where
 108         type0_unliftP _ = Just
 109 instance Type0_UnliftP Zero curr (Type_Alt curr next) where
 110         type0_unliftP _ (Type_Alt_Curr x) = Just x
 111         type0_unliftP _ (Type_Alt_Next _) = Nothing
 112 instance
 113  Type0_UnliftP p other next =>
 114  Type0_UnliftP (Succ p) other (Type_Alt curr next) where
 115         type0_unliftP _ (Type_Alt_Next x) = type0_unliftP (Proxy::Proxy p) x
 116         type0_unliftP _ (Type_Alt_Curr _) = Nothing
 117
 118 -- | Convenient wrapper around 'type0_unliftP',
 119 -- passing it the 'Peano' number from 'Peano_of_Type'.
 120 type0_unlift
 121  :: forall ty tys (root:: * -> *) h.
 122  Type0_Unlift ty tys =>
 123  tys root h -> Maybe (ty root h)
 124 type0_unlift = type0_unliftP (Proxy::Proxy (Peano_of_Type ty tys))
 125
 126 -- * Class 'Type0_Eq'
 127 -- | Test two types for equality,
 128 -- returning an Haskell type-level proof
 129 -- of the equality when it holds.
 130 class Type0_Eq (ty:: * -> *) where
 131         type0_eq :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
 132 instance -- Type_Root
 133  Type0_Eq (ty (Type_Root ty)) =>
 134  Type0_Eq (Type_Root ty) where
 135         type0_eq (Type_Root x) (Type_Root y) = x `type0_eq` y
 136 instance -- Eq Type_Root
 137  Type0_Eq (Type_Root ty) =>
 138  Eq (Type_Root ty h) where
 139         x == y = isJust $ x `type0_eq` y
 140 instance -- Type_Alt
 141  ( Type0_Eq (curr root)
 142  , Type0_Eq (next root)
 143  ) => Type0_Eq (Type_Alt curr next root) where
 144         type0_eq (Type_Alt_Curr x) (Type_Alt_Curr y) = x `type0_eq` y
 145         type0_eq (Type_Alt_Next x) (Type_Alt_Next y) = x `type0_eq` y
 146         type0_eq _ _ = Nothing
 147 instance -- Eq Type_Alt
 148  ( Type0_Eq (curr root)
 149  , Type0_Eq (next root)
 150  ) => Eq (Type_Alt curr next root h) where
 151         x == y = isJust $ x `type0_eq` y
 152
 153 -- * Class 'Type0_From'
 154 -- | Parse given @ast@ into a 'Root_of_Type',
 155 -- or return an 'Error_of_Type'.
 156 --
 157 -- NOTE: making a distinction between @ty@ and 'Root_of_Type'@ ty@,
 158 -- instead of having only a @root@ variable
 159 -- is what enables to define many instances, one per type.
 160 class Type0_From ast (ty:: * -> *) where
 161         type0_from
 162          :: Proxy ty
 163          -> ast
 164          -> (forall h. Root_of_Type ty h
 165                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
 166          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
 167 instance -- Type_Root
 168  ( Type0_Eq (Type_Root ty)
 169  , Type0_From ast (ty (Type_Root ty))
 170  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 171  ) => Type0_From ast (Type_Root ty) where
 172         type0_from _ty = type0_from (Proxy::Proxy (ty (Type_Root ty)))
 173 instance -- Type_Alt
 174  ( Type0_Eq (curr root)
 175  , Type0_From ast (curr root)
 176  , Type0_From ast (next root)
 177  , Root_of_Type (curr root) ~ root
 178  , Root_of_Type (next root) ~ root
 179  , Error_Type_Unlift (Error_Type ast) (Error_of_Type ast root)
 180  ) => Type0_From ast (Type_Alt curr next root) where
 181         type0_from _ty ast k =
 182                 case type0_from (Proxy::Proxy (curr root)) ast (Right . k) of
 183                  Right ret -> ret
 184                  Left err ->
 185                         case error_type_unlift err of
 186                          Just (Error_Type_Unsupported_here (_::ast)) ->
 187                                 type0_from (Proxy::Proxy (next root)) ast k
 188                          _ -> Left err
 189
 190 -- * Class 'String_from_Type'
 191 -- | Return a 'String' from a type.
 192 class String_from_Type ty where
 193         string_from_type :: ty h -> String
 194 instance -- Type_Root
 195  String_from_Type (ty (Type_Root ty)) =>
 196  String_from_Type (Type_Root ty) where
 197         string_from_type (Type_Root ty) = string_from_type ty
 198 instance -- Show Type_Root
 199  String_from_Type (Type_Root ty) =>
 200  Show (Type_Root ty h) where
 201         show = string_from_type
 202 instance -- Type_Alt
 203  ( String_from_Type (curr root)
 204  , String_from_Type (next root)
 205  ) => String_from_Type (Type_Alt curr next root) where
 206         string_from_type (Type_Alt_Curr t) = string_from_type t
 207         string_from_type (Type_Alt_Next t) = string_from_type t
 208
 209 -- * Type 'Exists_Type0'
 210 -- | Existential data type wrapping the index of a 'Type0'.
 211 data Exists_Type0 ty
 212  = forall h. Exists_Type0 (ty h)
 213 instance -- Eq
 214  Type0_Eq ty =>
 215  Eq (Exists_Type0 ty) where
 216         Exists_Type0 xh == Exists_Type0 yh =
 217                 isJust $ xh `type0_eq` yh
 218 instance -- Show
 219  String_from_Type ty =>
 220  Show (Exists_Type0 ty) where
 221         show (Exists_Type0 ty) = string_from_type ty
 222
 223 -- * Type 'Exists_Type0_and_Repr'
 224 data Exists_Type0_and_Repr ty repr
 225  =   forall h.
 226      Exists_Type0_and_Repr (ty h) (repr h)