]> Git — Sourcephile - haskell/symantic-base.git/blob - src/Symantic/Semantics/Forall.hs
impl: fix `Unabstractable` instance for `SomeData`
[haskell/symantic-base.git] / 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