Language/LOL/Symantic/Type/Fun.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE Rank2Types #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeFamilies #-}
   8 {-# LANGUAGE UndecidableInstances #-}
   9 module Language.LOL.Symantic.Type.Fun where
  10
  11 import Data.Maybe (isJust)
  12 import Data.Type.Equality ((:~:)(Refl))
  13 import Data.Proxy
  14
  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
  42 type_fun_from
  43  :: forall (lam :: * -> *) (root :: * -> *) ast ret.
  44  ( Type_Root_Lift (Type_Fun lam) root
  45  , Type_from ast root
  46  , Root_of_Type root ~ root
  47  ) => Proxy (Type_Fun lam root)
  48  -> ast -> ast
  49  -> (forall h. root h -> Either (Error_of_Type ast root) ret)
  50  -> Either (Error_of_Type ast (Root_of_Type root)) ret
  51 type_fun_from (_px_ty::Proxy (Type_Fun lam root)) (ast_arg::ast) (ast_res::ast)
  52  (k::(forall h. Root_of_Type (Type_Fun lam root) h
  53                     -> Either (Error_of_Type ast (Root_of_Type (Type_Fun lam root))) ret)) =
  54         type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
  55         type_from (Proxy::Proxy root) ast_res $ \(ty_res::root h_res) ->
  56                 k (ty_arg `type_fun` ty_res
  57                  :: root (Lambda lam h_arg h_res))
  58 instance -- String_from_Type
  59  String_from_Type root =>
  60  String_from_Type (Type_Fun lam root) where
  61         string_from_type (arg `Type_Fun` res) =
  62                 "(" ++ string_from_type arg ++ " -> "
  63                     ++ string_from_type res ++ ")"
  64 instance -- Show
  65  String_from_Type root =>
  66  Show (Type_Fun lam root h) where
  67         show = string_from_type
  68
  69 -- | Convenient alias to include a 'Type_Fun' within a type.
  70 type_fun
  71  :: Type_Root_Lift (Type_Fun lam) root
  72  => root h_arg -> root h_res
  73  -> root (Lambda lam h_arg h_res)
  74 type_fun arg res = type_root_lift (Type_Fun arg res)
  75
  76 -- ** Type 'Lambda'
  77 -- | A type synonym for the host-type function,
  78 -- wrapping argument and result within a type constructor @lam@,
  79 -- which is used in the 'Repr_Host' instance of 'Sym_Lambda'
  80 -- to implement 'val' and 'lazy'.
  81 type Lambda lam arg res = lam arg -> lam res