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 Language.Symantic.Type.Root
  16 import Language.Symantic.Type.Error
  17 import Language.Symantic.Type.Type0
  18 import Language.Symantic.Type.Type1
  19 import Language.Symantic.Type.Type2
  20
  21 -- * Type 'Type_Fun'
  22 -- | The @->@ type.
  23 type Type_Fun lam
  24  = Type_Type2 (Proxy (Lambda lam))
  25
  26 type instance Constraint2_of (Proxy (Lambda lam))
  27  = Constraint2_Empty
  28 instance Unlift_Type1 (Type_Type2 (Proxy (Lambda lam))) where
  29         unlift_type1 (Type_Type2 px a b) k =
  30                 k ( Type_Type1 (Proxy::Proxy (Lambda lam a)) b
  31                   , Lift_Type1 (\(Type_Type1 _ b') -> Type_Type2 px a b')
  32                   )
  33 instance Eq_Type root => Eq_Type1 (Type_Type2 (Proxy (Lambda lam)) root) where
  34         eq_type1 (Type_Type2 _ a1 _b1) (Type_Type2 _ a2 _b2)
  35          | Just Refl <- eq_type a1 a2
  36          = Just Refl
  37         eq_type1 _ _ = Nothing
  38 {- FIXME: OverlappingInstances
  39 instance (Monad lam, Monoid a) => Monoid (lam a) where
  40         mempty  = return mempty
  41         mappend = liftM2 mappend
  42 instance
  43  ( Monad lam
  44  , Constraint_Type Monoid root
  45  ) => Constraint_Type Monoid (Type_Type2 (Proxy (Lambda lam)) root) where
  46         constraint_type c (Type_Type2 _ _arg res)
  47          | Just Dict <- constraint_type c res
  48          = Just Dict
  49 -}
  50 instance Constraint_Type Monoid (Type_Type2 (Proxy (Lambda lam)) root)
  51 instance (Constraint_Type1 Functor root, Functor lam)
  52  => Constraint_Type1 Functor (Type_Type2 (Proxy (Lambda lam)) root) where
  53         constraint_type1 _c Type_Type2{} = Just Dict
  54 instance (Constraint_Type1 Applicative root, Applicative lam)
  55  => Constraint_Type1 Applicative (Type_Type2 (Proxy (Lambda lam)) root) where
  56         constraint_type1 _c Type_Type2{} = Just Dict
  57 instance Constraint_Type1 Foldable (Type_Fun lam root)
  58 instance Constraint_Type1 Traversable (Type_Fun lam root)
  59 instance Monad lam => Constraint_Type1 Monad (Type_Fun lam root) where
  60         constraint_type1 _c Type_Type2{} = Just Dict
  61
  62 pattern Type_Fun
  63  :: root arg -> root res
  64  -> Type_Fun lam root ((Lambda lam) arg res)
  65 pattern Type_Fun arg res
  66  = Type_Type2 Proxy arg res
  67
  68 instance -- Eq_Type
  69  Eq_Type root =>
  70  Eq_Type (Type_Type2 (Proxy (Lambda lam)) root) where
  71         eq_type
  72          (Type_Type2 _ arg1 res1)
  73          (Type_Type2 _ arg2 res2)
  74          | Just Refl <- arg1 `eq_type` arg2
  75          , Just Refl <- res1 `eq_type` res2
  76          = Just Refl
  77         eq_type _ _ = Nothing
  78 instance -- String_from_Type
  79  String_from_Type root =>
  80  String_from_Type (Type_Fun lam root) where
  81         string_from_type (Type_Type2 _ arg res) =
  82                 "(" ++ string_from_type arg ++ " -> "
  83                     ++ string_from_type res ++ ")"
  84
  85 -- ** Type 'Lambda'
  86 -- | A newtype for the host-type function (->),
  87 -- wrapping argument and result within a type constructor @lam@,
  88 -- which is used in the 'Repr_Host' instance of 'Sym_Lambda'
  89 -- to control the calling (see 'val' and 'lazy').
  90 --
  91 -- NOTE: a newtype is used instead of a type synonym
  92 -- in order to be able to use it as a type constructor: @Lambda lam arg@,
  93 -- which for instance has instances: 'Functor', 'Applicative', and 'Monad'.
  94 newtype Lambda lam arg res
  95  =      Lambda { unLambda :: (->) (lam arg) (lam res) }
  96 instance Functor lam => Functor (Lambda lam a) where
  97         fmap a2b (Lambda a) = Lambda $ \x -> fmap a2b (a x)
  98 instance Applicative lam => Applicative (Lambda lam a) where
  99         pure = Lambda . const . pure
 100         (<*>) (Lambda a2b) (Lambda a) = Lambda $ \x -> a2b x <*> a x
 101 instance Monad lam => Monad (Lambda lam a) where
 102         return = Lambda . const . return
 103         (>>=) (Lambda a) a2mb = Lambda $ \x -> a x >>= (\y -> unLambda (a2mb y) x)
 104
 105 -- | Convenient alias to include a 'Type_Fun' within a type.
 106 type_fun
 107  :: forall lam root h_arg h_res.
 108  Lift_Type_Root (Type_Fun lam) root
 109  => root h_arg -> root h_res
 110  -> root (Lambda lam h_arg h_res)
 111 type_fun arg res = lift_type_root (Type_Fun arg res
 112          ::Type_Fun lam root (Lambda lam h_arg h_res))
 113
 114 -- | Parse 'Type_Fun'.
 115 type_fun_from
 116  :: forall (lam :: * -> *) (root :: * -> *) ast ret.
 117  ( Lift_Type_Root (Type_Fun lam) root
 118  , Type_from ast root
 119  , Root_of_Type root ~ root
 120  ) => Proxy (Type_Fun lam root)
 121  -> ast -> ast
 122  -> (forall h. root h -> Either (Error_of_Type ast root) ret)
 123  -> Either (Error_of_Type ast root) ret
 124 type_fun_from _ty ast_arg ast_res k =
 125         type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
 126         type_from (Proxy::Proxy root) ast_res $ \(ty_res::root h_res) ->
 127         k (ty_arg `type_fun` ty_res
 128          :: root (Lambda lam h_arg h_res))