TFHOE/Type/Common.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE ExistentialQuantification #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE GADTs #-}
   5 {-# LANGUAGE KindSignatures #-}
   6 {-# LANGUAGE MultiParamTypeClasses #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# LANGUAGE TypeOperators #-}
  10 module TFHOE.Type.Common where
  11
  12 import Data.Maybe (isJust)
  13 import Data.Type.Equality ((:~:)(Refl))
  14
  15 -- * Class 'Type_Eq'
  16
  17 -- | Test two types for equality,
  18 -- returning an Haskell type-level proof
  19 -- of the equality when it holds.
  20 class Type_Eq ty where
  21         type_eq :: forall h1 h2. ty h1 -> ty h2 -> Maybe (h1 :~: h2)
  22
  23 -- * Class 'Type_from'
  24
  25 class Type_Eq ty => Type_from raw ty where
  26         type_from
  27          :: raw
  28          -> (forall h. ty h -> Either Error_Type ret)
  29          -> Either Error_Type ret
  30
  31 type Error_Type = String
  32
  33 -- * Class 'String_from_Type'
  34
  35 class String_from_Type ty where
  36         string_from_type :: ty h -> String
  37
  38 -- * Type 'Var'
  39
  40 -- | Join a name and a type;
  41 -- used to handle lambda variables by name
  42 -- (and not DeBruijn indices).
  43 data Var ty h
  44  =   Var String (ty h)
  45
  46 -- * Type 'Context'
  47
  48 -- | GADT for a typing context,
  49 -- accumulating an @item@ at each lambda;
  50 -- used to accumulate object-types of lambda variables in 'Expr_from'
  51 -- or meta-terms of lambda variables in 'Repr_Host'.
  52 data Context :: (* -> *) -> [*] -> * where
  53         Context_Empty :: Context item '[]
  54         Context_Next  :: item h -> Context item hs -> Context item (h ': hs)
  55 infixr 5 `Context_Next`
  56
  57 -- ** Type 'Type_End'
  58
  59 -- | Close an extensible type.
  60 data Type_End h where
  61         Type_End :: Type_End ()
  62
  63 instance Type_Eq Type_End where
  64         type_eq Type_End Type_End = Just Refl
  65 instance Eq (Type_End h) where
  66         _ == _ = True
  67 instance String_from_Type Type_End where
  68         string_from_type _ = ""
  69 instance Type_from raw Type_End where
  70         type_from _raw k = k Type_End
  71
  72 -- * Type 'Exists_Type'
  73
  74 -- | Existential data type to wrap an indexed type.
  75 data Exists_Type ty
  76  = forall h. Exists_Type (ty h)
  77 instance -- Eq
  78  Type_Eq ty =>
  79  Eq (Exists_Type ty) where
  80         Exists_Type xh == Exists_Type yh =
  81                 isJust $ type_eq xh yh
  82 instance -- Show
  83  String_from_Type ty =>
  84  Show (Exists_Type ty) where
  85         show (Exists_Type ty) = string_from_type ty
  86
  87 -- * Type 'Exists_Type_and_Repr'
  88
  89 data Exists_Type_and_Repr ty repr
  90  =   forall h.
  91      Exists_Type_and_Repr (ty h) (repr h)