]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Type/Var.hs
init
[haskell/symantic.git] / Language / Symantic / Type / Var.hs
1 {-# LANGUAGE FlexibleContexts #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE MultiParamTypeClasses #-}
4 {-# LANGUAGE Rank2Types #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE TypeFamilies #-}
7 {-# LANGUAGE TypeOperators #-}
8 {-# LANGUAGE UndecidableInstances #-}
9 -- | Type variable.
10 module Language.Symantic.Type.Var
11 ( module Language.Symantic.Type.Var
12 , module Language.Symantic.Lib.Data.Peano
13 ) where
14
15 import Data.Maybe (isJust)
16
17 import Language.Symantic.Type.Common
18 import Language.Symantic.Lib.Data.Peano
19
20 -- * Type 'Type_Var'
21 -- | The variable type.
22 data Type_Var (root:: * -> *) p where
23 Type_Var :: SPeano p -> Type_Var root p
24 type instance Root_of_Type (Type_Var root) = root
25 type instance Error_of_Type ast (Type_Var root) = ()
26
27 instance -- Type_Eq
28 Type_Eq (Type_Var root) where
29 type_eq (Type_Var x) (Type_Var y) = x `peano_eq` y
30 instance -- Eq
31 Eq (Type_Var root h) where
32 x == y = isJust $ x `type_eq` y
33 instance -- String_from_Type
34 String_from_Type (Type_Var root) where
35 string_from_type (Type_Var p) =
36 "t" ++ show (integral_from_peano p::Integer)
37 instance -- Show
38 Show (Type_Var root h) where
39 show = string_from_type
40 instance Type_Constraint Eq (Type_Var root)
41 instance Type_Constraint Ord (Type_Var root)
42
43 -- | Convenient alias to include a 'Type_Var' within a type.
44 type_var :: Type_Root_Lift Type_Var root => SPeano p -> root p
45 type_var = type_root_lift . Type_Var