Language/Symantic/Typing/Type.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE GADTs #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE PolyKinds #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE StandaloneDeriving #-}
  10 {-# LANGUAGE TypeFamilies #-}
  11 {-# LANGUAGE TypeOperators #-}
  12 {-# LANGUAGE TypeInType #-}
  13 {-# LANGUAGE UndecidableInstances #-}
  14 module Language.Symantic.Typing.Type where
  15
  16 import Data.Monoid ((<>))
  17 import Data.Proxy
  18 import Data.Maybe (fromMaybe, isJust)
  19 import Data.Type.Equality
  20 import qualified Data.Kind as K
  21
  22 import Language.Symantic.Typing.Kind
  23 import Language.Symantic.Typing.Constant
  24 import Language.Symantic.Typing.Syntax
  25
  26 -- * Type 'Type'
  27
  28 -- | /Type of terms/.
  29 --
  30 -- * @cs@: /type constants/, fixed at compile time.
  31 -- * @h@: indexed Haskell type.
  32 --
  33 -- * 'TyConst': /type constant/, selected amongst @cs@.
  34 -- * @(:$)@: /type application/.
  35 data Type (cs::[K.Type]) (h::k) where
  36         TyConst
  37          :: Const cs c
  38          -> Type  cs c
  39         (:$)
  40          :: Type cs f
  41          -> Type cs x
  42          -> Type cs (f x)
  43         {-
  44         TyVar
  45          :: SKind k
  46          -> Type cs (v::k)
  47         -}
  48 infixl 9 :$
  49
  50 instance TestEquality (Type cs) where
  51         testEquality = eq_type
  52 instance Eq (Type cs h) where
  53         _x == _y = True
  54 instance Show_Const cs => Show (Type cs h) where
  55         show = show_type
  56 -- deriving instance Show_Const cs => Show (Type cs h)
  57
  58 kind_of :: Type cs (h::k) -> SKind k
  59 kind_of t =
  60         case t of
  61          TyConst c -> kind_of_const c
  62          f :$ _x ->
  63                 case kind_of f of
  64                  _kx `SKiArrow` kf -> kf
  65
  66 eq_type
  67  :: Type cs (x::k) -> Type cs (y::k) -> Maybe (x:~:y)
  68 eq_type (TyConst x) (TyConst y)
  69  | Just Refl <- testEquality x y
  70  = Just Refl
  71 eq_type (xf :$ xx) (yf :$ yx)
  72  | Just Refl <- eq_skind (kind_of xf) (kind_of yf)
  73  , Just Refl <- eq_type xf yf
  74  , Just Refl <- eq_type xx yx
  75  = Just Refl
  76 eq_type _ _ = Nothing
  77
  78 eq_kind_type
  79  :: Type cs (x::kx) -> Type cs (y::ky) -> Maybe (kx:~:ky)
  80 eq_kind_type (TyConst x) (TyConst y)
  81  | Just Refl <- eq_kind_const x y
  82  = Just Refl
  83 eq_kind_type (xf :$ xx) (yf :$ yx)
  84  | Just Refl <- eq_kind_type xf yf
  85  , Just Refl <- eq_kind_type xx yx
  86  = Just Refl
  87 eq_kind_type _x _y = Nothing
  88
  89 show_type :: Show_Const cs => Type cs h -> String
  90 show_type (TyConst c) = show c
  91 show_type ((:$) f@(:$){} a@(:$){}) = "(" <> show_type f <> ") (" <> show_type a <> ")"
  92 show_type ((:$) f@(:$){} a) = "(" <> show_type f <> ") " <> show_type a
  93 show_type ((:$) f a@(:$){}) = show_type f <> " (" <> show_type a <> ")"
  94 show_type ((:$) f a) = show_type f <> " " <> show_type a
  95 -- show_type (TyVar v) = "t" <> show (integral_from_peano v::Integer)
  96
  97 -- * Type 'EType'
  98 -- | Existential for 'Type'.
  99 data EType cs = forall h. EType (Type cs h)
 100
 101 instance Eq (EType cs) where
 102         EType x == EType y
 103          | Just Refl <- eq_kind_type x y
 104          = isJust $ eq_type x y
 105         _x == _y = False
 106 instance Show_Const cs => Show (EType cs) where
 107         show (EType ty) = show ty
 108
 109 -- * Type 'KType'
 110 -- | Existential for 'Type' of a known 'Kind'.
 111 data KType cs k = forall (h::k). KType (Type cs h)
 112
 113 instance Eq (KType cs ki) where
 114         KType x == KType y = isJust $ eq_type x y
 115 instance Show_Const cs => Show (KType cs ki) where
 116         show (KType ty) = show_type ty
 117
 118 -- * Class 'Type_from'
 119 -- | Try to build a 'Type' from raw data.
 120 class Type_from ast cs where
 121         type_from
 122          :: ast
 123          -> (forall k h. Type cs (h::k) -> Either (Error_Type cs ast) ret)
 124          -> Either (Error_Type cs ast) ret
 125
 126 -- ** Type 'Error_Type'
 127 data Error_Type cs ast
 128  =   Error_Type_Constant_unknown    (At ast (Lexem ast))
 129  |   Error_Type_Kind_mismatch       (At ast EKind) (At ast EKind)
 130  |   Error_Type_Kind_not_applicable (At ast EKind)
 131 deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Type cs ast)
 132 deriving instance (Show ast, Show (Lexem ast), Show_Const cs) => Show (Error_Type cs ast)
 133
 134 instance
 135  ( Const_from (Lexem ast) cs
 136  , AST ast
 137  ) => Type_from ast cs where
 138         type_from ast kk =
 139                 fromMaybe (Left $ Error_Type_Constant_unknown $ At (Just ast) $ ast_lexem ast) $
 140                 const_from (ast_lexem ast) $ \c -> Just $
 141                 go (ast_nodes ast) (TyConst c) kk
 142                 where
 143                 go :: [ast]
 144                  -> Type cs h
 145                  -> (forall k' h'. Type cs (h'::k') -> Either (Error_Type cs ast) ret)
 146                  -> Either (Error_Type cs ast) ret
 147                 go [] ty k = k ty
 148                 go (ast_x:ast_xs) ty_f k =
 149                         type_from ast_x $ \ty_x ->
 150                         case kind_of ty_f of
 151                          ki_f_a `SKiArrow` _ki_f_b ->
 152                                 let ki_x = kind_of ty_x in
 153                                 case eq_skind ki_f_a ki_x of
 154                                  Just Refl -> go ast_xs (ty_f :$ ty_x) k
 155                                  Nothing -> Left $ Error_Type_Kind_mismatch
 156                                          (At (Just ast)   $ EKind ki_f_a)
 157                                          (At (Just ast_x) $ EKind ki_x)
 158                          ki -> Left $ Error_Type_Kind_not_applicable $ At (Just ast) $ EKind ki
 159
 160 -- * Type 'Args'
 161 data Args (cs::[K.Type]) (args::[K.Type]) where
 162         ArgZ :: Args cs '[]
 163         ArgS :: Type cs arg
 164              -> Args cs args
 165              -> Args cs (Proxy arg ': args)
 166 infixr 5 `ArgS`
 167
 168 -- | Build the left spine of a 'Type'.
 169 spine_of_type
 170  :: Type cs h
 171  -> (forall kc (c::kc) as. Const cs c -> Args cs as -> ret) -> ret
 172 spine_of_type (TyConst c) k = k c ArgZ
 173 spine_of_type (f :$ a) k = spine_of_type f $ \c as -> k c (a `ArgS` as)
 174
 175 -- * Usual 'Type's
 176
 177 -- | The '()' 'Type'
 178 tyUnit :: Inj_Const cs () => Type cs ()
 179 tyUnit = TyConst inj_const