Language/LOL/Symantic/Type/Fun.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE OverloadedStrings #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# LANGUAGE UndecidableInstances #-}
   8 module Language.LOL.Symantic.Type.Fun where
   9
  10 import Control.Arrow (left)
  11 import Data.Maybe (isJust)
  12 import Data.Type.Equality ((:~:)(Refl))
  13 import Data.Proxy
  14
  15 import Language.LOL.Symantic.AST
  16 import Language.LOL.Symantic.Type.Common
  17
  18 -- * Type 'Type_Fun'
  19
  20 -- | The function type.
  21 data Type_Fun lam root h where
  22         Type_Fun :: root h_arg
  23                  -> root h_res
  24                  -> Type_Fun lam root (Lambda lam h_arg h_res)
  25
  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
  28
  29 -- | Convenient alias to include a 'Type_Fun' within a type.
  30 type_fun
  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)
  35
  36 instance -- Type_Eq
  37  Type_Eq root =>
  38  Type_Eq (Type_Fun lam root) where
  39         type_eq
  40          (arg1 `Type_Fun` res1)
  41          (arg2 `Type_Fun` res2)
  42          | Just Refl <- arg1 `type_eq` arg2
  43          , Just Refl <- res1 `type_eq` res2
  44          = Just Refl
  45         type_eq _ _ = Nothing
  46 instance -- Eq
  47  Type_Eq root =>
  48  Eq (Type_Fun lam root h) where
  49         x == y = isJust $ type_eq x y
  50 instance -- Type_from AST
  51  ( Type_Eq root
  52  , Type_from AST root
  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  , Root_of_Type root ~ root
  60  , Implicit_HBool (Is_Last_Type (Type_Fun lam root) root)
  61  ) => Type_from AST (Type_Fun lam root) where
  62         type_from _px_ty ast k =
  63                 case ast of
  64                  AST "->" asts ->
  65                         case asts of
  66                          [ast_arg, ast_res] ->
  67                                 left (\err ->
  68                                         case error_type_unlift err of
  69                                          Just (Error_Type_Unsupported (a::AST)) ->
  70                                                 error_type_lift $ Error_Type_Unsupported_from_root a
  71                                          _ -> err) $
  72                                 type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
  73                                 type_from (Proxy::Proxy root) ast_res $ \(ty_res::root h_res) ->
  74                                         k (type_root_lift $ ty_arg `Type_Fun` ty_res
  75                                          :: root (Lambda lam h_arg h_res))
  76                          _ -> Left $ error_type_lift $
  77                                 Error_Type_Fun_Wrong_number_of_arguments 2 ast
  78                  _ -> Left $
  79                         case hbool :: HBool (Is_Last_Type (Type_Fun lam root) root) of
  80                          HTrue  -> error_type_lift $ Error_Type_Unsupported_from_root ast
  81                          HFalse -> error_type_lift $ Error_Type_Unsupported ast
  82 instance -- String_from_Type
  83  String_from_Type root =>
  84  String_from_Type (Type_Fun lam root) where
  85         string_from_type (arg `Type_Fun` res) =
  86                 "(" ++ string_from_type arg ++ " -> "
  87                     ++ string_from_type res ++ ")"
  88 instance -- Show
  89  String_from_Type root =>
  90  Show (Type_Fun lam root h) where
  91         show = string_from_type
  92
  93 -- ** Type 'Lambda'
  94
  95 -- | A type synonym for the host-type function,
  96 -- wrapping argument and result within a type constructor @lam@,
  97 -- which is used in the 'Repr_Host' instance of 'Sym_Lambda'
  98 -- to implement 'val' and 'lazy'.
  99 type Lambda lam arg res = lam arg -> lam res
 100
 101 -- * Type 'Error_Type_Fun'
 102
 103 -- | The 'Error_of_Type' of 'Type_Fun'.
 104 data Error_Type_Fun ast
 105  =   Error_Type_Fun_Wrong_number_of_arguments Int ast
 106  deriving (Eq, Show)