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 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
   9 module Language.Symantic.Type.Fun where
  10
  11 import Data.Maybe (isJust)
  12 import Data.Proxy
  13 import Data.Type.Equality ((:~:)(Refl))
  14
  15 import Language.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 -- Eq_Type
  28  Eq_Type root =>
  29  Eq_Type (Type_Fun lam root) where
  30         eq_type
  31          (arg1 `Type_Fun` res1)
  32          (arg2 `Type_Fun` res2)
  33          | Just Refl <- arg1 `eq_type` arg2
  34          , Just Refl <- res1 `eq_type` res2
  35          = Just Refl
  36         eq_type _ _ = Nothing
  37 instance -- Eq
  38  Eq_Type root =>
  39  Eq (Type_Fun lam root h) where
  40         x == y = isJust $ x `eq_type` 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 Constraint_Type Eq  (Type_Fun lam root)
  52 instance Constraint_Type Ord (Type_Fun lam root)
  53 instance Unlift_Type1 (Type_Fun lam)
  54 instance Eq_Type1 (Type_Fun lam root)
  55
  56 type_fun_from
  57  :: forall (lam :: * -> *) (root :: * -> *) ast ret.
  58  ( Type_Root_Lift (Type_Fun lam) root
  59  , Type_from ast root
  60  , Root_of_Type root ~ root
  61  ) => Proxy (Type_Fun lam root)
  62  -> ast -> ast
  63  -> (forall h. root h -> Either (Error_of_Type ast root) ret)
  64  -> Either (Error_of_Type ast root) ret
  65 type_fun_from _ty ast_arg ast_res k =
  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 newtype 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 --
  84 -- NOTE: a newtype is used instead of a type synonym
  85 -- in order to be able to use it as a type constructor: @Lambda lam arg@,
  86 -- which for instance has instances: 'Functor', 'Applicative', and 'Monad'.
  87 newtype Lambda lam arg res
  88  =      Lambda { unLambda :: (->) (lam arg) (lam res) }