Language/Symantic/Type/Tuple.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE PatternSynonyms #-}
   4 {-# LANGUAGE ScopedTypeVariables #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# OPTIONS_GHC -fno-warn-orphans #-}
   7 module Language.Symantic.Type.Tuple where
   8
   9 import Data.Proxy
  10 import Language.Symantic.Type.Root
  11 import Language.Symantic.Type.Type0
  12 import Language.Symantic.Type.Type2
  13
  14 -- * Type 'Type_Tuple2'
  15 -- | The @(,)@ type.
  16 type Type_Tuple2 = Type_Type2 (Proxy (,))
  17
  18 type instance Constraint2_of (Proxy (,))
  19  = Constraint2_Empty
  20
  21 pattern Type_Tuple2
  22  :: root a -> root b
  23  -> Type_Tuple2 root ((,) a b)
  24 pattern Type_Tuple2 a b
  25  = Type_Type2 Proxy a b
  26
  27 instance -- String_from_Type
  28  String_from_Type root =>
  29  String_from_Type (Type_Tuple2 root) where
  30         string_from_type (Type_Type2 _ a b) =
  31                 "("  ++ string_from_type a ++
  32                 ", " ++ string_from_type b ++ ")"
  33
  34 -- | Inject 'Type_Tuple2' within a root type.
  35 type_tuple2
  36  :: forall root h_a h_b.
  37  Lift_Type_Root Type_Tuple2 root
  38  => root h_a
  39  -> root h_b
  40  -> root (h_a, h_b)
  41 type_tuple2 a b = lift_type_root
  42          (Type_Tuple2 a b
  43          ::Type_Tuple2 root (h_a, h_b))