src/Symantic/Compiler/Term.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE QuantifiedConstraints #-}
   3 {-# LANGUAGE RankNTypes #-}
   4 {-# LANGUAGE UndecidableInstances #-}
   5
   6 module Symantic.Compiler.Term where
   7
   8 import Control.Applicative (Applicative (..))
   9 import Control.Monad (Monad (..))
  10 import Data.Functor (Functor (..))
  11 import GHC.Types (Constraint, Type)
  12
  13 import Symantic.Typer.Type (Ty)
  14
  15 type Semantic = GHC.Types.Type -> GHC.Types.Type
  16 type Syntax = Semantic -> GHC.Types.Constraint
  17
  18 data ForallSem (syn :: Syntax) (a :: GHC.Types.Type) = ForallSem {unForallSem :: forall sem. syn sem => sem a}
  19
  20 instance
  21   ( forall sem. syn sem => Functor sem
  22   ) =>
  23   Functor (ForallSem syn)
  24   where
  25   fmap f (ForallSem sem) = ForallSem (fmap f sem)
  26   a <$ (ForallSem sem) = ForallSem (a <$ sem)
  27 instance
  28   ( forall sem. syn sem => Applicative sem
  29   , Functor (ForallSem syn)
  30   ) =>
  31   Applicative (ForallSem syn)
  32   where
  33   pure a = ForallSem (pure a)
  34   liftA2 f (ForallSem a) (ForallSem b) = ForallSem (liftA2 f a b)
  35   (<*>) (ForallSem f) (ForallSem a) = ForallSem ((<*>) f a)
  36   (<*) (ForallSem f) (ForallSem a) = ForallSem ((<*) f a)
  37   (*>) (ForallSem f) (ForallSem a) = ForallSem ((*>) f a)
  38 instance
  39   ( forall sem. syn sem => Monad sem
  40   , Applicative (ForallSem syn)
  41   ) =>
  42   Monad (ForallSem syn)
  43   where
  44   (>>=) (ForallSem sa) f = ForallSem (sa >>= \a -> case f a of ForallSem sb -> sb)
  45   return = pure
  46   (>>) = (*>)
  47
  48 -- * Interpreter 'Parser'
  49 data TermVT syn = forall vs a.
  50   TermVT
  51   { typeTermVT :: Ty () vs a
  52   , unTermVT :: ForallSem syn a
  53   }