TFHOE/Type/Fun.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE TypeFamilies #-}
   5 module TFHOE.Type.Fun where
   6
   7 import Data.Maybe (isJust)
   8 import Data.Type.Equality ((:~:)(Refl))
   9
  10 import TFHOE.Raw
  11 import TFHOE.Type.Common
  12
  13 -- * Type 'Type_Fun'
  14
  15 data Type_Fun fun next h where
  16         Type_Fun      :: Type_Fun fun next arg
  17                       -> Type_Fun fun next res
  18                       -> Type_Fun fun next (Fun fun arg res)
  19         Type_Fun_Next :: next h -> Type_Fun fun next h
  20
  21 instance -- Type_Eq
  22  Type_Eq next =>
  23  Type_Eq (Type_Fun fun next) where
  24         type_eq
  25          (arg1 `Type_Fun` res1)
  26          (arg2 `Type_Fun` res2)
  27          | Just Refl <- arg1 `type_eq` arg2
  28          , Just Refl <- res1 `type_eq` res2
  29          = Just Refl
  30         type_eq (Type_Fun_Next x)
  31                 (Type_Fun_Next y) = x `type_eq` y
  32         type_eq _ _ = Nothing
  33 instance -- Eq
  34  Type_Eq next =>
  35  Eq (Type_Fun fun next h) where
  36         x == y = isJust $ type_eq x y
  37 instance -- Type_from Raw
  38  Type_from Raw next =>
  39  Type_from Raw (Type_Fun fun next) where
  40         type_from (Raw "->" [raw_arg, raw_res]) k =
  41                 type_from raw_arg $ \ty_arg ->
  42                 type_from raw_res $ \ty_res ->
  43                 k (ty_arg `Type_Fun` ty_res)
  44         type_from raw k = type_from raw $ k . Type_Fun_Next
  45 instance -- String_from_Type
  46  String_from_Type next =>
  47  String_from_Type (Type_Fun fun next) where
  48         string_from_type (arg `Type_Fun` res) =
  49                 "(" ++ string_from_type arg ++ " -> "
  50                     ++ string_from_type res ++ ")"
  51         string_from_type (Type_Fun_Next t) = string_from_type t
  52 instance -- Show
  53  String_from_Type next =>
  54  Show (Type_Fun fun next h) where
  55         show = string_from_type
  56
  57 -- ** Type 'Fun'
  58
  59 -- | A type synonym for the host-type function,
  60 -- wrapping argument and result within a type constructor @fun@,
  61 -- which is used in the 'Repr_Host' instance of 'Expr_Fun'
  62 -- to implement 'val' and 'lazy'.
  63 type Fun fun arg res = (fun arg -> fun res)