]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Type/Constraint.hs
polish names
[haskell/symantic.git] / 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)