Language/Symantic/Type/Type1.hs

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