]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Type/Tuple.hs
init
[haskell/symantic.git] / Language / Symantic / Type / Tuple.hs
1 {-# LANGUAGE FlexibleContexts #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE MultiParamTypeClasses #-}
4 {-# LANGUAGE OverloadedStrings #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeFamilies #-}
7 module Language.Symantic.Type.Tuple where
8
9 import Data.Maybe (isJust)
10 import Data.Type.Equality ((:~:)(Refl))
11
12 import Language.Symantic.Type.Common
13 import Language.Symantic.Type.Fun
14 import Language.Symantic.Type.Bool
15 import Language.Symantic.Type.Var
16
17 -- * Type 'Type_Tuple2'
18 -- | The 'Tuple' type.
19 data Type_Tuple2 root h where
20 Type_Tuple2 :: root h_a
21 -> root h_b
22 -> Type_Tuple2 root (h_a, h_b)
23
24 type instance Root_of_Type (Type_Tuple2 root) = root
25 type instance Error_of_Type ast (Type_Tuple2 root) = No_Error_Type
26
27 instance -- Eq_Type
28 Eq_Type root =>
29 Eq_Type (Type_Tuple2 root) where
30 eq_type (Type_Tuple2 a1 b1) (Type_Tuple2 a2 b2)
31 | Just Refl <- a1 `eq_type` a2
32 , Just Refl <- b1 `eq_type` b2
33 = Just Refl
34 eq_type _ _ = Nothing
35 instance -- Eq
36 Eq_Type root =>
37 Eq (Type_Tuple2 root h) where
38 x == y = isJust $ eq_type x y
39 instance -- String_from_Type
40 String_from_Type root =>
41 String_from_Type (Type_Tuple2 root) where
42 string_from_type (Type_Tuple2 a b) =
43 "Tuple (" ++ string_from_type a ++
44 ", " ++ string_from_type b ++ ")"
45 instance -- Show
46 String_from_Type root =>
47 Show (Type_Tuple2 root h) where
48 show = string_from_type
49
50 -- | Convenient alias to include a 'Type_Tuple2' within a type.
51 type_tuple2
52 :: Type_Root_Lift Type_Tuple2 root
53 => root h_a
54 -> root h_b
55 -> root (h_a, h_b)
56 type_tuple2 a b = type_root_lift (Type_Tuple2 a b)
57
58 -- * Type 'Type_Fun_Bool_Tuple2'
59 -- | Convenient alias.
60 type Type_Fun_Bool_Tuple2 lam
61 = Type_Root (Type_Alt Type_Var
62 (Type_Alt (Type_Fun lam)
63 (Type_Alt Type_Bool
64 Type_Tuple2)))