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 ta h0 :: *
  20
  21 -- * Type 'Type_Family_MonoElement'
  22 -- | Proxy type for 'MT.Element'.
  23 data Type_Family_MonoElement
  24 type instance Host_of_Type0_Family Type_Family_MonoElement h = MT.Element h
  25
  26 -- * Class 'Type0_Family'
  27 class Type0_Family (ta:: *) (ty:: * -> *) where
  28         type0_family
  29          :: forall h0. Proxy ta -> ty h0
  30          -> Maybe (Root_of_Type ty (Host_of_Type0_Family ta h0))
  31         type0_family _tf _ty = Nothing
  32 instance -- Type_Root
  33  ( Type0_Family ta (ty (Type_Root ty))
  34  , Root_of_Type (ty (Type_Root ty)) ~ Type_Root ty
  35  ) => Type0_Family ta (Type_Root ty) where
  36         type0_family ta (Type_Root ty) = type0_family ta ty
  37 instance -- Type_Alt
  38  ( Type0_Family ta (curr root)
  39  , Type0_Family ta (next root)
  40  , Root_of_Type (curr root) ~ root
  41  , Root_of_Type (next root) ~ root
  42  ) => Type0_Family ta (Type_Alt curr next root) where
  43         type0_family ta (Type_Alt_Curr ty) = type0_family ta ty
  44         type0_family ta (Type_Alt_Next ty) = type0_family ta ty
  45
  46 -- | Parsing utility to check that an associated type is supported,
  47 -- or raise 'Error_Type_No_Type0_Family'.
  48 check_type_type0_family
  49  :: forall ast ty ta h ret.
  50  ( Error_Type_Lift (Error_Type ast) (Error_of_Type ast ty)
  51  , Type0_Family ta ty
  52  , Root_of_Type ty ~ ty
  53  ) => Proxy ta -> ast -> ty h
  54  -> (ty (Host_of_Type0_Family ta h) -> Either (Error_of_Type ast ty) ret)
  55  -> Either (Error_of_Type ast ty) ret
  56 check_type_type0_family ta ast ty k =
  57         case type0_family ta ty of
  58          Just t -> k t
  59          Nothing -> Left $ error_type_lift $
  60                 Error_Type_No_Type_Family ast -- (Exists_Type0 ty)