Language/Symantic/Type/Family.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE ScopedTypeVariables #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7 {-# OPTIONS_GHC -fno-warn-orphans #-}
   8 -- | Type Families.
   9 module Language.Symantic.Type.Family where
  10
  11 import Data.Proxy (Proxy(..))
  12 import qualified Data.MonoTraversable as MT
  13
  14 import Language.Symantic.Type.Error
  15 import Language.Symantic.Type.Root
  16 import Language.Symantic.Type.Alt
  17
  18 -- * Type 'Host_of_Type0_Family'
  19 type family Host_of_Type0_Family tf h0 :: *
  20
  21 -- * Class 'Type0_Family'
  22 class Type0_Family (tf:: *) (ty:: * -> *) where
  23         type0_family
  24          :: forall h0. Proxy tf -> ty h0
  25          -> Maybe (Root_of_Type ty (Host_of_Type0_Family tf h0))
  26         type0_family _tf _ty = Nothing
  27 instance -- Type_Root
  28  ( Type0_Family tf (ty (Type_Root ty))
  29  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
  30  ) => Type0_Family tf (Type_Root ty) where
  31         type0_family tf (Type_Root ty) = type0_family tf ty
  32 instance -- Type_Alt
  33  ( Type0_Family tf (curr root)
  34  , Type0_Family tf (next root)
  35  , Root_of_Type (curr root) ~ root
  36  , Root_of_Type (next root) ~ root
  37  ) => Type0_Family tf (Type_Alt curr next root) where
  38         type0_family tf (Type_Alt_Curr ty) = type0_family tf ty
  39         type0_family tf (Type_Alt_Next ty) = type0_family tf ty
  40
  41 -- | Parsing utility to check that the resulting type
  42 -- from the application of a given type family to a given type
  43 -- is within the type stack,
  44 -- or raise 'Error_Type_No_Type0_Family'.
  45 check_type_type0_family
  46  :: forall ast ty tf h ret.
  47  ( Error_Type_Lift (Error_Type ast) (Error_of_Type ast ty)
  48  , Type0_Family tf ty
  49  , Root_of_Type ty ~ ty
  50  ) => Proxy tf -> ast -> ty h
  51  -> (ty (Host_of_Type0_Family tf h) -> Either (Error_of_Type ast ty) ret)
  52  -> Either (Error_of_Type ast ty) ret
  53 check_type_type0_family tf ast ty k =
  54         case type0_family tf ty of
  55          Just t -> k t
  56          Nothing -> Left $ error_type_lift $
  57                 Error_Type_No_Type_Family ast -- (Exists_Type0 ty)
  58
  59 -- * Type 'Type_Family_MonoElement'
  60 -- | Proxy type for 'MT.Element'.
  61 data Type_Family_MonoElement
  62 type instance Host_of_Type0_Family Type_Family_MonoElement h = MT.Element h