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 import Language.Symantic.Type.Constraint
  25 import Language.Symantic.Type.Family
  26
  27 -- * Type 'Var0'
  28 newtype Var0 = Var0 EPeano
  29 type instance Host0_of EPeano = Var0
  30
  31 -- | Undefined instance required to build errors.
  32 instance Eq Var0
  33 -- | Undefined instance required to build errors.
  34 instance Ord Var0
  35 -- | Undefined instance required to build errors.
  36 instance Monoid Var0
  37
  38 -- * Type 'Var1'
  39 newtype Var1 a = Var1 EPeano
  40 type instance Host1_of EPeano = Var1
  41
  42 -- * Type 'Type_Var0'
  43 -- | The variable type of kind @*@.
  44 type Type_Var0 = Type0 EPeano
  45
  46 pattern Type_Var0 :: SPeano p -> Type_Var0 root Var0
  47 pattern Type_Var0 p = Type0 (EPeano p)
  48
  49 instance Type1_Eq (Type_Var0 root) where
  50 instance Type0_Constraint Eq             (Type_Var0 root)
  51 instance Type0_Constraint Monoid         (Type_Var0 root)
  52 instance Type0_Constraint Ord            (Type_Var0 root)
  53 instance Type0_Constraint Num            (Type_Var0 root)
  54 instance Type0_Constraint Integral       (Type_Var0 root)
  55 instance Type0_Constraint MT.MonoFunctor (Type_Var0 root)
  56 instance Type0_Family Type_Family_MonoElement (Type_Var0 root)
  57 instance String_from_Type (Type_Var0 root) where
  58         string_from_type (Type0 (EPeano p)) =
  59                 "t" ++ show (integral_from_peano p::Integer)
  60
  61 -- | Inject 'Type_Var0' within a root type.
  62 type_var0 :: Type_Root_Lift Type_Var0 root => SPeano p -> root Var0
  63 type_var0 = type_root_lift . Type0 . EPeano
  64
  65 -- * Type 'Type_Var1'
  66 -- | The variable type of kind @* -> *@.
  67 type Type_Var1 = Type1 EPeano
  68
  69 pattern Type_Var1 :: SPeano p -> root a -> Type_Var1 root (Var1 a)
  70 pattern Type_Var1 p a = Type1 (EPeano p) a
  71
  72 instance Type0_Constraint Eq             (Type_Var1 root)
  73 instance Type0_Constraint Ord            (Type_Var1 root)
  74 instance Type0_Constraint Monoid         (Type_Var1 root)
  75 instance Type0_Constraint Num            (Type_Var1 root)
  76 instance Type0_Constraint Integral       (Type_Var1 root)
  77 instance Type0_Constraint MT.MonoFunctor (Type_Var1 root)
  78 instance Type1_Constraint Applicative    (Type_Var1 root)
  79 instance Type1_Constraint Foldable       (Type_Var1 root)
  80 instance Type1_Constraint Functor        (Type_Var1 root)
  81 instance Type1_Constraint Monad          (Type_Var1 root)
  82 instance Type1_Constraint Traversable    (Type_Var1 root)
  83 instance Type0_Family Type_Family_MonoElement (Type_Var1 root)
  84 instance Type1_Eq (Type_Var1 root) where
  85         type1_eq (Type1 p1 _) (Type1 p2 _) | p1 == p2 = Just Refl
  86         type1_eq _ _ = Nothing
  87 instance -- String_from_Type
  88  String_from_Type root =>
  89  String_from_Type (Type_Var1 root) where
  90         string_from_type (Type1 (EPeano p) a) =
  91                 "t_" ++ show (integral_from_peano p::Integer) ++
  92                 " " ++ string_from_type a
  93
  94 -- | Inject 'Type_Var1' within a root type.
  95 type_var1 :: Type_Root_Lift Type_Var1 root => SPeano p -> root a -> root (Var1 a)
  96 type_var1 p = type_root_lift . Type_Var1 p