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 Control.Monad.Trans.Except qualified as MT
  11 import Control.Monad.Trans.Reader qualified as MT
  12 import Control.Monad.Trans.State qualified as MT
  13 import Data.Bool (otherwise)
  14 import Data.Either (Either (..))
  15 import Data.Eq (Eq (..))
  16 import Data.Function (id, ($), (.))
  17 import Data.Functor (Functor (..), (<$>))
  18 import Data.Functor.Constant (Constant (..))
  19 import Data.Int (Int)
  20 import Data.Kind (Constraint, Type)
  21 import Data.Maybe (Maybe (..), isJust)
  22 import Data.Proxy (Proxy (..))
  23 import Data.Semigroup (Semigroup (..))
  24 import Data.String (String)
  25 import GHC.Types
  26 import Text.Read (Read (..), reads)
  27 import Text.Show (Show (..))
  28 import Unsafe.Coerce (unsafeCoerce)
  29 import Prelude (error)
  30 import Prelude qualified
  31
  32 import Symantic.Typer
  33
  34 type Semantic = Type -> Type
  35 type Syntax = Semantic -> Constraint
  36
  37 data ForallSem (syn :: Syntax) (a :: Type) = ForallSem {unForallSem :: forall sem. syn sem => sem a}
  38
  39 instance
  40   ( forall sem. syn sem => Functor sem
  41   ) =>
  42   Functor (ForallSem syn)
  43   where
  44   fmap f (ForallSem sem) = ForallSem (fmap f sem)
  45   a <$ (ForallSem sem) = ForallSem (a <$ sem)
  46 instance
  47   ( forall sem. syn sem => Applicative sem
  48   , Functor (ForallSem syn)
  49   ) =>
  50   Applicative (ForallSem syn)
  51   where
  52   pure a = ForallSem (pure a)
  53   liftA2 f (ForallSem a) (ForallSem b) = ForallSem (liftA2 f a b)
  54   (<*>) (ForallSem f) (ForallSem a) = ForallSem ((<*>) f a)
  55   (<*) (ForallSem f) (ForallSem a) = ForallSem ((<*) f a)
  56   (*>) (ForallSem f) (ForallSem a) = ForallSem ((*>) f a)
  57 instance
  58   ( forall sem. syn sem => Monad sem
  59   , Applicative (ForallSem syn)
  60   ) =>
  61   Monad (ForallSem syn)
  62   where
  63   (>>=) (ForallSem sa) f = ForallSem (sa >>= \a -> case f a of ForallSem sb -> sb)
  64   return = pure
  65   (>>) = (*>)
  66
  67 -- * Interpreter 'Parser'
  68 data TermVT syn = forall vs a.
  69   TermVT
  70   { typeTermVT :: Ty () vs a
  71   , unTermVT :: ForallSem syn a
  72   }