1 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE MultiParamTypeClasses #-}
4 {-# LANGUAGE OverloadedStrings #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeFamilies #-}
7 {-# LANGUAGE UndecidableInstances #-}
8 module Language.LOL.Symantic.Type.Fun where
10 import Control.Arrow (left)
11 import Data.Maybe (isJust)
12 import Data.Type.Equality ((:~:)(Refl))
15 import Language.LOL.Symantic.AST
16 import Language.LOL.Symantic.Type.Common
20 -- | The function type.
21 data Type_Fun lam root h where
22 Type_Fun :: root h_arg
24 -> Type_Fun lam root (Lambda lam h_arg h_res)
26 type instance Root_of_Type (Type_Fun lam root) = root
27 type instance Error_of_Type ast (Type_Fun lam root) = Error_Type_Fun ast
29 -- | Convenient alias to include a 'Type_Fun' within a type.
31 :: Type_Root_Lift (Type_Fun lam) root
32 => root h_arg -> root h_res
33 -> root (Lambda lam h_arg h_res)
34 type_fun arg res = type_root_lift (Type_Fun arg res)
38 Type_Eq (Type_Fun lam root) where
40 (arg1 `Type_Fun` res1)
41 (arg2 `Type_Fun` res2)
42 | Just Refl <- arg1 `type_eq` arg2
43 , Just Refl <- res1 `type_eq` res2
48 Eq (Type_Fun lam root h) where
49 x == y = isJust $ type_eq x y
50 instance -- Type_from AST
53 , Type_Root_Lift (Type_Fun lam) root
54 , Error_Type_Lift (Error_Type AST) (Error_of_Type AST root)
55 -- NOTE: require UndecidableInstances.
56 , Error_Type_Lift (Error_Type_Fun AST) (Error_of_Type AST root)
57 -- NOTE: require UndecidableInstances.
58 , Error_Type_Unlift (Error_Type AST) (Error_of_Type AST root)
59 -- NOTE: require UndecidableInstances.
60 , Root_of_Type root ~ root
61 , Implicit_HBool (Is_Last_Type (Type_Fun lam root) root)
62 -- NOTE: require UndecidableInstances.
63 ) => Type_from AST (Type_Fun lam root) where
64 type_from _px_ty ast k =
70 case error_type_unlift err of
71 Just (Error_Type_Unsupported_here (a::AST)) ->
72 error_type_lift $ Error_Type_Unsupported a
74 type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
75 type_from (Proxy::Proxy root) ast_res $ \(ty_res::root h_res) ->
76 k (type_root_lift $ ty_arg `Type_Fun` ty_res
77 :: root (Lambda lam h_arg h_res))
78 _ -> Left $ error_type_lift $
79 Error_Type_Fun_Wrong_number_of_arguments 2 ast
81 case hbool :: HBool (Is_Last_Type (Type_Fun lam root) root) of
82 HTrue -> error_type_lift $ Error_Type_Unsupported ast
83 HFalse -> error_type_lift $ Error_Type_Unsupported_here ast
84 instance -- String_from_Type
85 String_from_Type root =>
86 String_from_Type (Type_Fun lam root) where
87 string_from_type (arg `Type_Fun` res) =
88 "(" ++ string_from_type arg ++ " -> "
89 ++ string_from_type res ++ ")"
91 String_from_Type root =>
92 Show (Type_Fun lam root h) where
93 show = string_from_type
97 -- | A type synonym for the host-type function,
98 -- wrapping argument and result within a type constructor @lam@,
99 -- which is used in the 'Repr_Host' instance of 'Sym_Lambda'
100 -- to implement 'val' and 'lazy'.
101 type Lambda lam arg res = lam arg -> lam res
103 -- * Type 'Error_Type_Fun'
105 -- | The 'Error_of_Type' of 'Type_Fun'.
106 data Error_Type_Fun ast
107 = Error_Type_Fun_Wrong_number_of_arguments Int ast