Language/Symantic/Type/Constraint.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   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 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12 module Language.Symantic.Type.Constraint where
  13
  14 import Data.Proxy
  15 import GHC.Prim (Constraint)
  16
  17 import Language.Symantic.Type.Root
  18 import Language.Symantic.Type.Alt
  19 import Language.Symantic.Type.Error
  20 import Language.Symantic.Type.Type0
  21
  22 -- * Type 'Dict'
  23 -- | 'Dict' captures the dictionary of a 'Constraint':
  24 -- pattern matching on the 'Dict' constructor
  25 -- brings the 'Constraint' into scope.
  26 data Dict :: Constraint -> * where
  27         Dict :: c => Dict c
  28
  29 -- * Class 'Type0_Constraint'
  30 -- | Test if a type satisfies a given 'Constraint',
  31 -- returning an Haskell type-level proof
  32 -- of that satisfaction when it holds.
  33 class Type0_Constraint (c:: * -> Constraint) (ty:: * -> *) where
  34         type0_constraint :: forall h. Proxy c -> ty h -> Maybe (Dict (c h))
  35         type0_constraint _c _ = Nothing
  36 instance -- Type_Root
  37  Type0_Constraint c (ty (Type_Root ty)) =>
  38  Type0_Constraint c (Type_Root ty) where
  39         type0_constraint c (Type_Root ty) = type0_constraint c ty
  40 instance -- Type_Alt
  41  ( Type0_Constraint c (curr root)
  42  , Type0_Constraint c (next root)
  43  ) => Type0_Constraint c (Type_Alt curr next root) where
  44         type0_constraint c (Type_Alt_Curr ty) = type0_constraint c ty
  45         type0_constraint c (Type_Alt_Next ty) = type0_constraint c ty
  46
  47 -- | Parsing utility to check that a type is an instance of a given 'Constraint',
  48 -- or raise 'Error_Type_Constraint_missing'.
  49 check_type_type0_constraint
  50  :: forall ast c root ty h ret.
  51  ( root ~ Root_of_Type ty
  52  , Error_Type_Lift (Error_Type ast) (Error_of_Type ast root)
  53  , Type0_Constraint c ty
  54  ) => Proxy c -> ast -> ty h
  55  -> (Dict (c h) -> Either (Error_of_Type ast root) ret)
  56  -> Either (Error_of_Type ast root) ret
  57 check_type_type0_constraint c ast ty k =
  58         case type0_constraint c ty of
  59          Just Dict -> k Dict
  60          Nothing -> Left $ error_type_lift $
  61                 Error_Type_Constraint_missing ast -- (Exists_Type0 ty_k)
  62
  63 -- * Class 'Type1_Constraint'
  64 -- | Test if a type constructor satisfies a given 'Constraint',
  65 -- returning an Haskell type-level proof
  66 -- of that satisfaction when it holds.
  67 class Type1_Constraint (c:: (* -> *) -> Constraint) (ty:: * -> *) where
  68         type1_constraint :: forall h1 h. Proxy c -> ty (h1 h) -> Maybe (Dict (c h1))
  69         type1_constraint _c _ = Nothing
  70 instance -- Type_Root
  71  Type1_Constraint c (ty (Type_Root ty)) =>
  72  Type1_Constraint c (Type_Root ty) where
  73         type1_constraint c (Type_Root ty) = type1_constraint c ty
  74 instance -- Type_Alt
  75  ( Type1_Constraint c (curr root)
  76  , Type1_Constraint c (next root)
  77  ) => Type1_Constraint c (Type_Alt curr next root) where
  78         type1_constraint c (Type_Alt_Curr ty) = type1_constraint c ty
  79         type1_constraint c (Type_Alt_Next ty) = type1_constraint c ty
  80 instance Type1_Constraint c (Type0 px root)