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
  17 import Language.Symantic.Lib.Data.Peano
  18 import Language.Symantic.Lib.Data.Bool
  19 import Language.Symantic.Type.Root
  20 import Language.Symantic.Type.Alt
  21 import Language.Symantic.Type.Error
  22 import Language.Symantic.Type.Type0
  23
  24 -- * Type 'Type1'
  25 -- | A type of kind @(* -> *)@.
  26 data Type1 px (root:: * -> *) h where
  27         Type1 :: px -> root a -> Type1 px root ((Host1_of px) a)
  28
  29 type instance Root_of_Type      (Type1 px root) = root
  30 type instance Error_of_Type ast (Type1 px root) = No_Error_Type
  31
  32 instance -- Type0_Eq
  33  Type0_Eq root =>
  34  Type0_Eq (Type1 (Proxy h1) root) where
  35         type0_eq (Type1 _px1 a1) (Type1 _px2 a2)
  36          | Just Refl <- a1 `type0_eq` a2
  37          = Just Refl
  38         type0_eq _ _ = Nothing
  39 instance -- Type0_Eq
  40  Type0_Eq root =>
  41  Type0_Eq (Type1 EPeano root) where
  42         type0_eq (Type1 p1 a1)
  43                 (Type1 p2 a2)
  44          | p1 == p2
  45          , Just Refl <- a1 `type0_eq` a2
  46          = Just Refl
  47         type0_eq _ _ = Nothing
  48 instance -- Eq
  49  Type0_Eq root =>
  50  Eq (Type1 (Proxy h1) root h) where
  51         x == y = isJust $ type0_eq x y
  52 instance -- Eq
  53  Type0_Eq root =>
  54  Eq (Type1 EPeano root h) where
  55         x == y = isJust $ type0_eq x y
  56 instance -- Type1_Eq
  57  Type1_Eq (Type1 (Proxy t1) root) where
  58         type1_eq Type1{} Type1{} = Just Refl
  59 instance -- Show
  60  String_from_Type (Type1 px root) =>
  61  Show (Type1 px root h) where
  62         show = string_from_type
  63
  64 -- | Inject a 'Type1' within a root type.
  65 type1
  66  :: forall root h1 a.
  67  Type_Root_Lift (Type1 (Proxy h1)) root
  68  => root a -> root (h1 a)
  69 type1 = type_root_lift . Type1 (Proxy::Proxy h1)
  70
  71 -- ** Type family 'Host1_of'
  72 type family Host1_of px :: * -> *
  73 type instance Host1_of (Proxy h1) = h1
  74
  75 -- * Class 'Type1_Eq'
  76 -- | Test two type constructors for equality,
  77 -- returning an Haskell type-level proof
  78 -- of the equality when it holds.
  79 class Type1_Eq (ty:: * -> *) where
  80         type1_eq :: forall h1 h2 a1 a2. ty (h1 a1) -> ty (h2 a2) -> Maybe (h1 :~: h2)
  81         type1_eq = error "type1_eq"
  82 instance -- Type_Root
  83  Type1_Eq (ty (Type_Root ty)) =>
  84  Type1_Eq (Type_Root ty) where
  85         type1_eq (Type_Root x) (Type_Root y) = x `type1_eq` y
  86 instance -- Type_Alt
  87  ( Type1_Eq (curr root)
  88  , Type1_Eq (next root)
  89  ) => Type1_Eq (Type_Alt curr next root) where
  90         type1_eq (Type_Alt_Curr x) (Type_Alt_Curr y) = x `type1_eq` y
  91         type1_eq (Type_Alt_Next x) (Type_Alt_Next y) = x `type1_eq` y
  92         type1_eq _ _ = Nothing
  93 instance -- Type0 (Proxy h0)
  94  Type1_Eq (Type0 (Proxy h0) root)
  95
  96 -- * Class 'Type1_From'
  97 -- | Parse given @ast@ into a 'Root_of_Type' constructor,
  98 -- or return an 'Error_of_Type'.
  99 class Type1_From ast (ty:: * -> *) where
 100         type1_from
 101          :: Proxy ty
 102          -> ast
 103          -> (forall (h1:: * -> *). Proxy h1
 104                     -> (forall h. Root_of_Type ty h -> Root_of_Type ty (h1 h))
 105                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
 106          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
 107         default type1_from ::
 108          ( Error_Type_Lift (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 109          , IBool (Is_Last_Type ty (Root_of_Type ty))
 110          ) => Proxy ty
 111          -> ast
 112          -> (forall (h1:: * -> *). Proxy h1
 113                     -> (forall h. Root_of_Type ty h -> Root_of_Type ty (h1 h))
 114                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
 115          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
 116         type1_from ty ast _k =
 117                 Left $ error_type_unsupported ty ast
 118 instance -- Type_Root
 119  ( Type0_Eq (Type_Root ty)
 120  , Type1_From ast (ty (Type_Root ty))
 121  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 122  ) => Type1_From ast (Type_Root ty) where
 123         type1_from _ty = type1_from (Proxy::Proxy (ty (Type_Root ty)))
 124
 125 instance -- Type_Alt
 126  ( Type0_Eq (curr root)
 127  , Type1_From ast (curr root)
 128  , Type1_From ast (next root)
 129  , Root_of_Type (curr root) ~ root
 130  , Root_of_Type (next root) ~ root
 131  , Error_Type_Unlift (Error_Type ast) (Error_of_Type ast root)
 132  ) => Type1_From ast (Type_Alt curr next root) where
 133         type1_from _ty ast k =
 134                 case type1_from (Proxy::Proxy (curr root)) ast (\f ty -> Right $ k f ty) of
 135                  Right ret -> ret
 136                  Left err ->
 137                         case error_type_unlift err of
 138                          Just (Error_Type_Unsupported_here (_::ast)) ->
 139                                 type1_from (Proxy::Proxy (next root)) ast k
 140                          _ -> Left err
 141
 142 -- ** Type 'Type1_Lift'
 143 data Type1_Lift px root tys
 144  =   Type1_Lift (forall h. Type1 px root h -> tys root h)
 145
 146 -- ** Type 'Type1_Unlift'
 147 class Type1_Unlift ty where
 148         type1_unlift
 149          :: forall (root:: * -> *) ret h.
 150          ty root h
 151          -> (forall (px:: *).
 152              ( Type1 px root h
 153              , Type1_Lift px root ty
 154              ) -> Maybe ret)
 155          -> Maybe ret
 156 instance Type1_Unlift (Type0 px) where
 157         type1_unlift _ty _k = Nothing
 158 instance Type1_Unlift (Type1 px) where
 159         type1_unlift ty k = k (ty, Type1_Lift id)
 160 instance -- Type_Alt
 161  ( Type1_Unlift curr
 162  , Type1_Unlift next
 163  ) => Type1_Unlift (Type_Alt curr next) where
 164         type1_unlift (Type_Alt_Curr ty) k =
 165                 fromMaybe Nothing $ type1_unlift ty $ \(t, Type1_Lift l) ->
 166                         Just $ k (t, Type1_Lift $ Type_Alt_Curr . l)
 167         type1_unlift (Type_Alt_Next ty) k =
 168                 fromMaybe Nothing $ type1_unlift ty $ \(t, Type1_Lift l) ->
 169                         Just $ k (t, Type1_Lift $ Type_Alt_Next . l)
 170
 171 -- * Type 'Exists_Type1'
 172 -- | Existential data type wrapping the index of a 'Type1'.
 173 data Exists_Type1 ty
 174  = forall h. Exists_Type1 (ty h -> ty h)