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.Functor (Functor (..))
  20 import Data.Kind (Type)
  21 import Text.Show (Show (..))
  22 import Unsafe.Coerce (unsafeCoerce)
  23 import qualified Data.Function as Fun
  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   ) => Functor (Forall syns) where
  34   fmap f (Forall sem) = Forall (fmap f sem)
  35   a <$ (Forall sem) = Forall (a <$ sem)
  36 instance
  37   ( forall sem. Syntaxes syns sem => Applicative sem
  38   , Functor (Forall syns)
  39   ) => Applicative (Forall syns) where
  40   pure a = Forall (pure a)
  41   liftA2 f (Forall a) (Forall b) = Forall (liftA2 f a b)
  42   (<*>) (Forall f) (Forall a) = Forall ((<*>) f a)
  43   (<*) (Forall f) (Forall a) = Forall ((<*) f a)
  44   (*>) (Forall f) (Forall a) = Forall ((*>) f a)
  45 instance
  46   ( forall sem. Syntaxes syns sem => Monad sem
  47   , Applicative (Forall syns)
  48   ) => Monad (Forall syns) 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 => Instantiable sem) =>
  54   Instantiable (Forall syns)
  55   where
  56   Forall a2b .@ Forall a = Forall (a2b .@ a)
  57 instance
  58   ( forall sem. Syntaxes syns sem => Abstractable sem
  59   , forall sem. Syntaxes syns sem => Instantiable sem
  60   ) => Abstractable (Forall syns) where
  61   lam f = Forall (lam (\a -> let Forall b = f (forallSem a) in b))
  62     where
  63       -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
  64       forallSem :: sem a -> Forall syns a
  65       forallSem a = Forall (unsafeCoerce a)
  66 instance
  67   ( forall sem. Syntaxes syns sem => Unabstractable sem
  68   ) => Unabstractable (Forall syns) where
  69   ap = Forall ap
  70   const = Forall const
  71   id = Forall id
  72   (.) = Forall (.)
  73   flip = Forall flip
  74   ($) = Forall ($)
  75
  76 -- * Type 'PerSyntax'
  77 data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
  78   PerSyntaxZ :: a syn -> PerSyntax (syn ': syns) a
  79   PerSyntaxS :: PerSyntax syns a -> PerSyntax (skipSyn ': syns) a
  80
  81 instance Eq (PerSyntax '[] a) where
  82   (==) = \case {}
  83 instance
  84   ( Eq (a syn)
  85   , Eq (PerSyntax syns a)
  86   ) =>
  87   Eq (PerSyntax (syn ': syns) a)
  88   where
  89   PerSyntaxZ x == PerSyntaxZ y = x == y
  90   PerSyntaxS x == PerSyntaxS y = x == y
  91   _ == _ = False
  92
  93 instance Show (PerSyntax '[] a) where
  94   showsPrec _p = \case {}
  95 instance
  96   ( Show (a syn)
  97   , Show (PerSyntax syns a)
  98   ) =>
  99   Show (PerSyntax (syn ': syns) a)
 100   where
 101   showsPrec p = \case
 102     PerSyntaxZ a -> showsPrec p a
 103     PerSyntaxS s -> showsPrec p s
 104
 105 -- ** Class 'PerSyntaxable'
 106 class PerSyntaxable (syns :: [Syntax]) (syn :: Syntax) where
 107   perSyntax :: a syn -> PerSyntax syns a
 108 instance {-# OVERLAPS #-} PerSyntaxable (syn ': syns) syn where
 109   perSyntax = PerSyntaxZ
 110 instance PerSyntaxable syns syn => PerSyntaxable (skipSyn ': syns) syn where
 111   perSyntax = PerSyntaxS Fun.. perSyntax