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-missing-methods #-}
  11 module Language.Symantic.Type.Fun where
  12
  13 import Data.Proxy
  14
  15 import Language.Symantic.Type.Common
  16
  17 -- * Type 'Type_Fun'
  18 -- | The @->@ type.
  19 type Type_Fun lam = Type_Type2 (Lambda lam)
  20 pattern Type_Fun arg res = Type_Type2 Proxy arg res
  21
  22 instance -- String_from_Type
  23  String_from_Type root =>
  24  String_from_Type (Type_Fun lam root) where
  25         string_from_type (Type_Type2 _ arg res) =
  26                 "(" ++ string_from_type arg ++ " -> "
  27                     ++ string_from_type res ++ ")"
  28
  29 -- | Convenient alias to include a 'Type_Fun' within a type.
  30 type_fun
  31  :: Lift_Type_Root (Type_Fun lam) root
  32  => root h_arg -> root h_res
  33  -> root (Lambda lam h_arg h_res)
  34 type_fun arg res = lift_type_root (Type_Type2 Proxy arg res)
  35
  36 type_fun_from
  37  :: forall (lam :: * -> *) (root :: * -> *) ast ret.
  38  ( Lift_Type_Root (Type_Fun lam) root
  39  , Type_from ast root
  40  , Root_of_Type root ~ root
  41  ) => Proxy (Type_Fun lam root)
  42  -> ast -> ast
  43  -> (forall h. root h -> Either (Error_of_Type ast root) ret)
  44  -> Either (Error_of_Type ast root) ret
  45 type_fun_from _ty ast_arg ast_res k =
  46         type_from (Proxy::Proxy root) ast_arg $ \(ty_arg::root h_arg) ->
  47         type_from (Proxy::Proxy root) ast_res $ \(ty_res::root h_res) ->
  48         k (ty_arg `type_fun` ty_res
  49          :: root (Lambda lam h_arg h_res))
  50
  51 -- ** Type 'Lambda'
  52 -- | A newtype for the host-type function (->),
  53 -- wrapping argument and result within a type constructor @lam@,
  54 -- which is used in the 'Repr_Host' instance of 'Sym_Lambda'
  55 -- to implement 'val' and 'lazy'.
  56 --
  57 -- NOTE: a newtype is used instead of a type synonym
  58 -- in order to be able to use it as a type constructor: @Lambda lam arg@,
  59 -- which for instance has instances: 'Functor', 'Applicative', and 'Monad'.
  60 newtype Lambda lam arg res
  61  =      Lambda { unLambda :: (->) (lam arg) (lam res) }
  62
  63 {-
  64 data Type_Fun lam root h where
  65         Type_Fun :: root h_arg
  66                  -> root h_res
  67                  -> Type_Fun lam root (Lambda lam h_arg h_res)
  68
  69 type instance Root_of_Type      (Type_Fun lam root) = root
  70 type instance Error_of_Type ast (Type_Fun lam root) = ()
  71
  72 instance -- Eq_Type
  73  Eq_Type root =>
  74  Eq_Type (Type_Fun lam root) where
  75         eq_type
  76          (arg1 `Type_Fun` res1)
  77          (arg2 `Type_Fun` res2)
  78          | Just Refl <- arg1 `eq_type` arg2
  79          , Just Refl <- res1 `eq_type` res2
  80          = Just Refl
  81         eq_type _ _ = Nothing
  82 instance -- Eq
  83  Eq_Type root =>
  84  Eq (Type_Fun lam root h) where
  85         x == y = isJust $ x `eq_type` y
  86 instance -- Show
  87  String_from_Type root =>
  88  Show (Type_Fun lam root h) where
  89         show = string_from_type
  90 instance Constraint_Type Eq  (Type_Fun lam root)
  91 instance Constraint_Type Ord (Type_Fun lam root)
  92 instance Unlift_Type1 (Type_Fun lam)
  93 instance Eq_Type1 (Type_Fun lam root)
  94
  95
  96 -}