]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Type/Fun.hs
fix Num requiring Integer
[haskell/symantic.git] / Language / Symantic / Type / Fun.hs
1 {-# LANGUAGE FlexibleContexts #-}
2 {-# LANGUAGE FlexibleInstances #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE MultiParamTypeClasses #-}
5 {-# LANGUAGE OverloadedStrings #-}
6 {-# LANGUAGE PatternSynonyms #-}
7 {-# LANGUAGE Rank2Types #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE TypeFamilies #-}
10 {-# OPTIONS_GHC -fno-warn-orphans #-}
11 module Language.Symantic.Type.Fun where
12
13 import Data.Proxy
14 import Data.Type.Equality ((:~:)(Refl))
15 import qualified Data.MonoTraversable as MT
16
17 import Language.Symantic.Type.Root
18 import Language.Symantic.Type.Error
19 import Language.Symantic.Type.Type0
20 import Language.Symantic.Type.Type1
21 import Language.Symantic.Type.Type2
22 import Language.Symantic.Type.Constraint
23 import Language.Symantic.Type.Family
24
25 -- * Type 'Type_Fun'
26 -- | The @->@ type.
27 type Type_Fun = Type2 (Proxy (->))
28
29 pattern Type_Fun
30 :: root arg -> root res
31 -> Type_Fun root ((->) arg res)
32 pattern Type_Fun arg res
33 = Type2 Proxy arg res
34
35 instance Type1_Unlift Type_Fun where
36 type1_unlift (Type2 px a b) k =
37 k ( Type1 (Proxy::Proxy ((->) a)) b
38 , Type1_Lift (\(Type1 _ b') -> Type2 px a b')
39 )
40 instance Type0_Eq root => Type1_Eq (Type_Fun root) where
41 type1_eq (Type2 _ a1 _b1) (Type2 _ a2 _b2)
42 | Just Refl <- type0_eq a1 a2
43 = Just Refl
44 type1_eq _ _ = Nothing
45 instance Type0_Constraint Eq (Type_Fun root)
46 instance Type0_Constraint Ord (Type_Fun root)
47 instance
48 Type0_Constraint Monoid root =>
49 Type0_Constraint Monoid (Type_Fun root) where
50 type0_constraint c (Type2 _ _arg res)
51 | Just Dict <- type0_constraint c res
52 = Just Dict
53 type0_constraint _c _ = Nothing
54 instance Type0_Constraint Num (Type_Fun root)
55 instance Type0_Constraint Integral (Type_Fun root)
56 instance Type0_Family Type_Family_MonoElement (Type_Fun root) where
57 type0_family _at (Type2 _px _r a) = Just a
58 instance Type0_Constraint MT.MonoFunctor (Type_Fun root) where
59 type0_constraint _c Type2{} = Just Dict
60 instance Type1_Constraint Functor (Type_Fun root) where
61 type1_constraint _c Type2{} = Just Dict
62 instance Type1_Constraint Applicative (Type_Fun root) where
63 type1_constraint _c Type2{} = Just Dict
64 instance Type1_Constraint Foldable (Type_Fun root)
65 instance Type1_Constraint Traversable (Type_Fun root)
66 instance Type1_Constraint Monad (Type_Fun root) where
67 type1_constraint _c Type2{} = Just Dict
68
69 instance -- Type0_Eq
70 Type0_Eq root =>
71 Type0_Eq (Type_Fun root) where
72 type0_eq
73 (Type2 _ arg1 res1)
74 (Type2 _ arg2 res2)
75 | Just Refl <- arg1 `type0_eq` arg2
76 , Just Refl <- res1 `type0_eq` res2
77 = Just Refl
78 type0_eq _ _ = Nothing
79 instance -- String_from_Type
80 String_from_Type root =>
81 String_from_Type (Type_Fun root) where
82 string_from_type (Type2 _ arg res) =
83 "(" ++ string_from_type arg ++ " -> "
84 ++ string_from_type res ++ ")"
85
86 -- | Convenient alias to include a 'Type_Fun' within a type.
87 type_fun
88 :: Type_Root_Lift Type_Fun root
89 => root h_arg -> root h_res -> root ((->) h_arg h_res)
90 type_fun = type2
91
92 -- | Parse 'Type_Fun'.
93 type_fun_from
94 :: forall (root :: * -> *) ast ret.
95 ( Type_Root_Lift Type_Fun root
96 , Type0_From ast root
97 , Root_of_Type root ~ root
98 ) => Proxy (Type_Fun root)
99 -> ast -> ast
100 -> (forall h. root h -> Either (Error_of_Type ast root) ret)
101 -> Either (Error_of_Type ast root) ret
102 type_fun_from _ty ast_arg ast_res k =
103 type0_from (Proxy::Proxy root) ast_arg $ \ty_arg ->
104 type0_from (Proxy::Proxy root) ast_res $ \ty_res ->
105 k (ty_arg `type_fun` ty_res)