Recognizing context free grammars based on https://www.well-typed.com/blog/2020/06/fix-ing-regular-expressions/#references

Gram.hs

{- cabal:
build-depends: base, liquidhaskell == 0.9.6.*
-}
{- project:
allow-newer: bytestring
-}
{-# LANGUAGE GHC2021 #-}
{-# OPTIONS_GHC -Wall -fplugin=LiquidHaskell #-}

-- Liquid Haskell checks termination for us, but you can disable it if you want.

import Data.Void
import Control.Monad

data Gram a 
  = Fail
  | Empty
  | Char Char 
  | Var a
  | Gram a :|: Gram a
  | Gram a :>: Gram a
  | Fix (Gram (Maybe a))
  deriving (Show, Functor)

infixl 3 :|:
infixl 4 :>:

instance Applicative Gram where
  pure = Var
  (<*>) = ap
-- substitution
instance Monad Gram where
  Fail >>= _ = Fail
  Empty >>= _ = Empty
  Char c >>= _ = Char c
  Var x >>= k = k x
  (g1 :|: g2) >>= k = (g1 >>= k) :|: (g2 >>= k)
  (g1 :>: g2) >>= k = (g1 >>= k) :>: (g2 >>= k)
  (Fix g) >>= k = Fix (g >>= traverse k)

n :: (a -> Bool) -> Gram a -> Bool
n _ Fail = False
n _ Empty = True
n _ Char{} = False
n ev (Var x) = ev x
n ev (g1 :|: g2) = n ev g1 || n ev g2
n ev (g1 :>: g2) = n ev g1 && n ev g2
n ev (Fix g) = n (maybe True ev) g

nullable :: Gram Void -> Bool
nullable = n absurd

data DEv a = DEv { ev_n :: Bool, ev_d :: a, ev_i :: a } deriving Functor

-- derivative
d :: (a -> DEv (Gram b)) -> Char -> Gram a -> Gram b
d _ _ Fail = Fail
d _ _ Empty = Fail
d _ c1 (Char c2)
  | c1 == c2 = Empty
  | otherwise = Fail
d ev _ (Var x) = ev_d (ev x)
d ev c (g1 :|: g2) = d ev c g1 :|: d ev c g2
d ev c (g1 :>: g2)
  | n (ev_n . ev) g1 = (d ev c g1 :>: (g2 >>= ev_i . ev)) :|: d ev c g2
  | otherwise = d ev c g1 :>: (g2 >>= ev_i . ev)
d ev c (Fix g) = Fix $ 
  d 
    (maybe 
      (DEv 
        True 
        (Var Nothing) 
        (Fix (g >>= traverse (fmap Just . ev_i . ev)))) 
      (fmap (fmap Just) . ev))
    c 
    g 

derivative :: Char -> Gram Void -> Gram Void
derivative = d absurd

parse :: String -> Gram Void -> Bool
parse s g0 = nullable (go s g0) where
  go [] g = g
  go (c:cs) g = go cs (derivative c g)

ex :: Gram Void
ex = Fix 
   $  Var Nothing :>: Char '+' :>: Var Nothing
  :|: Char 'x'
  :|: Char '(' :>: Var Nothing :>: Char ')'