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 -- | This module provides the 'Forall' semantic
   9 -- which preserves the polymorphism of the semantic.
  10 -- Useful when parsing the syntax from a text
  11 -- (ie. when the domain-specific language
  12 -- is not embedded into a Haskell file).
  13 module Symantic.Semantics.Forall where
  14
  15 import Control.Applicative (Applicative (..))
  16 import Control.Monad (Monad (..))
  17 import Data.Bool (Bool (..))
  18 import Data.Eq (Eq (..))
  19 import Data.Function ((.))
  20 import Data.Functor (Functor (..))
  21 import Data.Kind (Type)
  22 import Text.Show (Show (..))
  23 import Unsafe.Coerce (unsafeCoerce)
  24
  25 import Symantic.Syntaxes.Classes (Abstractable (..), Syntax, Syntaxes, Instantiable (..), Unabstractable (..))
  26
  27 -- * Type 'Forall'
  28 newtype Forall (syns :: [Syntax]) (a :: Type)
  29   = Forall (forall sem. Syntaxes syns sem => sem a)
  30
  31 instance
  32   ( forall sem. Syntaxes syns sem => Functor sem
  33   ) =>
  34   Functor (Forall syns)
  35   where
  36   fmap f (Forall sem) = Forall (fmap f sem)
  37   a <$ (Forall sem) = Forall (a <$ sem)
  38 instance
  39   ( forall sem. Syntaxes syns sem => Applicative sem
  40   , Functor (Forall syns)
  41   ) =>
  42   Applicative (Forall syns)
  43   where
  44   pure a = Forall (pure a)
  45   liftA2 f (Forall a) (Forall b) = Forall (liftA2 f a b)
  46   (<*>) (Forall f) (Forall a) = Forall ((<*>) f a)
  47   (<*) (Forall f) (Forall a) = Forall ((<*) f a)
  48   (*>) (Forall f) (Forall a) = Forall ((*>) f a)
  49 instance
  50   ( forall sem. Syntaxes syns sem => Monad sem
  51   , Applicative (Forall syns)
  52   ) =>
  53   Monad (Forall syns)
  54   where
  55   (>>=) (Forall sa) f = Forall (sa >>= \a -> case f a of Forall sb -> sb)
  56   return = pure
  57   (>>) = (*>)
  58 instance
  59   (forall sem. Syntaxes syns sem => Instantiable sem) =>
  60   Instantiable (Forall syns)
  61   where
  62   Forall a2b .@ Forall a = Forall (a2b .@ a)
  63 instance
  64   ( forall sem. Syntaxes syns sem => Abstractable sem
  65   , forall sem. Syntaxes syns sem => Instantiable sem
  66   ) => Abstractable (Forall syns) where
  67   lam f = Forall (lam (\a -> let Forall b = f (forallSem a) in b))
  68     where
  69       -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
  70       forallSem :: sem a -> Forall syns a
  71       forallSem a = Forall (unsafeCoerce a)
  72
  73 -- * Type 'PerSyntax'
  74 data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
  75   PerSyntaxZ :: a syn -> PerSyntax (syn ': syns) a
  76   PerSyntaxS :: PerSyntax syns a -> PerSyntax (skipSyn ': syns) a
  77
  78 instance Eq (PerSyntax '[] a) where
  79   (==) = \case {}
  80 instance
  81   ( Eq (a syn)
  82   , Eq (PerSyntax syns a)
  83   ) =>
  84   Eq (PerSyntax (syn ': syns) a)
  85   where
  86   PerSyntaxZ x == PerSyntaxZ y = x == y
  87   PerSyntaxS x == PerSyntaxS y = x == y
  88   _ == _ = False
  89
  90 instance Show (PerSyntax '[] a) where
  91   showsPrec _p = \case {}
  92 instance
  93   ( Show (a syn)
  94   , Show (PerSyntax syns a)
  95   ) =>
  96   Show (PerSyntax (syn ': syns) a)
  97   where
  98   showsPrec p = \case
  99     PerSyntaxZ a -> showsPrec p a
 100     PerSyntaxS s -> showsPrec p s
 101
 102 -- ** Class 'PerSyntaxable'
 103 class PerSyntaxable (syns :: [Syntax]) (syn :: Syntax) where
 104   perSyntax :: a syn -> PerSyntax syns a
 105 instance {-# OVERLAPS #-} PerSyntaxable (syn ': syns) syn where
 106   perSyntax = PerSyntaxZ
 107 instance PerSyntaxable syns syn => PerSyntaxable (skipSyn ': syns) syn where
 108   perSyntax = PerSyntaxS . perSyntax