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    -- 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 =
  65                 case ast of
  66                  AST "->" asts ->
  67                         case asts of
  68                          [ast_arg, ast_res] ->
  69                                 left (\err ->
  70                                         case error_type_unlift err of
  71                                          Just (Error_Type_Unsupported_here (a::AST)) ->
  72                                                 error_type_lift $ Error_Type_Unsupported a
  73                                          _ -> err) $
  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
  80                  _ -> Left $
  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 ++ ")"
  90 instance -- Show
  91  String_from_Type root =>
  92  Show (Type_Fun lam root h) where
  93         show = string_from_type
  94
  95 -- ** Type 'Lambda'
  96
  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
 102
 103 -- * Type 'Error_Type_Fun'
 104
 105 -- | The 'Error_of_Type' of 'Type_Fun'.
 106 data Error_Type_Fun ast
 107  =   Error_Type_Fun_Wrong_number_of_arguments Int ast
 108  deriving (Eq, Show)