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