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 import Language.Symantic.Type.Root
  17 import Language.Symantic.Type.Error
  18 import Language.Symantic.Type.Type0
  19 import Language.Symantic.Type.Type1
  20 import Language.Symantic.Type.Type2
  21
  22 -- * Type 'Type_Fun'
  23 -- | The @->@ type.
  24 type Type_Fun = Type_Type2 (Proxy (->))
  25
  26 instance Unlift_Type1 Type_Fun where
  27         unlift_type1 (Type_Type2 px a b) k =
  28                 k ( Type_Type1 (Proxy::Proxy ((->) a)) b
  29                   , Lift_Type1 (\(Type_Type1 _ b') -> Type_Type2 px a b')
  30                   )
  31 instance Eq_Type root => Eq_Type1 (Type_Fun root) where
  32         eq_type1 (Type_Type2 _ a1 _b1) (Type_Type2 _ a2 _b2)
  33          | Just Refl <- eq_type a1 a2
  34          = Just Refl
  35         eq_type1 _ _ = Nothing
  36 instance Constraint_Type Eq (Type_Fun root)
  37 instance Constraint_Type Ord (Type_Fun root)
  38 instance
  39  Constraint_Type Monoid root =>
  40  Constraint_Type Monoid (Type_Fun root) where
  41         constraint_type c (Type_Type2 _ _arg res)
  42          | Just Dict <- constraint_type c res
  43          = Just Dict
  44         constraint_type _c _ = Nothing
  45 instance Constraint_Type Num (Type_Fun root)
  46 instance Constraint_Type Integral (Type_Fun root)
  47 instance Constraint_Type MT.MonoFunctor (Type_Fun root) where
  48         constraint_type _c Type_Type2{} = Just Dict
  49 instance Constraint_Type1 Functor (Type_Fun root) where
  50         constraint_type1 _c Type_Type2{} = Just Dict
  51 instance Constraint_Type1 Applicative (Type_Fun root) where
  52         constraint_type1 _c Type_Type2{} = Just Dict
  53 instance Constraint_Type1 Foldable (Type_Fun root)
  54 instance Constraint_Type1 Traversable (Type_Fun root)
  55 instance Constraint_Type1 Monad (Type_Fun root) where
  56         constraint_type1 _c Type_Type2{} = Just Dict
  57
  58 pattern Type_Fun
  59  :: root arg -> root res
  60  -> Type_Fun root ((->) arg res)
  61 pattern Type_Fun arg res
  62  = Type_Type2 Proxy arg res
  63
  64 instance -- Eq_Type
  65  Eq_Type root =>
  66  Eq_Type (Type_Fun root) where
  67         eq_type
  68          (Type_Type2 _ arg1 res1)
  69          (Type_Type2 _ arg2 res2)
  70          | Just Refl <- arg1 `eq_type` arg2
  71          , Just Refl <- res1 `eq_type` res2
  72          = Just Refl
  73         eq_type _ _ = Nothing
  74 instance -- String_from_Type
  75  String_from_Type root =>
  76  String_from_Type (Type_Fun root) where
  77         string_from_type (Type_Type2 _ arg res) =
  78                 "(" ++ string_from_type arg ++ " -> "
  79                     ++ string_from_type res ++ ")"
  80
  81 -- | Convenient alias to include a 'Type_Fun' within a type.
  82 type_fun
  83  :: forall root h_arg h_res.
  84  Lift_Type_Root Type_Fun root
  85  => root h_arg -> root h_res
  86  -> root ((->) h_arg h_res)
  87 type_fun = type_type2
  88
  89 -- | Parse 'Type_Fun'.
  90 type_fun_from
  91  :: forall (root :: * -> *) ast ret.
  92  ( Lift_Type_Root Type_Fun root
  93  , Type_from ast root
  94  , Root_of_Type root ~ root
  95  ) => Proxy (Type_Fun root)
  96  -> ast -> ast
  97  -> (forall h. root h -> Either (Error_of_Type ast root) ret)
  98  -> Either (Error_of_Type ast root) ret
  99 type_fun_from _ty ast_arg ast_res k =
 100         type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
 101         type_from (Proxy::Proxy root) ast_res $ \(ty_res::root h_res) ->
 102         k (ty_arg `type_fun` ty_res
 103          :: root ((->) h_arg h_res))