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