src/Symantic/Semantics/Forall.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE EmptyCase #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE QuantifiedConstraints #-}
   5 {-# LANGUAGE RankNTypes #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7
   8 module Symantic.Semantics.Forall where
   9
  10 import Control.Applicative (Applicative (..))
  11 import Control.Monad (Monad (..))
  12 import Data.Bool (Bool (..))
  13 import Data.Eq (Eq (..))
  14 import Data.Function ((.))
  15 import Data.Functor (Functor (..))
  16 import Data.Kind (Type)
  17 import Text.Show (Show (..))
  18
  19 import Symantic.Syntaxes.Classes (Syntax, Syntaxes, Unabstractable (..))
  20
  21 -- * Type 'Forall'
  22 newtype Forall (syns :: [Syntax]) (a :: Type)
  23   = Forall (forall sem. Syntaxes syns sem => sem a)
  24
  25 instance
  26   ( forall sem. Syntaxes syns sem => Functor sem
  27   ) =>
  28   Functor (Forall syns)
  29   where
  30   fmap f (Forall sem) = Forall (fmap f sem)
  31   a <$ (Forall sem) = Forall (a <$ sem)
  32 instance
  33   ( forall sem. Syntaxes syns sem => Applicative sem
  34   , Functor (Forall syns)
  35   ) =>
  36   Applicative (Forall syns)
  37   where
  38   pure a = Forall (pure a)
  39   liftA2 f (Forall a) (Forall b) = Forall (liftA2 f a b)
  40   (<*>) (Forall f) (Forall a) = Forall ((<*>) f a)
  41   (<*) (Forall f) (Forall a) = Forall ((<*) f a)
  42   (*>) (Forall f) (Forall a) = Forall ((*>) f a)
  43 instance
  44   ( forall sem. Syntaxes syns sem => Monad sem
  45   , Applicative (Forall syns)
  46   ) =>
  47   Monad (Forall syns)
  48   where
  49   (>>=) (Forall sa) f = Forall (sa >>= \a -> case f a of Forall sb -> sb)
  50   return = pure
  51   (>>) = (*>)
  52 instance
  53   (forall sem. Syntaxes syns sem => Unabstractable sem) =>
  54   Unabstractable (Forall syns)
  55   where
  56   Forall a2b .@ Forall a = Forall (a2b .@ a)
  57
  58 -- * Type 'PerSyntax'
  59 data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
  60   PerSyntaxZ :: a syn -> PerSyntax (syn ': syns) a
  61   PerSyntaxS :: PerSyntax syns a -> PerSyntax (skipSyn ': syns) a
  62
  63 instance Eq (PerSyntax '[] a) where
  64   (==) = \case {}
  65 instance
  66   ( Eq (a syn)
  67   , Eq (PerSyntax syns a)
  68   ) =>
  69   Eq (PerSyntax (syn ': syns) a)
  70   where
  71   PerSyntaxZ x == PerSyntaxZ y = x == y
  72   PerSyntaxS x == PerSyntaxS y = x == y
  73   _ == _ = False
  74
  75 instance Show (PerSyntax '[] a) where
  76   showsPrec _p = \case {}
  77 instance
  78   ( Show (a syn)
  79   , Show (PerSyntax syns a)
  80   ) =>
  81   Show (PerSyntax (syn ': syns) a)
  82   where
  83   showsPrec p = \case
  84     PerSyntaxZ a -> showsPrec p a
  85     PerSyntaxS s -> showsPrec p s
  86
  87 -- ** Class 'PerSyntaxable'
  88 class PerSyntaxable (syns :: [Syntax]) (syn :: Syntax) where
  89   perSyntax :: a syn -> PerSyntax syns a
  90 instance {-# OVERLAPS #-} PerSyntaxable (syn ': syns) syn where
  91   perSyntax = PerSyntaxZ
  92 instance PerSyntaxable syns syn => PerSyntaxable (skipSyn ': syns) syn where
  93   perSyntax = PerSyntaxS . perSyntax