Let’s say I have a type Re a
with two features which I call Unsupported.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TypeOperators #-}
import GDP
data Re a =
Eps
| Char a
| Concat (Re a) (Re a)
| Union (Re a) (Re a)
| Star (Re a)
| UnsupportedA (Re a)
| UnsupportedB (Re a)
unsafeSupportedEval :: [a] -> Re a -> Bool
unsafeSupportedEval = undefined
I want to use the GDP library to make sure that when I use this unsafe function, I have a proof that the regex being used is checked to be safe. So I start doing this:
hasUnsupported :: Re a -> Bool
hasUnsupported Eps = False
hasUnsupported (Char _) = False
hasUnsupported (Concat r1 r2) = hasUnsupported r1 || hasUnsupported r2
hasUnsupported (Union r1 r2) = hasUnsupported r1 || hasUnsupported r2
hasUnsupported (Star r) = hasUnsupported r
hasUnsupported (UnsupportedA _) = True
hasUnsupported (UnsupportedB _) = True
And then, I bring in some magic incantations
newtype Unsupported re = Unsupported Defn
type role Unsupported nominal
classifySupported :: (Re a ~~ re) -> Either (Proof (Unsupported re)) (Proof (Not (Unsupported re)))
classifySupported (The re)
| hasUnsupported re = Left axiom
| otherwise = Right axiom
Question 1: What is nominal?
Question 2: Is this the correct signature for the function I want for reflection? I can think of some other alternatives. For example,
(Re a ~~ re) -> Proof (Unsupported re || Not (Unsupported re))
Or, Re a -> Either ((Re a) ?Unsupported) ((Re a) ? (Not Unsupported))
Question 3: The second option is a kind mismatch. What should be the correct way to use the Not operation?
I can have a function which only deals with the subtype of Unsupported things.
withUnsupported :: (Re a ? Unsupported) -> IO ()
withUnsupported (The re) = case re of
UnsupportedA _ -> putStrLn "UnsupportedA"
UnsupportedB _ -> putStrLn "UnsupportedB"
This looks fine to me?
Question 4: How do I write something similar for supported? withSupported :: (Re a ? (Not Unsupported)) -> IO ()
Question 5: How do invoke withUnsupported
correctly in the following function? I want to be able to combine the proof with the re.
useRe :: Re a -> IO ()
useRe re = case classifySupported (The re) of
Left unsupported -> withUnsupported undefined -- how do I define this?
Right supported -> do
putStrLn "Supported"
print $ unsafeSupportedEval "abc" re