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 instance -- String_from_Type
  42  String_from_Type root =>
  43  String_from_Type (Type_Fun lam root) where
  44         string_from_type (arg `Type_Fun` res) =
  45                 "(" ++ string_from_type arg ++ " -> "
  46                     ++ string_from_type res ++ ")"
  47 instance -- Show
  48  String_from_Type root =>
  49  Show (Type_Fun lam root h) where
  50         show = string_from_type
  51 instance Type_Constraint Eq  (Type_Fun lam root)
  52 instance Type_Constraint Ord (Type_Fun lam root)
  53
  54 type_fun_from
  55  :: forall (lam :: * -> *) (root :: * -> *) ast ret.
  56  ( Type_Root_Lift (Type_Fun lam) root
  57  , Type_from ast root
  58  , Root_of_Type root ~ root
  59  ) => Proxy (Type_Fun lam root)
  60  -> ast -> ast
  61  -> (forall h. root h -> Either (Error_of_Type ast root) ret)
  62  -> Either (Error_of_Type ast (Root_of_Type root)) ret
  63 type_fun_from (_ty::Proxy (Type_Fun lam root)) (ast_arg::ast) (ast_res::ast)
  64  (k::(forall h. Root_of_Type (Type_Fun lam root) h
  65                     -> Either (Error_of_Type ast (Root_of_Type (Type_Fun lam root))) ret)) =
  66         type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
  67         type_from (Proxy::Proxy root) ast_res $ \(ty_res::root h_res) ->
  68                 k (ty_arg `type_fun` ty_res
  69                  :: root (Lambda lam h_arg h_res))
  70
  71 -- | Convenient alias to include a 'Type_Fun' within a type.
  72 type_fun
  73  :: Type_Root_Lift (Type_Fun lam) root
  74  => root h_arg -> root h_res
  75  -> root (Lambda lam h_arg h_res)
  76 type_fun arg res = type_root_lift (Type_Fun arg res)
  77
  78 -- ** Type 'Lambda'
  79 -- | A type synonym for the host-type function,
  80 -- wrapping argument and result within a type constructor @lam@,
  81 -- which is used in the 'Repr_Host' instance of 'Sym_Lambda'
  82 -- to implement 'val' and 'lazy'.
  83 type Lambda lam arg res = lam arg -> lam res