Language/Symantic/Type/Fun.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE PatternSynonyms #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# OPTIONS_GHC -fno-warn-orphans #-}
  11 module Language.Symantic.Type.Fun where
  12
  13 import Data.Proxy
  14 import Data.Type.Equality ((:~:)(Refl))
  15 import qualified Data.MonoTraversable as MT
  16
  17 import Language.Symantic.Type.Root
  18 import Language.Symantic.Type.Error
  19 import Language.Symantic.Type.Type0
  20 import Language.Symantic.Type.Type1
  21 import Language.Symantic.Type.Type2
  22 import Language.Symantic.Type.Constraint
  23 import Language.Symantic.Type.Family
  24
  25 -- * Type 'Type_Fun'
  26 -- | The @->@ type.
  27 type Type_Fun = Type2 (Proxy (->))
  28
  29 pattern Type_Fun
  30  :: root arg -> root res
  31  -> Type_Fun root ((->) arg res)
  32 pattern Type_Fun arg res
  33  = Type2 Proxy arg res
  34
  35 instance Type1_Unlift Type_Fun where
  36         type1_unlift (Type2 px a b) k =
  37                 k ( Type1 (Proxy::Proxy ((->) a)) b
  38                   , Type1_Lift (\(Type1 _ b') -> Type2 px a b')
  39                   )
  40 instance Type0_Eq root => Type1_Eq (Type_Fun root) where
  41         type1_eq (Type2 _ a1 _b1) (Type2 _ a2 _b2)
  42          | Just Refl <- type0_eq a1 a2
  43          = Just Refl
  44         type1_eq _ _ = Nothing
  45 instance Type0_Constraint Eq (Type_Fun root)
  46 instance Type0_Constraint Ord (Type_Fun root)
  47 instance
  48  Type0_Constraint Monoid root =>
  49  Type0_Constraint Monoid (Type_Fun root) where
  50         type0_constraint c (Type2 _ _arg res)
  51          | Just Dict <- type0_constraint c res
  52          = Just Dict
  53         type0_constraint _c _ = Nothing
  54 instance Type0_Constraint Num (Type_Fun root)
  55 instance Type0_Constraint Integral (Type_Fun root)
  56 instance Type0_Constraint MT.MonoFunctor (Type_Fun root) where
  57         type0_constraint _c Type2{} = Just Dict
  58 instance Type1_Constraint Functor (Type_Fun root) where
  59         type1_constraint _c Type2{} = Just Dict
  60 instance Type1_Constraint Applicative (Type_Fun root) where
  61         type1_constraint _c Type2{} = Just Dict
  62 instance Type1_Constraint Foldable (Type_Fun root)
  63 instance Type1_Constraint Traversable (Type_Fun root)
  64 instance Type1_Constraint Monad (Type_Fun root) where
  65         type1_constraint _c Type2{} = Just Dict
  66 instance Type0_Family Type_Family_MonoElement (Type_Fun root) where
  67         type0_family _at (Type2 _px _r a) = Just a
  68
  69 instance -- Type0_Eq
  70  Type0_Eq root =>
  71  Type0_Eq (Type_Fun root) where
  72         type0_eq
  73          (Type2 _ arg1 res1)
  74          (Type2 _ arg2 res2)
  75          | Just Refl <- arg1 `type0_eq` arg2
  76          , Just Refl <- res1 `type0_eq` res2
  77          = Just Refl
  78         type0_eq _ _ = Nothing
  79 instance -- String_from_Type
  80  String_from_Type root =>
  81  String_from_Type (Type_Fun root) where
  82         string_from_type (Type2 _ arg res) =
  83                 "(" ++ string_from_type arg ++ " -> "
  84                     ++ string_from_type res ++ ")"
  85
  86 -- | Convenient alias to include a 'Type_Fun' within a type.
  87 type_fun
  88  :: forall root h_arg h_res.
  89  Type_Root_Lift Type_Fun root
  90  => root h_arg -> root h_res
  91  -> root ((->) h_arg h_res)
  92 type_fun = type2
  93
  94 -- | Parse 'Type_Fun'.
  95 type_fun_from
  96  :: forall (root :: * -> *) ast ret.
  97  ( Type_Root_Lift Type_Fun root
  98  , Type0_From ast root
  99  , Root_of_Type root ~ root
 100  ) => Proxy (Type_Fun root)
 101  -> ast -> ast
 102  -> (forall h. root h -> Either (Error_of_Type ast root) ret)
 103  -> Either (Error_of_Type ast root) ret
 104 type_fun_from _ty ast_arg ast_res k =
 105         type0_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
 106         type0_from (Proxy::Proxy root) ast_res $ \(ty_res::root h_res) ->
 107         k (ty_arg `type_fun` ty_res
 108          :: root ((->) h_arg h_res))