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 (Syntax, Syntaxes, Unabstractable (..), Abstractable(..))
  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 => Unabstractable sem) =>
  60   Unabstractable (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 => Unabstractable sem
  66   ) =>
  67   Abstractable (Forall syns)
  68   where
  69   lam f = Forall (lam (\a -> let Forall b = f (forallSem a) in b))
  70     where
  71       -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
  72       forallSem :: sem a -> Forall syns a
  73       forallSem a = Forall (unsafeCoerce a)
  74
  75 -- * Type 'PerSyntax'
  76 data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
  77   PerSyntaxZ :: a syn -> PerSyntax (syn ': syns) a
  78   PerSyntaxS :: PerSyntax syns a -> PerSyntax (skipSyn ': syns) a
  79
  80 instance Eq (PerSyntax '[] a) where
  81   (==) = \case {}
  82 instance
  83   ( Eq (a syn)
  84   , Eq (PerSyntax syns a)
  85   ) =>
  86   Eq (PerSyntax (syn ': syns) a)
  87   where
  88   PerSyntaxZ x == PerSyntaxZ y = x == y
  89   PerSyntaxS x == PerSyntaxS y = x == y
  90   _ == _ = False
  91
  92 instance Show (PerSyntax '[] a) where
  93   showsPrec _p = \case {}
  94 instance
  95   ( Show (a syn)
  96   , Show (PerSyntax syns a)
  97   ) =>
  98   Show (PerSyntax (syn ': syns) a)
  99   where
 100   showsPrec p = \case
 101     PerSyntaxZ a -> showsPrec p a
 102     PerSyntaxS s -> showsPrec p s
 103
 104 -- ** Class 'PerSyntaxable'
 105 class PerSyntaxable (syns :: [Syntax]) (syn :: Syntax) where
 106   perSyntax :: a syn -> PerSyntax syns a
 107 instance {-# OVERLAPS #-} PerSyntaxable (syn ': syns) syn where
 108   perSyntax = PerSyntaxZ
 109 instance PerSyntaxable syns syn => PerSyntaxable (skipSyn ': syns) syn where
 110   perSyntax = PerSyntaxS . perSyntax