Language/Symantic/Type/Var.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE PatternSynonyms #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# LANGUAGE ScopedTypeVariables #-}
   8 {-# LANGUAGE UndecidableInstances #-}
   9 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
  10 {-# OPTIONS_GHC -fno-warn-orphans #-}
  11 -- | Type variable.
  12 module Language.Symantic.Type.Var
  13  ( module Language.Symantic.Type.Var
  14  , module Language.Symantic.Lib.Data.Peano
  15  ) where
  16
  17 import qualified Data.MonoTraversable as MT
  18 import Data.Type.Equality ((:~:)(Refl))
  19
  20 import Language.Symantic.Lib.Data.Peano
  21 import Language.Symantic.Type.Root
  22 import Language.Symantic.Type.Type0
  23 import Language.Symantic.Type.Type1
  24
  25 -- * Type 'Var0'
  26 newtype Var0 = Var0 EPeano
  27 type instance Host0_of EPeano = Var0
  28
  29 -- | Undefined instance required to build errors.
  30 instance Eq Var0
  31 -- | Undefined instance required to build errors.
  32 instance Ord Var0
  33 -- | Undefined instance required to build errors.
  34 instance Monoid Var0
  35 instance Constraint_Type Eq             (Type_Var0 root)
  36 instance Constraint_Type Monoid         (Type_Var0 root)
  37 instance Constraint_Type Ord            (Type_Var0 root)
  38 instance Constraint_Type Num            (Type_Var0 root)
  39 instance Constraint_Type Integral       (Type_Var0 root)
  40 instance Constraint_Type MT.MonoFunctor (Type_Var0 root)
  41
  42 -- * Type 'Var1'
  43 newtype Var1 a = Var1 EPeano
  44 type instance Host1_of EPeano = Var1
  45
  46 -- * Type 'Type_Var0'
  47 -- | The variable type of kind @*@.
  48 type Type_Var0 = Type_Type0 EPeano
  49
  50 pattern Type_Var0 :: SPeano p -> Type_Var0 root Var0
  51 pattern Type_Var0 p = Type_Type0 (EPeano p)
  52
  53 instance Eq_Type1 (Type_Var0 root) where
  54 instance -- String_from_Type
  55  String_from_Type (Type_Var0 root) where
  56         string_from_type (Type_Type0 (EPeano p)) =
  57                 "t" ++ show (integral_from_peano p::Integer)
  58
  59 -- | Inject 'Type_Var0' within a root type.
  60 type_var0 :: Lift_Type_Root Type_Var0 root => SPeano p -> root Var0
  61 type_var0 = lift_type_root . Type_Type0 . EPeano
  62
  63 -- * Type 'Type_Var1'
  64 -- | The variable type of kind @* -> *@.
  65 type Type_Var1 = Type_Type1 EPeano
  66
  67 pattern Type_Var1 :: SPeano p -> root a -> Type_Var1 root (Var1 a)
  68 pattern Type_Var1 p a = Type_Type1 (EPeano p) a
  69
  70 instance Constraint_Type  Eq             (Type_Var1 root)
  71 instance Constraint_Type  Ord            (Type_Var1 root)
  72 instance Constraint_Type  Monoid         (Type_Var1 root)
  73 instance Constraint_Type  Num            (Type_Var1 root)
  74 instance Constraint_Type  Integral       (Type_Var1 root)
  75 instance Constraint_Type  MT.MonoFunctor (Type_Var1 root)
  76 instance Constraint_Type1 Applicative    (Type_Var1 root)
  77 instance Constraint_Type1 Foldable       (Type_Var1 root)
  78 instance Constraint_Type1 Functor        (Type_Var1 root)
  79 instance Constraint_Type1 Monad          (Type_Var1 root)
  80 instance Constraint_Type1 Traversable    (Type_Var1 root)
  81 instance Eq_Type1 (Type_Var1 root) where
  82         eq_type1 (Type_Type1 p1 _) (Type_Type1 p2 _)
  83          | p1 == p2
  84          = Just Refl
  85         eq_type1 _ _ = Nothing
  86 instance -- String_from_Type
  87  String_from_Type root =>
  88  String_from_Type (Type_Var1 root) where
  89         string_from_type (Type_Type1 (EPeano p) a) =
  90                 "t_" ++ show (integral_from_peano p::Integer) ++
  91                 " " ++ string_from_type a
  92
  93 -- | Inject 'Type_Var1' within a root type.
  94 type_var1 :: Lift_Type_Root Type_Var1 root => SPeano p -> root a -> root (Var1 a)
  95 type_var1 p = lift_type_root . Type_Var1 p