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 Data.Maybe (isJust)
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import Data.Proxy
  13
  14 import Language.LOL.Symantic.AST
  15 import Language.LOL.Symantic.Type.Common
  16
  17 -- * Type 'Type_Fun'
  18
  19 -- | The function type.
  20 data Type_Fun lam root h where
  21         Type_Fun :: root h_arg
  22                  -> root h_res
  23                  -> Type_Fun lam root (Lambda lam h_arg h_res)
  24
  25 type instance Root_of_Type (Type_Fun lam root) = root
  26 type instance Error_of_Type ast (Type_Fun lam root) = Error_Type_Fun ast
  27
  28 -- | Convenient alias to include a 'Type_Fun' within a type.
  29 type_fun
  30  :: Type_Root_Lift (Type_Fun lam) root
  31  => root h_arg -> root h_res
  32  -> root (Lambda lam h_arg h_res)
  33 type_fun arg res = type_root_lift (Type_Fun arg res)
  34
  35 instance -- Type_Eq
  36  Type_Eq root =>
  37  Type_Eq (Type_Fun lam root) where
  38         type_eq
  39          (arg1 `Type_Fun` res1)
  40          (arg2 `Type_Fun` res2)
  41          | Just Refl <- arg1 `type_eq` arg2
  42          , Just Refl <- res1 `type_eq` res2
  43          = Just Refl
  44         type_eq _ _ = Nothing
  45 instance -- Eq
  46  Type_Eq root =>
  47  Eq (Type_Fun lam root h) where
  48         x == y = isJust $ type_eq x y
  49 instance -- Type_from AST
  50  ( Type_Eq root
  51  , Type_from AST root
  52  , Type_Root_Lift (Type_Fun lam) root
  53  , Error_Type_Lift (Error_Type_Fun AST) (Error_of_Type AST root)
  54    -- NOTE: require UndecidableInstances.
  55  , Root_of_Type root ~ root
  56  ) => Type_from AST (Type_Fun lam root) where
  57         type_from _px_ty ast@(AST "->" asts) k =
  58                 case asts of
  59                  [ast_arg, ast_res] ->
  60                         type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
  61                         type_from (Proxy::Proxy root) ast_res $ \(ty_res::root h_res) ->
  62                                 k (type_root_lift $ ty_arg `Type_Fun` ty_res
  63                                  :: root (Lambda lam h_arg h_res))
  64                  _ -> Left $ Just $ error_type_lift $
  65                         Error_Type_Fun_Wrong_number_of_arguments 2 ast
  66         type_from _px_ty _ast _k = Left Nothing
  67 instance -- String_from_Type
  68  String_from_Type root =>
  69  String_from_Type (Type_Fun lam root) where
  70         string_from_type (arg `Type_Fun` res) =
  71                 "(" ++ string_from_type arg ++ " -> "
  72                     ++ string_from_type res ++ ")"
  73 instance -- Show
  74  String_from_Type root =>
  75  Show (Type_Fun lam root h) where
  76         show = string_from_type
  77
  78 -- ** Type 'Lambda'
  79
  80 -- | A type synonym for the host-type function,
  81 -- wrapping argument and result within a type constructor @lam@,
  82 -- which is used in the 'Repr_Host' instance of 'Sym_Lambda'
  83 -- to implement 'val' and 'lazy'.
  84 type Lambda lam arg res = lam arg -> lam res
  85
  86 -- * Type 'Error_Type_Fun'
  87
  88 -- | The 'Error_of_Type' of 'Type_Fun'.
  89 data Error_Type_Fun ast
  90  =   Error_Type_Fun_Wrong_number_of_arguments Int ast
  91  deriving (Eq, Show)