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