TFHOE/Expr/Common.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE ExistentialQuantification #-}
   3 {-# LANGUAGE KindSignatures #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE Rank2Types #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeFamilies #-}
   8 module TFHOE.Expr.Common where
   9
  10 import Data.Proxy (Proxy(..))
  11 import GHC.Prim (Constraint)
  12
  13 import TFHOE.Type
  14
  15 -- * Class 'Expr_from'
  16
  17 class Expr_from raw (ty:: {-h-}* -> *) (ty_end:: {-h-}* -> *) where
  18         expr_from
  19          :: forall hs ret
  20          .  Proxy ty
  21          -> Proxy ty_end
  22          -> Context (Var ty_end) hs
  23          -> raw
  24          -> (forall h. ty_end h -> Forall_Repr_with_Context ty_end hs h
  25                                 -> Either Error_Type ret)
  26          -> Either Error_Type ret
  27
  28 -- ** Type 'Expr_from_Type'
  29
  30 -- | A type family recursively accumulating the expressions
  31 -- an interpreter will have to support.
  32 type family   Expr_from_Type (ty:: * -> *) (repr:: * -> *) :: Constraint
  33 type instance Expr_from_Type Type_End repr = ()
  34
  35 -- ** Type 'Forall_Repr_with_Context'
  36
  37 -- | A data type embedding a universal quantification over @repr@
  38 -- to construct an expression polymorphic enough to stay
  39 -- interpretable by different interpreters;
  40 -- moreover the expression is abstracted by a 'Context'
  41 -- built at parsing time.
  42 data Forall_Repr_with_Context ty hs h
  43  =   Forall_Repr_with_Context
  44  (   forall repr. Expr_from_Type ty repr =>
  45                   Context repr hs -> repr h )
  46
  47 -- ** Type 'Forall_Repr'
  48
  49 data Forall_Repr ty h
  50  =   Forall_Repr
  51  { unForall_Repr :: forall repr
  52                  .  Expr_from_Type ty repr
  53                  => repr h }