]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Typing/Type.hs
Fix lambda application.
[haskell/symantic.git] / Language / Symantic / Typing / Type.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE FlexibleInstances #-}
4 {-# LANGUAGE GADTs #-}
5 {-# LANGUAGE MultiParamTypeClasses #-}
6 {-# LANGUAGE PolyKinds #-}
7 {-# LANGUAGE Rank2Types #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE StandaloneDeriving #-}
10 {-# LANGUAGE TypeFamilies #-}
11 {-# LANGUAGE TypeOperators #-}
12 {-# LANGUAGE TypeInType #-}
13 {-# LANGUAGE UndecidableInstances #-}
14 module Language.Symantic.Typing.Type where
15
16 import Data.Monoid ((<>))
17 import Data.Proxy
18 import Data.Maybe (fromMaybe, isJust)
19 import Data.Type.Equality
20 import qualified Data.Kind as K
21
22 import Language.Symantic.Typing.Kind
23 import Language.Symantic.Typing.Constant
24 import Language.Symantic.Typing.Syntax
25
26 -- * Type 'Type'
27
28 -- | /Type of terms/.
29 --
30 -- * @cs@: /type constants/, fixed at compile time.
31 -- * @h@: indexed Haskell type.
32 --
33 -- * 'TyConst': /type constant/, selected amongst @cs@.
34 -- * @(:$)@: /type application/.
35 data Type (cs::[K.Type]) (h::k) where
36 TyConst
37 :: Const cs c
38 -> Type cs c
39 (:$)
40 :: Type cs f
41 -> Type cs x
42 -> Type cs (f x)
43 {-
44 TyVar
45 :: SKind k
46 -> Type cs (v::k)
47 -}
48 infixl 9 :$
49
50 instance TestEquality (Type cs) where
51 testEquality = eq_type
52 instance Eq (Type cs h) where
53 _x == _y = True
54 instance Show_Const cs => Show (Type cs h) where
55 show = show_type
56 -- deriving instance Show_Const cs => Show (Type cs h)
57
58 kind_of :: Type cs (h::k) -> SKind k
59 kind_of t =
60 case t of
61 TyConst c -> kind_of_const c
62 f :$ _x ->
63 case kind_of f of
64 _kx `SKiArrow` kf -> kf
65
66 eq_type
67 :: Type cs (x::k) -> Type cs (y::k) -> Maybe (x:~:y)
68 eq_type (TyConst x) (TyConst y)
69 | Just Refl <- testEquality x y
70 = Just Refl
71 eq_type (xf :$ xx) (yf :$ yx)
72 | Just Refl <- eq_skind (kind_of xf) (kind_of yf)
73 , Just Refl <- eq_type xf yf
74 , Just Refl <- eq_type xx yx
75 = Just Refl
76 eq_type _ _ = Nothing
77
78 eq_kind_type
79 :: Type cs (x::kx) -> Type cs (y::ky) -> Maybe (kx:~:ky)
80 eq_kind_type (TyConst x) (TyConst y)
81 | Just Refl <- eq_kind_const x y
82 = Just Refl
83 eq_kind_type (xf :$ xx) (yf :$ yx)
84 | Just Refl <- eq_kind_type xf yf
85 , Just Refl <- eq_kind_type xx yx
86 = Just Refl
87 eq_kind_type _x _y = Nothing
88
89 show_type :: Show_Const cs => Type cs h -> String
90 show_type (TyConst c) = show c
91 show_type ((:$) f@(:$){} a@(:$){}) = "(" <> show_type f <> ") (" <> show_type a <> ")"
92 show_type ((:$) f@(:$){} a) = "(" <> show_type f <> ") " <> show_type a
93 show_type ((:$) f a@(:$){}) = show_type f <> " (" <> show_type a <> ")"
94 show_type ((:$) f a) = show_type f <> " " <> show_type a
95 -- show_type (TyVar v) = "t" <> show (integral_from_peano v::Integer)
96
97 -- * Type 'EType'
98 -- | Existential for 'Type'.
99 data EType cs = forall h. EType (Type cs h)
100
101 instance Eq (EType cs) where
102 EType x == EType y
103 | Just Refl <- eq_kind_type x y
104 = isJust $ eq_type x y
105 _x == _y = False
106 instance Show_Const cs => Show (EType cs) where
107 show (EType ty) = show ty
108
109 -- * Type 'KType'
110 -- | Existential for 'Type' of a known 'Kind'.
111 data KType cs k = forall (h::k). KType (Type cs h)
112
113 instance Eq (KType cs ki) where
114 KType x == KType y = isJust $ eq_type x y
115 instance Show_Const cs => Show (KType cs ki) where
116 show (KType ty) = show_type ty
117
118 -- * Class 'Type_from'
119 -- | Try to build a 'Type' from raw data.
120 class Type_from ast cs where
121 type_from
122 :: ast
123 -> (forall k h. Type cs (h::k) -> Either (Error_Type cs ast) ret)
124 -> Either (Error_Type cs ast) ret
125
126 -- ** Type 'Error_Type'
127 data Error_Type cs ast
128 = Error_Type_Constant_unknown (At ast (Lexem ast))
129 | Error_Type_Kind_mismatch (At ast EKind) (At ast EKind)
130 | Error_Type_Kind_not_applicable (At ast EKind)
131 deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Type cs ast)
132 deriving instance (Show ast, Show (Lexem ast), Show_Const cs) => Show (Error_Type cs ast)
133
134 instance
135 ( Const_from (Lexem ast) cs
136 , AST ast
137 ) => Type_from ast cs where
138 type_from ast kk =
139 fromMaybe (Left $ Error_Type_Constant_unknown $ At (Just ast) $ ast_lexem ast) $
140 const_from (ast_lexem ast) $ \c -> Just $
141 go (ast_nodes ast) (TyConst c) kk
142 where
143 go :: [ast]
144 -> Type cs h
145 -> (forall k' h'. Type cs (h'::k') -> Either (Error_Type cs ast) ret)
146 -> Either (Error_Type cs ast) ret
147 go [] ty k = k ty
148 go (ast_x:ast_xs) ty_f k =
149 type_from ast_x $ \ty_x ->
150 case kind_of ty_f of
151 ki_f_a `SKiArrow` _ki_f_b ->
152 let ki_x = kind_of ty_x in
153 case eq_skind ki_f_a ki_x of
154 Just Refl -> go ast_xs (ty_f :$ ty_x) k
155 Nothing -> Left $ Error_Type_Kind_mismatch
156 (At (Just ast) $ EKind ki_f_a)
157 (At (Just ast_x) $ EKind ki_x)
158 ki -> Left $ Error_Type_Kind_not_applicable $ At (Just ast) $ EKind ki
159
160 -- * Type 'Args'
161 data Args (cs::[K.Type]) (args::[K.Type]) where
162 ArgZ :: Args cs '[]
163 ArgS :: Type cs arg
164 -> Args cs args
165 -> Args cs (Proxy arg ': args)
166 infixr 5 `ArgS`
167
168 -- | Build the left spine of a 'Type'.
169 spine_of_type
170 :: Type cs h
171 -> (forall kc (c::kc) as. Const cs c -> Args cs as -> ret) -> ret
172 spine_of_type (TyConst c) k = k c ArgZ
173 spine_of_type (f :$ a) k = spine_of_type f $ \c as -> k c (a `ArgS` as)
174
175 -- * Usual 'Type's
176
177 -- | The '()' 'Type'
178 tyUnit :: Inj_Const cs () => Type cs ()
179 tyUnit = TyConst inj_const