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 import GHC.Prim (Constraint)
  17
  18 import Language.Symantic.Lib.Data.Peano
  19 import Language.Symantic.Lib.Data.Bool
  20 import Language.Symantic.Type.Root
  21 import Language.Symantic.Type.Alt
  22 import Language.Symantic.Type.Error
  23 import Language.Symantic.Type.Type0
  24
  25 -- * Type 'Type_Type1'
  26 -- | A type of kind @(k -> *)@.
  27 data Type_Type1 px (root:: * -> *) h where
  28         Type_Type1 :: px -> root a -> Type_Type1 px root ((Host1_of px) a)
  29
  30 type instance Root_of_Type      (Type_Type1 px root) = root
  31 type instance Error_of_Type ast (Type_Type1 px root) = No_Error_Type
  32
  33 instance -- Eq_Type
  34  Eq_Type root =>
  35  Eq_Type (Type_Type1 (Proxy h1) root) where
  36         eq_type (Type_Type1 _px1 a1) (Type_Type1 _px2 a2)
  37          | Just Refl <- a1 `eq_type` a2
  38          = Just Refl
  39         eq_type _ _ = Nothing
  40 instance -- Eq_Type
  41  Eq_Type root =>
  42  Eq_Type (Type_Type1 EPeano root) where
  43         eq_type (Type_Type1 p1 a1)
  44                 (Type_Type1 p2 a2)
  45          | p1 == p2
  46          , Just Refl <- a1 `eq_type` a2
  47          = Just Refl
  48         eq_type _ _ = Nothing
  49 instance -- Eq
  50  Eq_Type root =>
  51  Eq (Type_Type1 (Proxy h1) root h) where
  52         x == y = isJust $ eq_type x y
  53 instance -- Eq
  54  Eq_Type root =>
  55  Eq (Type_Type1 EPeano root h) where
  56         x == y = isJust $ eq_type x y
  57 instance -- Eq_Type1
  58  Eq_Type1 (Type_Type1 (Proxy t1) root) where
  59         eq_type1 Type_Type1{} Type_Type1{}
  60          = Just Refl
  61 instance -- Show
  62  String_from_Type (Type_Type1 px root) =>
  63  Show (Type_Type1 px root h) where
  64         show = string_from_type
  65
  66 -- | Inject a 'Type_Type1' within a root type.
  67 type_type1
  68  :: forall root h1 a.
  69  Lift_Type_Root (Type_Type1 (Proxy h1)) root
  70  => root a -> root (h1 a)
  71 type_type1 = lift_type_root . Type_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 'Eq_Type1'
  78 -- | Test two type constructors for equality,
  79 -- returning an Haskell type-level proof
  80 -- of the equality when it holds.
  81 class Eq_Type1 (ty:: * -> *) where
  82         eq_type1 :: forall h1 h2 a1 a2. ty (h1 a1) -> ty (h2 a2) -> Maybe (h1 :~: h2)
  83         eq_type1 = error "eq_type1"
  84 instance -- Type_Root
  85  Eq_Type1 (ty (Type_Root ty)) =>
  86  Eq_Type1 (Type_Root ty) where
  87         eq_type1 (Type_Root x) (Type_Root y) = x `eq_type1` y
  88 instance -- Type_Alt
  89  ( Eq_Type1 (curr root)
  90  , Eq_Type1 (next root)
  91  ) => Eq_Type1 (Type_Alt curr next root) where
  92         eq_type1 (Type_Alt_Curr x) (Type_Alt_Curr y) = x `eq_type1` y
  93         eq_type1 (Type_Alt_Next x) (Type_Alt_Next y) = x `eq_type1` y
  94         eq_type1 _ _ = Nothing
  95 instance -- Type_Type0 (Proxy h0)
  96  Eq_Type1 (Type_Type0 (Proxy h0) root)
  97
  98 -- * Class 'Constraint_Type1'
  99 -- | Test if a type constructor satisfies a given 'Constraint',
 100 -- returning an Haskell type-level proof
 101 -- of that satisfaction when it holds.
 102 class Constraint_Type1 (c:: (* -> *) -> Constraint) (ty:: * -> *) where
 103         constraint_type1 :: forall h1 h. Proxy c -> ty (h1 h) -> Maybe (Dict (c h1))
 104         constraint_type1 _c _ = Nothing
 105 instance -- Type_Root
 106  Constraint_Type1 c (ty (Type_Root ty)) =>
 107  Constraint_Type1 c (Type_Root ty) where
 108         constraint_type1 c (Type_Root ty) = constraint_type1 c ty
 109 instance -- Type_Alt
 110  ( Constraint_Type1 c (curr root)
 111  , Constraint_Type1 c (next root)
 112  ) => Constraint_Type1 c (Type_Alt curr next root) where
 113         constraint_type1 c (Type_Alt_Curr ty) = constraint_type1 c ty
 114         constraint_type1 c (Type_Alt_Next ty) = constraint_type1 c ty
 115 instance Constraint_Type1 c (Type_Type0 px root)
 116
 117 -- * Class 'Type1_from'
 118 -- | Parse given @ast@ into a 'Root_of_Type' constructor,
 119 -- or return an 'Error_of_Type'.
 120 class Type1_from ast (ty:: * -> *) where
 121         type1_from
 122          :: Proxy ty
 123          -> ast
 124          -> (forall (h1:: * -> *). Proxy h1
 125                     -> (forall h. Root_of_Type ty h -> Root_of_Type ty (h1 h))
 126                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
 127          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
 128         default type1_from ::
 129          ( Lift_Error_Type (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 130          , IBool (Is_Last_Type ty (Root_of_Type ty))
 131          ) => Proxy ty
 132          -> ast
 133          -> (forall (h1:: * -> *). Proxy h1
 134                     -> (forall h. Root_of_Type ty h -> Root_of_Type ty (h1 h))
 135                     -> Either (Error_of_Type ast (Root_of_Type ty)) ret)
 136          ->            Either (Error_of_Type ast (Root_of_Type ty)) ret
 137         type1_from ty ast _k =
 138                 Left $ error_type_unsupported ty ast
 139 instance -- Type_Root
 140  ( Eq_Type (Type_Root ty)
 141  , Type1_from ast (ty (Type_Root ty))
 142  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
 143  ) => Type1_from ast (Type_Root ty) where
 144         type1_from _ty = type1_from (Proxy::Proxy (ty (Type_Root ty)))
 145
 146 instance -- Type_Alt
 147  ( Eq_Type (curr root)
 148  , Type1_from ast (curr root)
 149  , Type1_from ast (next root)
 150  , Root_of_Type (curr root) ~ root
 151  , Root_of_Type (next root) ~ root
 152  , Unlift_Error_Type (Error_Type ast) (Error_of_Type ast root)
 153  ) => Type1_from ast (Type_Alt curr next root) where
 154         type1_from _ty ast k =
 155                 case type1_from (Proxy::Proxy (curr root)) ast (\f ty -> Right $ k f ty) of
 156                  Right ret -> ret
 157                  Left err ->
 158                         case unlift_error_type err of
 159                          Just (Error_Type_Unsupported_here (_::ast)) ->
 160                                 type1_from (Proxy::Proxy (next root)) ast k
 161                          _ -> Left err
 162
 163 -- ** Type 'Lift_Type1'
 164 data Lift_Type1 px root tys
 165  =   Lift_Type1 ( forall {-(root:: * -> *)-} h
 166                 . Type_Type1 px root h -> tys root h
 167                 )
 168
 169 -- ** Type 'Unlift_Type1'
 170 class Unlift_Type1 ty where
 171         unlift_type1
 172          :: forall (root:: * -> *) ret h.
 173          ty root h
 174          -> (forall (px:: *).
 175              ( Type_Type1 px root h
 176              , Lift_Type1 px root ty
 177              ) -> Maybe ret)
 178          -> Maybe ret
 179         unlift_type1 _ty _k = Nothing
 180 instance Unlift_Type1 (Type_Type1 px) where
 181         unlift_type1 ty k = k (ty, Lift_Type1 id)
 182 instance -- Type_Alt
 183  ( Unlift_Type1 curr
 184  , Unlift_Type1 next
 185  ) => Unlift_Type1 (Type_Alt curr next) where
 186         unlift_type1 (Type_Alt_Curr ty) k =
 187                 fromMaybe Nothing $ unlift_type1 ty $ \(t, Lift_Type1 l) ->
 188                         Just $ k (t, Lift_Type1 $ Type_Alt_Curr . l)
 189         unlift_type1 (Type_Alt_Next ty) k =
 190                 fromMaybe Nothing $ unlift_type1 ty $ \(t, Lift_Type1 l) ->
 191                         Just $ k (t, Lift_Type1 $ Type_Alt_Next . l)
 192 instance -- Type_Type0 px
 193  Unlift_Type1 (Type_Type0 px)
 194
 195 -- * Type 'Exists_Type1'
 196 -- | Existential data type wrapping the index of a type1.
 197 data Exists_Type1 ty
 198  = forall h. Exists_Type1 (ty h -> ty h)